search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

'impossible' happened for lambda expression: bound not comparable #298

Closed gteege closed 4 years ago

gteege commented 4 years ago

The following code 

type A
type G a 
type R = { f1 : (G A)! }
f : R -> R
f r =
  let t = (\s => if True then s else s) r
  in if True then t else t

causes the error message:

Parsing...
Resolving dependencies...
Typechecking...
Desugaring and typing...
cogent: bound: not comparable: (TCon "A" [] (Boxed True (Bits {allocSize = 0, allocOffset = 0})),TCon "A" [] (Boxed False (Bits {allocSize = 0, allocOffset = 0}))): the 'impossible' happened!
If you see this, please report this bug to
    <https://github.com/NICTA/cogent/issues>

The error disappears when one of the conditions is simplified, or when the lambda expression is replaced by a seperate toplevel defined function.

vjackson725 commented 4 years ago

Here's a simplified test case which also causes the issue.

type A
type G a 

f : (G A)! -> (G A)!
f r = (\s => s) r

The issue is roughly caused because the core type inference infers the type (G A)! -> (G A)! for the function, but the argument has the type (G A!)! after is has been converted from the surface types.

Indeed, changing the example to

type A
type G a 

f : (G A!)! -> (G A!)!
f r = (\s => s) r

prevents the error from occuring.

The issue seems caused by the surface to core translation being incorrect at some point.