On Feb 6, 2008 7:24 AM, ChrisK <[EMAIL PROTECTED]> 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 > > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
