"A lazy (~) pattern cannot bind existential type variables" happens for non-existential GADTs

[ganesh]

This program:

{-# LANGUAGE GADTs #-}
module Foo where

data Foo a where
   Foo :: a -> Foo (a, Int)

foo :: Foo (a, Int) -> a
foo ~(Foo a) = a

causes this error:

Foo.hs:8:4:
    A lazy (~) pattern cannot bind existential type variables
      `a' is a rigid type variable bound by
          the constructor `Foo' at Foo.hs:8:6
    In the pattern: ~(Foo a)
    In the definition of `foo': foo ~(Foo a) = a

This doesn't seem like an existential, as there aren't any type variables in the arguments to Foo that aren't in the result type.

If easy it would be nice if the restriction were relaxed to allow for this case, otherwise I think the error message should be improved.

Tested with ghc 6.10.1.20081209 and ghc 6.11.20090107.

[simonpj]

The error message is not good, but it's right to reject this program. More precisely, it'd definitely be right to reject this program:

bar :: a -> Foo a -> a
bar x ~(Foo _) = fst x

Because I could call bar 3 undefined, and thereby crash. Now in this case (a) the data type has only one constructor, (b) the type signature for foo ensures that every call will match Foo's constraints. So nothing would go wrong. But it's a very special case. And I don't know how to translate it into System F (or more precisely Fc).

So it's not easy. So I propose to do nothing except perhaps make the error message mention GADTs too.

Simon

[simonpj]

Changed error message

Tue Jan 13 16:40:20 GMT 2009  simonpj@microsoft.com
  * Improve error messages slightly

The change is this

    hunk ./compiler/typecheck/TcPat.lhs 981
    -	        text "I can't handle pattern bindings for existentially-quantified constructors.",
    +	        text "I can't handle pattern bindings for existential or GADT data constructors.",
    hunk ./compiler/typecheck/TcPat.lhs 1033
    -    hang (ptext (sLit "A lazy (~) pattern cannot bind existential type variables"))
    +    hang (ptext (sLit "A lazy (~) pattern cannot match existential or GADT data constructors"))