19 Jun
2013
19 Jun
'13
6:11 a.m.
At Wed, 19 Jun 2013 10:03:27 +0000 (UTC), AntC wrote:
Hi Francesco, I think you'll find that the 'annoyance' is nothing to do with GADTs. I suggest you take the type signature off of foo1, and see what type ghc infers for it. It isn't :: a -> Foo a -> Int.
[...]
Yep, that message explains what's going on well enough for me.
Did you read the rest of the code? That ought to work, because GHC infers and uses the type equality (something like ‘v ~ Var v1’) and uses it to coerce the ‘x’. And, surprise surprise, if the argument order is switched, it works! data Foo v where Foo :: forall v. Foo (Maybe v) foo1 :: Foo a -> a -> Int foo1 Foo Nothing = undefined foo1 Foo (Just x) = undefined Francesco