Because I used a very large function, the output ended up making it difficult to notice all the errors. The message for a missing case could be at the end or at the beginning of the type-checker's output, as it is sandwiched between one error message and another, which can cause us to miss the error messages above it.
CHECKING The file 'issue-18-02.kind2'
ERROR Repeated name
┌──[issue-18-02.kind2:17:29]
│
16 │ Empty.absurd emp
17 │ Fro_mult_0_3 n (Nat.succ m) p (Either.right (Either.right l (Equal p Nat.zero) val)) =
│ ┬ ┬
│ │ └Second occurence
│ └First occurence
18 │ let mult_0_r_n = Mult_0_r n
Hint: Rename one of the occurences
WARN This function does not cover all the possibilities!
• Missing case : 0n 0n 0n (Either.right (Either.left _))
┌──[issue-18-02.kind2:1:1]
│
1 │ Fro_mult_0_3 (n: Nat) (m: Nat) (p: Nat) (e: Either (Equal n Nat.zero) (Either (Equal m Nat.zero) (Equal p Nat.zero))) : (Equal (Nat.mul n (Nat.mul m p)) Nat.zero )
│ ┬───────────
│ └Here!
2 │ Fro_mult_0_3 Nat.zero m p (Either.left Equal.refl) = Equal.refl
3 │ Fro_mult_0_3 n Nat.zero p (Either.right Equal.refl) = Mult_0_r n
ERROR Type mismatch
• Got : (Equal Nat (Nat.mul n (Nat.add (Nat.mul m p) p)) 0n)
• Expected : (Equal Nat (Nat.mul n (Nat.add (Nat.mul m p) p)) 0n)
• Context:
• n : Nat
• m : Nat
• p : Nat
• x_15 : Type
• x_15 = (Equal _ n 0n)
• x_16 : Type
• x_16 = (Either (Equal _ (Nat.succ m) 0n) (Equal _ p 0n))
• x_16 = (Either l (Equal x_17 p 0n))
• l : Type
• x_17 : Type
• x_17 = Nat
• p : x_17
• val : (Equal x_17 p 0n)
• mult_0_r_n : (Equal Nat (Nat.mul n 0n) 0n)
• mult_0_r_n = (Mult_0_r n)
• mult_m_p_e : (Equal Nat (Nat.add (Nat.mul m p) p) 0n)
• mult_m_p_e = (Mult_n_m_eq_z m p val)
• rwt : (Equal Nat (Nat.mul n (Nat.add (Nat.mul m p) p)) 0n)
• rwt = (Equal.rewrite Nat 0n (Nat.add (Nat.mul m p) p) (Equal.mirror Nat (Nat.add (Nat.mul m p) p) 0n mult_m_p_e) (x => (Equal Nat (Nat.mul n x) 0n)) mult_0_r_n)
┌──[issue-18-02.kind2:21:3]
│
20 │ let rwt = Equal.rewrite (Equal.mirror (mult_m_p_eq_0)) (x => (Equal Nat (Nat.mul n x) 0n)) mult_0_r_n
21 │ rwt
│ ┬──
│ └Here!
22 │
FAILED Took 0s
kind2 check --coverage issue-18-02.kind2 0,15s user 0,01s system 99% cpu 0,161 total
Because I used a very large function, the output ended up making it difficult to notice all the errors. The message for a missing case could be at the end or at the beginning of the type-checker's output, as it is sandwiched between one error message and another, which can cause us to miss the error messages above it.
Functions used when noticing an error:
https://gist.github.com/SergioBonatto/8cc248e165d54adca74879e9f1e88635