GADT pattern match in nonrigid context
Simon PeytonJones
simonpj at microsoft.com
Tue Sep 2 07:58:14 EDT 2008
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: glasgowhaskellusersbounces at haskell.org [mailto:glasgowhaskellusersbounces at haskell.org] On
 Behalf Of Wolfgang Jeltsch
 Sent: 02 September 2008 12:20
 To: glasgowhaskellusers at haskell.org
 Subject: GADT pattern match in nonrigid context

 Hello,

 I have some code giving me the error message: “GADT pattern match in nonrigid
 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 email 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
 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
More information about the Glasgowhaskellusers
mailing list