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 <r...@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.s...@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 <r...@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 <r...@hoelzro.net> >> > To: darcs-de...@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-de...@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 >> > > > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe