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

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 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" 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 wrote:

...

Forwarding to Haskell Cafe per Eric's suggestion.

Begin forwarded message:

Date: Sun, 11 Jan 2009 23:01:31 -0600 From: Rob Hoelz To: darcs-devel@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@darcs.net http://lists.osuosl.org/mailman/listinfo/darcs-devel _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe