<div dir="ltr">Hi Christian,<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">Given "bar :: Bool", I can't see how one could go from "Bool" to "F a = Bool" and determine "a" uniquely.<br>
</blockquote><div class="gmail_extra"><br></div><div class="gmail_extra">The same question applies to "foo :: Bool", right? Yet no error message there.<br><br></div><div class="gmail_extra">Regards, - Conal<br>
</div>
<div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jan 13, 2013 at 11:36 AM, Christian Höner zu Siederdissen <span dir="ltr"><<a href="mailto:choener@tbi.univie.ac.at" target="_blank">choener@tbi.univie.ac.at</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi,<br>
<br>
How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how<br>
one could go from "Bool" to "F a = Bool" and determine "a" uniquely.<br>
<br>
My question is not completely retorical, if there is an answer I would<br>
like to know it :-)<br>
<br>
Gruss,<br>
Christian<br>
<br>
<br>
* Conal Elliott <<a href="mailto:conal@conal.net">conal@conal.net</a>> [13.01.2013 20:13]:<br>
<div><div class="h5">> I sometimes run into trouble with lack of injectivity for type families.<br>
> I'm trying to understand what's at the heart of these difficulties and<br>
> whether I can avoid them. Also, whether some of the obstacles could be<br>
> overcome with simple improvements to GHC.<br>
><br>
> Here's a simple example:<br>
><br>
> > {-# LANGUAGE TypeFamilies #-}<br>
> ><br>
> > type family F a<br>
> ><br>
> > foo :: F a<br>
> > foo = undefined<br>
> ><br>
> > bar :: F a<br>
> > bar = foo<br>
><br>
> The error message:<br>
><br>
> Couldn't match type `F a' with `F a1'<br>
> NB: `F' is a type function, and may not be injective<br>
> In the expression: foo<br>
> In an equation for `bar': bar = foo<br>
><br>
> A terser (but perhaps subtler) example producing the same error:<br>
><br>
> > baz :: F a<br>
> > baz = baz<br>
><br>
> Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.<br>
><br>
> Does the difficulty here have to do with trying to *infer* the type and<br>
> then compare with the given one? Or is there an issue even with type<br>
> *checking* in such cases?<br>
><br>
> Other insights welcome, as well as suggested work-arounds.<br>
><br>
> I know about (injective) data families but don't want to lose the<br>
> convenience of type synonym families.<br>
><br>
> Thanks, -- Conal<br>
<br>
</div></div>> _______________________________________________<br>
> Glasgow-haskell-users mailing list<br>
> <a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
<br>
</blockquote></div><br></div></div>