[Haskell-cafe] Re: weird ghci behavior with gadts and existentials
haskell at list.mightyreason.com
Wed Feb 6 07:24:13 EST 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))
> 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:
> 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
More information about the Haskell-Cafe