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

[Jason Dagit]

On 6/15/07, Ian Lynagh <igloo at earth.li> wrote:
> 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.

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