GADT problems

[Jason Dagit]

On Sun, Sep 14, 2008 at 7:11 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> Neil
>
> It's by design, and for (I think) good reason.   GHC now enforces the rule that in a GADT pattern match
>        - the type of the scrutinee must be rigid
>        - the result type must be rigid
>        - the type of any variable free in the case branch must be rigid
>
> Here "rigid" means "fully known to the compiler, usually by way of a type signature".  This rule is to make type inference simple and predictable -- it dramatically simplifies inference.
>
> To see the issue, ask yourself what is the type of this function
>
> data E a where
>  EI :: E Int
>
> f EI = 3::Int
>
> Should the inferred type be
>        f :: E a -> a
> or
>        f :: E a -> Int
> We can't tell, and neither is more general than the other.  So GHC insists on knowing the result type.  That's why you had to give the signature g::[()] in your example.
>
>
> So that's the story.  If you find situations in which it's very hard to give a signature for the result type, I'd like to see them.

I find that usually when it becomes difficult is when I'm using
existential types and lexically scoped type variables.

I don't have an example ready but I could vaguely describe it.

For example, using a case expression to pattern match on a constructor
that has an existential type and also expecting part of the type of
that expression to match a lexically scope type variable (I'm often
also using phantom types, if that matters).  In this case, I usually
end up adding a where clause to specify the type signature while
dancing around the other issues.  It's typically not pretty but at the
end of the day I've always been able to find a way to specify the type
I need.

Although, it does make me quite aware that GHC could report the type
errors better when dealing with phantom types that are bound to an
existential type.  If you have multiple such phantoms as part of the
type it can be quite confusing to figure out which ones the type
checker isn't happy with.

data Sealed a where
  Sealed :: a x y -> Sealed a

data Foo a x y where ....

case sealedFoo where
  Sealed (Foo 4) -> ...

If you get a type error in the above sometimes it's hard to figure out
if it's happening with x or with y.  Sometimes the type parameter name
chosen doesn't give you a hint about which type parameter of Foo is
not unifying.

I wish I had a concrete example to show you.  I guess the next time it
shows up I should send it in.

Thanks,
Jason