RE: GADT pattern match in non-rigid context
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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] 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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: GADT pattern match in non-rigid context
| >> You should be giving a type signature to rewrap! That should fix it.
| >
| > Thanks, all works fine now :-)
|
| it would be great if the error message suggested giving a type signature
| as a solution (or maybe it already does, in the HEAD?)
Good point: I'll do that.
Simon
| >> | -Original Message-
| >> | From: [EMAIL PROTECTED] [mailto:glasgow-haskell-
| [EMAIL PROTECTED] On Behalf Of
| >> | Neil Mitchell
| >> | Sent: 17 December 2007 16:23
| >> | To: glasgow-haskell-users@haskell.org
| >> | Subject: GADT pattern match in non-rigid context
| >> |
| >> | Hi,
| >> |
| >> | Upgrading from GHC 6.6 to 6.8 has caused some code to stop working:
| >> |
| >> | --
| >> | {-# OPTIONS_GHC -fglasgow-exts #-}
| >> |
| >> | module Data2 where
| >> |
| >> | data CCompany
| >> |
| >> | data Paradise :: * -> * where
| >> | CC :: Paradise CCompany
| >> |
| >> | rewrapCC CC = []
| >> | --
| >> |
| >> | [1 of 1] Compiling Data2( Data2.hs, interpreted )
| >> |
| >> | Data2.hs:12:9:
| >> | GADT pattern match in non-rigid context for `CC'
| >> | Tell GHC HQ if you'd like this to unify the context
| >> | In the pattern: CC
| >> | In the definition of `rewrapCC': rewrapCC CC = []
| >> |
| >> | This code is from the Uniplate benchmarking code, which runs the
| >> | Paradise benchmark from SYB on Uniplate, Compos and SYB. The Compos
| >> | code uses GADT's, so the program first needs to convert from standard
| >> | data structures to GADT's before it can work, then back at the end.
| >> | It's the problem of converting from a GADT to a normal data structure
| >> | that is failing.
| >> |
| >> | So is there an easy workaround? Or should I be asking GHC HQ to unify
| things?
| >> |
| >> | Thanks
| >> |
| >> | Neil
| >> | ___
| >> | Glasgow-haskell-users mailing list
| >> | Glasgow-haskell-users@haskell.org
| >> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
| >>
| > ___
| > Glasgow-haskell-users mailing list
| > Glasgow-haskell-users@haskell.org
| > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
| >
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT pattern match in non-rigid context
Neil Mitchell wrote:
Hi Simon,
You should be giving a type signature to rewrap! That should fix it.
Thanks, all works fine now :-)
it would be great if the error message suggested giving a type signature
as a solution (or maybe it already does, in the HEAD?)
Isaac
Neil
| -Original Message-
| From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of
| Neil Mitchell
| Sent: 17 December 2007 16:23
| To: glasgow-haskell-users@haskell.org
| Subject: GADT pattern match in non-rigid context
|
| Hi,
|
| Upgrading from GHC 6.6 to 6.8 has caused some code to stop working:
|
| --
| {-# OPTIONS_GHC -fglasgow-exts #-}
|
| module Data2 where
|
| data CCompany
|
| data Paradise :: * -> * where
| CC :: Paradise CCompany
|
| rewrapCC CC = []
| --
|
| [1 of 1] Compiling Data2( Data2.hs, interpreted )
|
| Data2.hs:12:9:
| GADT pattern match in non-rigid context for `CC'
| Tell GHC HQ if you'd like this to unify the context
| In the pattern: CC
| In the definition of `rewrapCC': rewrapCC CC = []
|
| This code is from the Uniplate benchmarking code, which runs the
| Paradise benchmark from SYB on Uniplate, Compos and SYB. The Compos
| code uses GADT's, so the program first needs to convert from standard
| data structures to GADT's before it can work, then back at the end.
| It's the problem of converting from a GADT to a normal data structure
| that is failing.
|
| So is there an easy workaround? Or should I be asking GHC HQ to unify things?
|
| Thanks
|
| Neil
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT pattern match in non-rigid context
Hi Simon,
> You should be giving a type signature to rewrap! That should fix it.
Thanks, all works fine now :-)
Neil
>
> | -Original Message-
> | From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of
> | Neil Mitchell
> | Sent: 17 December 2007 16:23
> | To: glasgow-haskell-users@haskell.org
> | Subject: GADT pattern match in non-rigid context
> |
> | Hi,
> |
> | Upgrading from GHC 6.6 to 6.8 has caused some code to stop working:
> |
> | --
> | {-# OPTIONS_GHC -fglasgow-exts #-}
> |
> | module Data2 where
> |
> | data CCompany
> |
> | data Paradise :: * -> * where
> | CC :: Paradise CCompany
> |
> | rewrapCC CC = []
> | --
> |
> | [1 of 1] Compiling Data2( Data2.hs, interpreted )
> |
> | Data2.hs:12:9:
> | GADT pattern match in non-rigid context for `CC'
> | Tell GHC HQ if you'd like this to unify the context
> | In the pattern: CC
> | In the definition of `rewrapCC': rewrapCC CC = []
> |
> | This code is from the Uniplate benchmarking code, which runs the
> | Paradise benchmark from SYB on Uniplate, Compos and SYB. The Compos
> | code uses GADT's, so the program first needs to convert from standard
> | data structures to GADT's before it can work, then back at the end.
> | It's the problem of converting from a GADT to a normal data structure
> | that is failing.
> |
> | So is there an easy workaround? Or should I be asking GHC HQ to unify
> things?
> |
> | Thanks
> |
> | Neil
> | ___
> | Glasgow-haskell-users mailing list
> | Glasgow-haskell-users@haskell.org
> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: GADT pattern match in non-rigid context
You should be giving a type signature to rewrap! That should fix it.
Simon
| -Original Message-
| From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of
| Neil Mitchell
| Sent: 17 December 2007 16:23
| To: glasgow-haskell-users@haskell.org
| Subject: GADT pattern match in non-rigid context
|
| Hi,
|
| Upgrading from GHC 6.6 to 6.8 has caused some code to stop working:
|
| --
| {-# OPTIONS_GHC -fglasgow-exts #-}
|
| module Data2 where
|
| data CCompany
|
| data Paradise :: * -> * where
| CC :: Paradise CCompany
|
| rewrapCC CC = []
| --
|
| [1 of 1] Compiling Data2( Data2.hs, interpreted )
|
| Data2.hs:12:9:
| GADT pattern match in non-rigid context for `CC'
| Tell GHC HQ if you'd like this to unify the context
| In the pattern: CC
| In the definition of `rewrapCC': rewrapCC CC = []
|
| This code is from the Uniplate benchmarking code, which runs the
| Paradise benchmark from SYB on Uniplate, Compos and SYB. The Compos
| code uses GADT's, so the program first needs to convert from standard
| data structures to GADT's before it can work, then back at the end.
| It's the problem of converting from a GADT to a normal data structure
| that is failing.
|
| So is there an easy workaround? Or should I be asking GHC HQ to unify things?
|
| Thanks
|
| Neil
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
