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

[ChrisK]

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