GADT pattern match in non-rigid context

[Simon Peyton-Jones]

Wolfgang

You need to say that type "t", the case scrutinee, has.  You can use a type signature for that.

Presumably the way that a' is instantiated doesn't matter, but GHC isn't clever enough to realise that.  So I just instantiated it to ().

The result compiles fine.

Simon

{-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs #-}

module Foo where

data T a b where
    C :: T a [b]

f :: forall a b. (forall a'. T a' b) -> T a b
f t = case t :: T () b of C -> C

| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-bounces at haskell.org] On
| Behalf Of Wolfgang Jeltsch
| Sent: 02 September 2008 12:20
| To: glasgow-haskell-users at haskell.org
| Subject: GADT pattern match in non-rigid context
|
| Hello,
|
| I have some code giving me the error message: “GADT pattern match in non-rigid
| context for … Tell GHC HQ if you'd like this to unify the context”.  I
| reduced my code to the following example which still gives this error
| message:
|
| > data T a b where
| >
| >     C :: T a [b]
| >
| > f :: (forall a'. T a' b) -> T a b
| > f t = case t of C -> C
|
| How do I work around this error?  Some former e-mail discussion gave the hint
| of adding a type signature but this probably doesn’t work in my case.  Note
| also that specializing the type of the argument t to T a b inside the
| definition of f is not an option since in the real code I need the first
| argument of T to be universally quantified for calling another function which
| needs this quantification.
|
| I use GHC 6.8.2.  Don’t know whether this problem still shows up with GHC HEAD
| but am interested in hearing whether this is the case.
|
| I’m thankful for any help.
|
| Best wishes,
| Wolfgang
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users