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
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
participants (2)
-
Simon Peyton-Jones -
Wolfgang Jeltsch