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

On 6/15/07, Ian Lynagh wrote:

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.

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