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

[Jason Dagit]

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

For anyone reading along and not understanding our use of C(x,y),
that's a c pre-processor macro we've defined in gadts.h.  The C stands
for context.  In the case of the patches above, we're annotating the
type with the context for the patch; x for the context required by the
patch and y for the context after applying the patch.  The reason we
use a macro is so that we can incrementally make this modification to
the code and easily disable it at compile time since it doesn't work
everywhere yet.

Thanks,
Jason