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

[Chris Casinghino]

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

> 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
>
>