[GADTs] Small example of a forgotten refinement

[plredmond]

This GADT has a phantom type that gets refined (GHC-sense) by its constructor(s). That phantom type has a refinement (LH-sense) in the GADT-signature of its constructor. When we pattern match on the GADT constructor, GHC learns its type, but LH doesn't learn the refinement-type.

{-@
data Foo result where A :: Foo {i:Int | i == 0 } @-}
data Foo result where A :: Foo Int

foo :: Foo result -> result
foo A = 123

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1667027035_14060.hs

• Expected: This example should fail because 123 /= 0
• Actual: This example passes because LH applies no refinement-constraints in the branch where Foo result is constructed by A.

[facundominguez]

Another fix here could be to have LH reject the spec of the data constructor A.

[plredmond]

Yeah, if refining phantom types on gadt constructors isn't supported, then LH reject it early in the pipeline.