On 6/15/07, Ian Lynagh <igloo@earth.li> wrote:

On Thu, Jun 14, 2007 at 08:27:36PM -0700, Jason Dagit wrote:

...

On 6/14/07, David Roundy <droundy@darcs.net> wrote:

...

src/Darcs/Patch/Show.lhs:50:0: Quantified type variable `y' is unified with another quantified type variable `x' When trying to generalise the type inferred for `showPatch' Signature type: forall x y. Patch x y -> Doc Type to generalise: Patch y y -> Doc In the type signature for `showPatch' When generalising the type(s) for showPatch, showComP, showSplit, showConflicted, showNamed make: *** [src/Darcs/Patch/Show.o] Error 1

The relevant code is

showPatch :: Patch C(x,y) -> Doc showPatch (FP f AddFile) = showAddFile f ... showPatch (Conflicted p ps) = showConflicted p ps

and the trouble comes about because of (in Core.lhs)

data Patch C(x,y) where NamedP :: !PatchInfo -> ![PatchInfo] -> !(Patch C(x,y)) -> Patch C(x,y) ... Conflicted :: Patch C(a,b) -> FL Patch C(b,c) -> Patch C(c,c)

I would like to add that I've tried (and failed) to construct a minimal example that demonstrates the type check failure by simulating the relevant code above. This makes me wonder if the problem is not in the obvious place(s).

Here's one:

module Q where

data Foo x y where Foo :: Foo a b -> Foo b c -> Foo c c

------

module W where

import Q

wibble :: Foo a b -> String wibble (Foo x y) = foo x y

foo :: Foo a b -> Foo b c -> String foo x y = wibble x ++ wibble y

6.6 and 6.6.1 say:

$ ghc -c Q.hs -fglasgow-exts $ ghc -c W.hs

W.hs:7:0: Quantified type variable `b' is unified with another quantified type variable `a' When trying to generalise the type inferred for `wibble' Signature type: forall a b. Foo a b -> String Type to generalise: Foo b b -> String In the type signature for `wibble' When generalising the type(s) for wibble, foo $ ghc -c W.hs -fglasgow-exts $

i.e. you need to give the -fglasgow-exts flag when compiling W.hs. An {-# OPTIONS_GHC -fglasgow-exts #-} pragma in Show.lhs fixes the real thing too.

The HEAD is the same, except the error is:

W.hs:7:8: GADT pattern match in non-rigid context for `Foo' Tell GHC HQ if you'd like this to unify the context In the pattern: Foo x y In the definition of `wibble': wibble (Foo x y) = foo x y

I suspect your problem in making a testcase was moving the GADT declaration into the same file as the function, and thus needing to compile it with -fglasgow-exts anyway.

Yes, you're basically right about what I tried. I did suspect putting things into different modules was important, so I did that, but I was using ghci with -fglasgow-exts to load all the files. So that explains why I failed to trigger the problem. Sounds like this should be easy to fix on our end. thanks! Jason

I've improved the error message for this case. It was indeed bizarrely confusing. Simon | -----Original Message----- | From: Ian Lynagh [mailto:igloo@earth.li] | Sent: 15 June 2007 15:53 | To: Jason Dagit | Cc: haskell-cafe@haskell.org; darcs-devel@darcs.net; Simon Peyton-Jones | Subject: Re: [darcs-devel] advice on GADT type witnesses needed | | On Thu, Jun 14, 2007 at 08:27:36PM -0700, Jason Dagit wrote: | > On 6/14/07, David Roundy <droundy@darcs.net> wrote: | > | > >src/Darcs/Patch/Show.lhs:50:0: | > > Quantified type variable `y' is unified with another quantified type | > > variable `x' | > > When trying to generalise the type inferred for `showPatch' | > > Signature type: forall x y. Patch x y -> Doc | > > Type to generalise: Patch y y -> Doc | > > In the type signature for `showPatch' | > > When generalising the type(s) for showPatch, showComP, showSplit, | > > showConflicted, showNamed | > >make: *** [src/Darcs/Patch/Show.o] Error 1 | > > | > >The relevant code is | > > | > >showPatch :: Patch C(x,y) -> Doc | > >showPatch (FP f AddFile) = showAddFile f | > >... | > >showPatch (Conflicted p ps) = showConflicted p ps | > > | > >and the trouble comes about because of (in Core.lhs) | > > | > >data Patch C(x,y) where | > > NamedP :: !PatchInfo -> ![PatchInfo] -> !(Patch C(x,y)) -> Patch C(x,y) | > >... | > > Conflicted :: Patch C(a,b) -> FL Patch C(b,c) -> Patch C(c,c) | > > | > | > I would like to add that I've tried (and failed) to construct a | > minimal example that demonstrates the type check failure by simulating | > the relevant code above. This makes me wonder if the problem is not | > in the obvious place(s). | | Here's one: | | module Q where | | data Foo x y where | Foo :: Foo a b -> Foo b c -> Foo c c | | ------ | | module W where | | import Q | | wibble :: Foo a b -> String | wibble (Foo x y) = foo x y | | foo :: Foo a b -> Foo b c -> String | foo x y = wibble x ++ wibble y | | 6.6 and 6.6.1 say: | | $ ghc -c Q.hs -fglasgow-exts | $ ghc -c W.hs | | W.hs:7:0: | Quantified type variable `b' is unified with another quantified type variable `a' | When trying to generalise the type inferred for `wibble' | Signature type: forall a b. Foo a b -> String | Type to generalise: Foo b b -> String | In the type signature for `wibble' | When generalising the type(s) for wibble, foo | $ ghc -c W.hs -fglasgow-exts | $ | | i.e. you need to give the -fglasgow-exts flag when compiling W.hs. | An {-# OPTIONS_GHC -fglasgow-exts #-} pragma in Show.lhs fixes the real | thing too. | | The HEAD is the same, except the error is: | | W.hs:7:8: | GADT pattern match in non-rigid context for `Foo' | Tell GHC HQ if you'd like this to unify the context | In the pattern: Foo x y | In the definition of `wibble': wibble (Foo x y) = foo x y | | I suspect your problem in making a testcase was moving the GADT | declaration into the same file as the function, and thus needing to | compile it with -fglasgow-exts anyway. | | I'm not sure if GHC's behaviour is what is expected though; Simon? | | | Thanks | Ian

Good idea. I'll improve the message by adding the suggestion to use a case expression instead. Simon | -----Original Message----- | From: dagitj@gmail.com [mailto:dagitj@gmail.com] On Behalf Of Jason Dagit | Sent: 21 June 2007 00:46 | To: Simon Peyton-Jones | Cc: Ian Lynagh; haskell-cafe@haskell.org; darcs-devel@darcs.net | Subject: Re: [darcs-devel] advice on GADT type witnesses needed | | On 6/20/07, Simon Peyton-Jones <simonpj@microsoft.com> wrote: | > I've improved the error message for this case. It was indeed bizarrely confusing. | | While we're on the subject of bizarrely confusing error messages :) | | I had some code like this: | ... | where | MergeResult (_:>p2') (_:>p1' ) (_cp1 :\./:_cp2) = fancy_merge $ p1 :\./: p2 | | and GHC gave me this error message: | My brain just exploded. | I can't handle pattern bindings for existentially-quantified constructors. | | Which is amusing, but it doesn't hint (enough) at the workaround, | which appears to be using 'case' instead of let/where. Any chance | this could be improved to suggest the user tries switching to a case? | | I'm now using this code: | case fancy_merge $ p1 :\./: p2 of | MergeResult (_:>p2') (_:>p1' ) (_cp1 :\./:_cp2) | | Which seems to make it further with the type checking (my code is | wrong, but at least now I get a normal error from ghc). | | Thanks, | Jason | | > | > Simon | > | > | -----Original Message----- | > | From: Ian Lynagh [mailto:igloo@earth.li] | > | Sent: 15 June 2007 15:53 | > | To: Jason Dagit | > | Cc: haskell-cafe@haskell.org; darcs-devel@darcs.net; Simon Peyton-Jones | > | Subject: Re: [darcs-devel] advice on GADT type witnesses needed | > | | > | On Thu, Jun 14, 2007 at 08:27:36PM -0700, Jason Dagit wrote: | > | > On 6/14/07, David Roundy <droundy@darcs.net> wrote: | > | > | > | > >src/Darcs/Patch/Show.lhs:50:0: | > | > > Quantified type variable `y' is unified with another quantified type | > | > > variable `x' | > | > > When trying to generalise the type inferred for `showPatch' | > | > > Signature type: forall x y. Patch x y -> Doc | > | > > Type to generalise: Patch y y -> Doc | > | > > In the type signature for `showPatch' | > | > > When generalising the type(s) for showPatch, showComP, showSplit, | > | > > showConflicted, showNamed | > | > >make: *** [src/Darcs/Patch/Show.o] Error 1 | > | > > | > | > >The relevant code is | > | > > | > | > >showPatch :: Patch C(x,y) -> Doc | > | > >showPatch (FP f AddFile) = showAddFile f | > | > >... | > | > >showPatch (Conflicted p ps) = showConflicted p ps | > | > > | > | > >and the trouble comes about because of (in Core.lhs) | > | > > | > | > >data Patch C(x,y) where | > | > > NamedP :: !PatchInfo -> ![PatchInfo] -> !(Patch C(x,y)) -> Patch C(x,y) | > | > >... | > | > > Conflicted :: Patch C(a,b) -> FL Patch C(b,c) -> Patch C(c,c) | > | > > | > | > | > | > I would like to add that I've tried (and failed) to construct a | > | > minimal example that demonstrates the type check failure by simulating | > | > the relevant code above. This makes me wonder if the problem is not | > | > in the obvious place(s). | > | | > | Here's one: | > | | > | module Q where | > | | > | data Foo x y where | > | Foo :: Foo a b -> Foo b c -> Foo c c | > | | > | ------ | > | | > | module W where | > | | > | import Q | > | | > | wibble :: Foo a b -> String | > | wibble (Foo x y) = foo x y | > | | > | foo :: Foo a b -> Foo b c -> String | > | foo x y = wibble x ++ wibble y | > | | > | 6.6 and 6.6.1 say: | > | | > | $ ghc -c Q.hs -fglasgow-exts | > | $ ghc -c W.hs | > | | > | W.hs:7:0: | > | Quantified type variable `b' is unified with another quantified type variable `a' | > | When trying to generalise the type inferred for `wibble' | > | Signature type: forall a b. Foo a b -> String | > | Type to generalise: Foo b b -> String | > | In the type signature for `wibble' | > | When generalising the type(s) for wibble, foo | > | $ ghc -c W.hs -fglasgow-exts | > | $ | > | | > | i.e. you need to give the -fglasgow-exts flag when compiling W.hs. | > | An {-# OPTIONS_GHC -fglasgow-exts #-} pragma in Show.lhs fixes the real | > | thing too. | > | | > | The HEAD is the same, except the error is: | > | | > | W.hs:7:8: | > | GADT pattern match in non-rigid context for `Foo' | > | Tell GHC HQ if you'd like this to unify the context | > | In the pattern: Foo x y | > | In the definition of `wibble': wibble (Foo x y) = foo x y | > | | > | I suspect your problem in making a testcase was moving the GADT | > | declaration into the same file as the function, and thus needing to | > | compile it with -fglasgow-exts anyway. | > | | > | I'm not sure if GHC's behaviour is what is expected though; Simon? | > | | > | | > | Thanks | > | Ian | > | >