ghc 6.7 and GADT pattern-matching

[Conal Elliott]

got it.  thanks much!  - Conal

On 8/22/07, Simon Peyton-Jones <simonpj at microsoft.com> wrote:
>
>  The issue is different here. You are **lazily** matching the pattern, so
> it'd be unsound in general to accept this. Same thing if you said
>
>                 fstTy ~(a  :-> b) = a
>
> Now in this case the RHS is strict in 'a' so it's probably ok but it's not
> in general. Nothing to do with rigidity.  The error message is bad though
>
>
>
> S
>
>
>
> *From:* conal.elliott at gmail.com [mailto:conal.elliott at gmail.com] *On
> Behalf Of *Conal Elliott
> *Sent:* 22 August 2007 23:34
> *To:* Simon Peyton-Jones
> *Cc:* cvs-ghc at haskell.org
> *Subject:* Re: ghc 6.7 and GADT pattern-matching
>
>
>
> How about this one (relative to same Ty def)?
>
>     fstTy :: Ty (a -> b) -> Ty a
>     fstTy (a :-> b) = a
>
>     fstTy' :: Ty (a -> b) -> Ty a
>     fstTy' ty = a where (a :-> b) = ty
>
> The first definition works, while the second triggers the complaint about
> non-rigidity.    I don't know how to type-annotate the second one to provide
> the required rigidity.  Do you?
>
> Of course, in this example, I can use the first def instead of the
> second.  In my real example, the type being deconstructed is synthesized, so
> the second form is not so convenient.
>
> I'm working around this problem, so no emergency, but still I'd like to
> know what can be done.
>
> Thanks,  - Conal
>
> On 8/22/07, *Simon Peyton-Jones* <simonpj at microsoft.com> wrote:
>
> The issue is this.  When doing GADT matching, getting type inference to
> work well, and interact well with other features (e.g. indexed type
> families) is MUCH easier if the type being matched is totally known – we say
> "rigid".  When you used "$" you made GHC less sure about the type of the
> GADT match.    Our GADT paper describes this rigidity reasoning http://research.microsoft.com/~simonpj/papers/gadt/index.htm
> <http://research.microsoft.com/%7Esimonpj/papers/gadt/index.htm>
>
>
>
> GHC 6.6 was a bit more liberal, but the liberality was delicately
> balanced, and made life too complicated when we added more stuff.
>
>
>
> In any case, the solution is always "add a type signature", though in this
> case you could also escape with "omit a $".
>
>
>
> Simon
>
>
>
> *From:* cvs-ghc-bounces at haskell.org [mailto:cvs-ghc-bounces at haskell.org] *On
> Behalf Of *Conal Elliott
> *Sent:* 22 August 2007 06:15
> *To:* cvs-ghc at haskell.org
> *Subject:* ghc 6.7 and GADT pattern-matching
>
>
>
> In going from ghc-6.6 to ghc-6.7, I've lost some GADT pattern matching
> that I'd really like to have back. The message:
>
>     c:/conal/Haskell/Eros/src/gadt-example.hs :23:32:
>     GADT pattern match in non-rigid context for `:*'
>       Tell GHC HQ if you'd like this to unify the context
>     In the pattern: a :* b
>     In a lambda abstraction: \ (a :* b) -> ((f a) :* b)
>     In the second argument of `($)', namely
>         `\ (a :* b) -> ((f a) :* b)'
>
> and the relevant code:
>
>     -- | Statically typed type representations
>     data Ty :: * -> * where
>       (:*)   :: Ty a -> Ty b -> Ty (a, b)
>       (:->)  :: Ty a -> Ty b -> Ty (a->b)
>       OtherTy :: TypeRep -> Ty a
>
>     -- | Type transformations
>     newtype TyFun a b = TyFun { unTyFun :: Ty a -> Ty b }
>
>     instance Arrow TyFun where
>       TyFun f >>> TyFun g = TyFun (f >>> g)
>       first  (TyFun f) = TyFun $ \ (a :* b) -> (f a :* b)
>       second (TyFun g) = TyFun $ \ (a :* b) -> (a :* g b)
>
> Full test module attached with many more example matchings.
>
> I'd really like to get this code working in ghc-6.7.  How likely is that?
> The best alternative I know is *much* less readable.
>
> Thanks,  - Conal
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/cvs-ghc/attachments/20070822/e1b12979/attachment.htm