I've improved the error message for this case. It was indeed bizarrely confusing.
Simon | -----Original Message----- | From: Ian Lynagh [mailto:[EMAIL PROTECTED] | Sent: 15 June 2007 15:53 | To: Jason Dagit | Cc: haskell-cafe@haskell.org; [EMAIL PROTECTED]; 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 <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
