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

[Ryan Ingram]

Here's a minimal bit of code that gives you the error:

> data FL p x z where
>     ConsFL :: p x y -> FL p y z -> FL p x z
>     NilFL :: FL p x x
> data GTE a1 a2 x z where
>     GTE :: a1 x y -> a2 y z -> GTE a1 a2 x z

> ccwo (ConsFL x xs) (ConsFL y ys) =
>    case ccwo xs ys of
>        GTE nx ny -> undefined

However, your problem goes further than this; if we add the NilFL
cases, you *need* to understand the type of ccwo and qualify it with a
type signature, or else you get the "GADT pattern match in non-rigid
context" error.  The reason it doesn't show up in this first case is
that ConsFL isn't using all the powers of GADTs; it can be represented
with just existential types.

So, FL p represents an element of the transitive closure of p over
types; that is, if you have

ab :: P A B
ac :: P A C
bd :: P B D
cd :: P C D

then you can get the following FLs:

NilFL :: FL P x x -- for any x
ConsFL ab NilFL :: FL P A B
ConsFL ac NilFL :: FL P A C
ConsFL bd NilFL :: FL P B D
ConsFL cd NilFL :: FL P C D
abd = ConsFL ab (ConsFL bd NilFL) :: FL P A D
acd = ConsFL ac (ConsFL cd NilFL) :: FL P A D

Note the two separate constructions of FL P A D.  This means your
suggested type for ccwo can't work; consider "ccwo abd acd".  The
existentially held type in the first list is "B", and in the second
list is "C".

So, what do you expect compare_changes_with_old to do in this
"diamond" case?  I think if you understand that, you'll be able to
figure out a working definition.

  -- ryan

On Mon, Jan 12, 2009 at 10:21 AM, Rob Hoelz <rob at hoelzro.net> wrote:
> 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
>> >
>
>
>