HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.58k stars 142 forks source link

Inconsistency in type check messages #571

Closed SergioBonatto closed 4 months ago

SergioBonatto commented 1 year ago

In one case it claims that not all possible cases are covered, and when adding the case indicated by the Kind, it claims that the case is impossible

Message without the indicated case:

   CHECKING  The file 'book.kind2'
   WARN  This function does not cover all the possibilities!

      • Missing case : (Nat.succ (Nat.succ _)) Ev.ev_z 

      ┌──[book.kind2:96:1]
      │
   95 │    // #partial
   96 │    Ev_even 
      │    ┬──────
      │    └Here!
   97 │      (n: Nat) 

    CHECKED  All terms checked. took 0.22s

Message with the indicated case:


   CHECKING  The file 'book.kind2'
   ERROR  Impossible case.

      • Expected : (Ev (Nat.succ (Nat.succ n))) 
      • Got      : (Ev 0n) 

      ┌──[book.kind2:103:33]
      │
  102 │    Ev_even (Nat.succ (Nat.succ n)) (Ev.ev_ss e) = Ev_even_ss n (Ev_even n e)
  103 │    Ev_even (Nat.succ (Nat.succ n)) Ev.ev_z = ?
      │                                    ┬──────
      │                                    └Here!
  104 │    

     FAILED  Took 0s