Advice on type families and non-injectivity?

[Conal Elliott]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130113/1266ec13/attachment.htm>