[Haskell-cafe] Fw: [darcs-devel] "Inferred type is less
polymorphic than expected" and type witnesses
Ryan Ingram
ryani.spam at gmail.com
Mon Jan 12 15:58:52 EST 2009
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
>> >
>
>
>
More information about the Haskell-Cafe
mailing list