[Haskell-cafe] advice on GADT type witnesses needed

[David Roundy]

Hi all,

Jason and I have been working on getting GADT type witnesses into darcs,
and have run into a puzzling error.  For the life of me, I can't see how
this is an actual error, to the point that I'm wondering if it's actually a
bug in ghc.  You can check out the code and reproduce this with

darcs get http://physics.oregonstate.edu/~roundyd/darcs-gadts
cd darcs-gadts
autoconf
./configure --with-type-witnesses
make darcs

At this point ghc will compile for a bit.  It shouldn't get past Viewing,
since we haven't converted over much of the code yet, but it fails
inexplicably on Show.  The error message we get is:

ghc -DPACKAGE_NAME=\"darcs\" -DPACKAGE_TARNAME=\"darcs\" -DPACKAGE_VERSION=\"1.0.9\" -DPACKAGE_STRING=\"darcs\ 1.0.9\" -DPACKAGE_BUGREPORT=\"bugs at darcs.net\" -DSTDC_HEADERS=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_STDLIB_H=1 -DHAVE_STRING_H=1 -DHAVE_MEMORY_H=1 -DHAVE_STRINGS_H=1 -DHAVE_INTTYPES_H=1 -DHAVE_STDINT_H=1 -DHAVE_UNISTD_H=1 -DGADT_WITNESSES=1 -DHAVE_TERMIO_H=1 -cpp  -package regex-compat -package QuickCheck -package mtl -package parsec -package html -package unix -O -funbox-strict-fields  -Wall -Werror -I. -I./src -i./src -DHAVE_CURSES -DHAVE_CURL -c src/Darcs/Patch/Show.lhs

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)


Still, this makes no sense to me.  If any type gurus could help clarify,
that would be great.  Thanks!
-- 
David Roundy
Department of Physics
Oregon State University