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@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On | Behalf Of Wolfgang Jeltsch | Sent: 02 September 2008 12:20 | To: glasgow-haskell-users@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@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users