# Advice on type families and non-injectivity?

Christian Höner zu Siederdissen choener at tbi.univie.ac.at
Sun Jan 13 20:36:15 CET 2013

```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

> _______________________________________________