Surface Tc crash on variant mismatch

au-ts / cogent

Cogent Project

https://trustworthy.systems/projects/TS/cogent.pml

Other

158 stars 26 forks source link

Surface Tc crash on variant mismatch #411

Closed zilinc closed 2 years ago

zilinc commented 2 years ago

foo : <A | B | C > -> ()

bar : () -> <A | B>

quux : () -> ()
quux x = foo (bar x)

Error message:

cogent: src/Cogent/TypeCheck/Row.hs:(184,1)-(187,23): Non-exhaustive patterns in function pointwise

cmcl commented 2 years ago

NB: Also resolves an analogous bug for records:

type A
type B
type C

foo : { x : A , y : B } -> ()

bar : () -> { x : A , y : B , c : C! }

quux : () -> ()
quux x = foo (bar x)

zilinc commented 2 years ago

I don't think the fix is correct. In both cases, the surface typecheck should reject the programs. <A | B> is not a subtype of <A | B | C >. Same for the records.