[Haskell-cafe] Re: [darcs-devel] advice on GADT type witnesses needed

On 6/20/07, Simon Peyton-Jones 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 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