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

[Ian Lynagh]

On Thu, Jun 14, 2007 at 08:27:36PM -0700, Jason Dagit wrote:
> On 6/14/07, David Roundy <droundy at darcs.net> 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