Good idea. I'll improve the message by adding the suggestion to use a case expression instead.
Simon | -----Original Message----- | From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Jason Dagit | Sent: 21 June 2007 00:46 | To: Simon Peyton-Jones | Cc: Ian Lynagh; haskell-cafe@haskell.org; [EMAIL PROTECTED] | Subject: Re: [darcs-devel] advice on GADT type witnesses needed | | On 6/20/07, Simon Peyton-Jones <[EMAIL PROTECTED]> 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:[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
