GADT problems

[Simon Peyton-Jones]

Ah -- you used an *existential* there!  Yes, existentially-bound type variables are rigid.  They stand for themselves, as it were.

That resolves the mystery -- but it existentials admittedly introduce a new complication

How should this be clarified?

S

| -----Original Message-----
| From: Mitchell, Neil [mailto:neil.mitchell.2 at credit-suisse.com]
| Sent: 15 September 2008 13:56
| To: Simon Peyton-Jones; glasgow-haskell-users at haskell.org
| Subject: RE: GADT problems
|
| > | > | (case undefined of Foo GadtValue -> ()) :: () -- is rigid
| > ...
| > |
| > | But the first compiles fine, so it seems that the scrutinee doesn't
| > | have to always be rigid?
| >
| > Not for me! Either with 6.8.3 or HEAD.  What compiler are you using?
|
| HEAD from last Thursday. The code I'm using is slightly different to
| your code, and is attached at the end of the message. Is matching Foo
| causing its argument to become rigid?
|
| Thanks
|
| Neil
|
| {-# LANGUAGE GADTs, ScopedTypeVariables #-}
| module Test where
|
| data E x = E x
|
| data Foo where
|   Foo :: Gadt a -> Foo
|
| data Gadt a where
|   GadtValue :: Gadt (E a)
|
| g :: ()
| g = case undefined of
|         Foo GadtValue -> ()
|
| ==============================================================================
| Please access the attached hyperlink for an important electronic communications disclaimer:
|
| http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
| ==============================================================================
|