[Haskell-cafe] advice on GADT type witnesses needed

David Roundy droundy at darcs.net
Thu Jun 14 21:56:00 EDT 2007

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

    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

More information about the Haskell-Cafe mailing list