Hi, How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how one could go from "Bool" to "F a = Bool" and determine "a" uniquely.
My question is not completely retorical, if there is an answer I would
like to know it :-)
Gruss,
Christian
* Conal Elliott <co...@conal.net> [13.01.2013 20:13]:
> I sometimes run into trouble with lack of injectivity for type families.
> I'm trying to understand what's at the heart of these difficulties and
> whether I can avoid them. Also, whether some of the obstacles could be
> overcome with simple improvements to GHC.
>
> Here's a simple example:
>
> > {-# LANGUAGE TypeFamilies #-}
> >
> > type family F a
> >
> > foo :: F a
> > foo = undefined
> >
> > bar :: F a
> > bar = foo
>
> The error message:
>
> Couldn't match type `F a' with `F a1'
> NB: `F' is a type function, and may not be injective
> In the expression: foo
> In an equation for `bar': bar = foo
>
> A terser (but perhaps subtler) example producing the same error:
>
> > baz :: F a
> > baz = baz
>
> Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
>
> Does the difficulty here have to do with trying to *infer* the type and
> then compare with the given one? Or is there an issue even with type
> *checking* in such cases?
>
> Other insights welcome, as well as suggested work-arounds.
>
> I know about (injective) data families but don't want to lose the
> convenience of type synonym families.
>
> Thanks, -- Conal
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
pgpDSTt_twtD7.pgp
Description: PGP signature
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
