Advice on type families and non-injectivity?

[Christian Höner zu Siederdissen]

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 <conal at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130113/5e80c446/attachment-0001.pgp>