[Haskell-cafe] Re: weird ghci behavior with gadts and existentials
chris.casinghino at gmail.com
Wed Feb 6 12:59:25 EST 2008
On Feb 6, 2008 7:24 AM, ChrisK <haskell at list.mightyreason.com> wrote:
> 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))
I agree that unHide, as written, can't be typechecked, because the
existential variable escapes - without the GADT pattern match on
TyInt, t never gets refined. The addition of ExpChar has nothing to
do with this, though - if we replace the underscore with TyInt as
before, the function should still typecheck as:
HiddenTypeExp -> ExpGADT Int
At least, assuming my reasoning was right in the first message.
Now, with the addition of ExpChar we may have a runtime error when
using this function, but it doesn't change the type of these things,
and I'm still stuck trying to figure out if my example before is a bug
of if I misunderstand something. Haskell doesn't have good coverage
checking for GADT cases, and even if it did adding ExpChar would
probably only cause a warning.
It's certainly an interesting case to think about though, in terms of
how existentials and gadts interact.
> 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
More information about the Haskell-Cafe