[Haskell-cafe] weird ghci behavior with gadts and existentials

[Chris Casinghino]

Hi all,

I've been playing a bit with gadts and existentials lately, and I
have an example where I don't quite understand the behavior of
ghc.  The expression in question typechecks sometimes in some
versions of ghc, depending on where you write it, and not in
other versions.  Some other people I've asked report not getting
any errors, even when using apparently one of the same versions
of ghc I checked.

If I create a file which contains:

> data TypeGADT t where
>     TyInt :: TypeGADT Int
>
> data ExpGADT t where
>     ExpInt :: Int -> ExpGADT Int
>
> data HiddenTypeExp =  forall t . Hidden (TypeGADT t, ExpGADT t)
>
> weird = case Hidden (TyInt, ExpInt 3) of Hidden (TyInt, e) -> e

I am able to :load it into ghci just fine (with -fglasgow-exts)
with version 6.8.2.  However, if I then copy the line:

let weird2 = case Hidden (TyInt, ExpInt 3) of Hidden (TyInt, e) -> e

into ghci, I get a type error.  In the HEAD version 6.9, I get a
type error on the definition of "weird" right away when I :load
the file.  The type error goes away if I add the line

> weird :: ExpGADT Int

before the definition of weird.

The type error in question is this:

<interactive>:1:46:
    Inferred type is less polymorphic than expected
      Quantified type variable `t' escapes
    When checking an existential match that binds
        e :: ExpGADT t
    The pattern(s) have type(s): HiddenTypeExp
    The body has type: ExpGADT t
    In a case alternative: Hidden (TyInt, e) -> e
    In the expression:
        case Hidden (TyInt, ExpInt 3) of Hidden (TyInt, e) -> e

So, several questions.

1) Why the discrepancy in behavior between ":load"ing the file and
copying in the definition in 6.8.2.  It seems like, one way or the
other, this should be consistent.

2) Several other people report not getting any errors at all, even
people with ghc 6.8.2, one of the versions I tested.  What's the
"right" behavior?  My guess would be that this should cause no
type error, even without the type annotation.  The GADT pattern
match against "TyInt" in the case statement should refine the
existential type variable t to Int, so no existential type
variables are escaping.  Is that right?

3) Is there a bug here?  Are there two bugs (one, the typing error,
two, the difference between ghc and ghci)?  Or, do I just not
understand what is going on?

Sorry for the length of this email!

--Chris Casinghino