[Haskell-cafe] Fw: [darcs-devel] "Inferred type is less polymorphic than expected" and type witnesses

[Rob Hoelz]

I should've included these when I forwarded it, but that was pre-coffee
today. =P

class MyEq p where
  unsafeCompare :: p C(a b) -> p C(c d) -> Bool
  -- more stuff

data FL a C(x z) where
  (:>:) :: a C(x y) -> FL a C(y z) -> FL a C(x z)
  NilFL :: FL a C(x x)

data (a1 :> a2) C(x y) = FORALL(z) (a1 C(x z)) :> (a2 C(z y))
infixr 1 :>

-- I'm not entirely sure on this one, because type witnesses confuse me.
compare_changes_with_old :: (Patchy p) => 
      FL p C(x y)
   -> FL p C(x y)
   -> (FL p :> FL p) C(x y)

C(args...) is a preprocessor macro that expands to args if Darcs is
building with GADT type witnesses.  FORALL(args...) expands to forall
args. under the same condition.

All of the definitions are available at
http://darcs.net/api-doc/doc-index.html as well.

Thanks,
Rob

"Ryan Ingram" <ryani.spam at gmail.com> wrote:

> Some questions first:
> What's the type of this function supposed to be?
> What's the type of unsafeCompare?
> How is the data type with NilFL and :>: defined?
> 
>   -- ryan
> 
> On Mon, Jan 12, 2009 at 5:43 AM, Rob Hoelz <rob at hoelzro.net> wrote:
> > Forwarding to Haskell Cafe per Eric's suggestion.
> >
> > Begin forwarded message:
> >
> > Date: Sun, 11 Jan 2009 23:01:31 -0600
> > From: Rob Hoelz <rob at hoelzro.net>
> > To: darcs-devel at darcs.net
> > Subject: [darcs-devel] "Inferred type is less polymorphic than
> > expected" and type witnesses
> >
> >
> > Hello again, Darcs users and developers,
> >
> > As I mentioned in my last e-mail, I'm working on
> > http://bugs.darcs.net/issue291.  It's actually gone pretty well,
> > and I feel I'm just about finished (I've done all but sorting out
> > the changes after leaving the editor), only I've encountered the
> > compiler error you see in the subject of this message. This error
> > only appears when compiling with witnesses. Here's the source for
> > the function that it's complaining about:
> >
> > compare_changes_with_old (x :>: xs) (y :>: ys) =
> >  case compare_changes_with_old xs ys of
> >    nx :> ny -> if unsafeCompare x y
> >      then ((x :>: nx) :> ny)
> >      else (NilFL :> (y :>: ys))
> > compare_changes_with_old NilFL NilFL = (NilFL :> NilFL)
> > compare_changes_with_old NilFL ys@(_ :>: _) = (NilFL :> ys)
> > compare_changes_with_old x@(_ :>: _) NilFL = (NilFL :> NilFL)
> >
> > Now, I have two questions:
> >
> > 1) What exactly does this error mean, and how do I get around it?
> > 2) What are witness types, and what are they used for?
> >
> > I will gladly accept links to fine manuals as answers to either
> > question, but simple explanations would be nice. =D  I thought I
> > understood Haskell pretty well, but existentially qualified types
> > have thrown me for a loop.
> >
> > Thanks much,
> > Rob Hoelz
> > _______________________________________________
> > darcs-devel mailing list (AUTOMATIC POSTINGS ONLY PLEASE!)
> > darcs-devel at darcs.net
> > http://lists.osuosl.org/mailman/listinfo/darcs-devel
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >