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

6 Feb 2008

      Let me add:
...
data ExpGADT t where
    ExpInt :: Int -> ExpGADT Int
    ExpChar :: Char -> ExpGADT Char
Which type do you think 'unHide' and 'wierd' should have:
...
unHide h = case h of
             Hidden (_,e) -> e
wierd = unHide  (Hidden (TyInt,ExpInt 3))
either:
...
unHide :: HiddenTypeExp -> ExpGADT t    -- Choice 1: Polymorphic t
...
unHide :: HiddenTypeExp -> ExpGADT Int  -- Choice 2: Monomorphic Int
Note that TypeGADT/TyInt are irrelevant to unHide and wierd.

Clearly the first choice to unHide violates the encapsulation of 't'.
Clearly I cannot choose the 2nd choice, since it might be an ExpChar.
So unHide is impossible to write.

Chris Casinghino wrote:
...
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

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

ChrisK