HigherOrderCO/Kindex

Kind2 check --coverage bug

NaoEhSavio opened this issue · 0 comments

when I use "Kind2 check --coverage" on this file

Bits.from_hex (hex: String): Bits
Bits.from_hex (String.nil) = Bits.e
Bits.from_hex (String.cons '0' xs) = (Bits.o (Bits.o (Bits.o (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons '1' xs) = (Bits.o (Bits.o (Bits.o (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons '2' xs) = (Bits.o (Bits.o (Bits.i (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons '3' xs) = (Bits.o (Bits.o (Bits.i (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons '4' xs) = (Bits.o (Bits.i (Bits.o (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons '5' xs) = (Bits.o (Bits.i (Bits.o (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons '6' xs) = (Bits.o (Bits.i (Bits.i (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons '7' xs) = (Bits.o (Bits.i (Bits.i (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons '8' xs) = (Bits.i (Bits.o (Bits.o (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons '9' xs) = (Bits.i (Bits.o (Bits.o (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'a' xs) = (Bits.i (Bits.o (Bits.i (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'A' xs) = (Bits.i (Bits.o (Bits.i (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'b' xs) = (Bits.i (Bits.o (Bits.i (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'B' xs) = (Bits.i (Bits.o (Bits.i (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'c' xs) = (Bits.i (Bits.i (Bits.o (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'C' xs) = (Bits.i (Bits.i (Bits.o (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'd' xs) = (Bits.i (Bits.i (Bits.o (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'D' xs) = (Bits.i (Bits.i (Bits.o (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'e' xs) = (Bits.i (Bits.i (Bits.i (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'E' xs) = (Bits.i (Bits.i (Bits.i (Bits.o (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'f' xs) = (Bits.i (Bits.i (Bits.i (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons 'F' xs) = (Bits.i (Bits.i (Bits.i (Bits.i (Bits.from_hex xs)))))
Bits.from_hex (String.cons x xs)   = (Bits.from_hex xs)

I get an error

Internal Error: Cannot parse the report message from the type checker: [(Kind.Error.Quoted.uncovered_pattern [] 570425365 (List.cons (Kind.Term.Quoted.ctr (String.cons.) 0 [(Kind.Term.Quoted.var 0 63 0)]) (List.drop [] (Nat.succ (Nat.zero)))))]