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 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
