<div dir="ltr">I sometimes run into trouble with lack of injectivity for type families. I&#39;m trying to understand what&#39;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.<br>

<br>Here&#39;s a simple example:<br><br>&gt; {-# LANGUAGE TypeFamilies #-}<br>&gt;<br>&gt; type family F a<br>&gt;<br>&gt; foo :: F a<br>&gt; foo = undefined<br>&gt;<br>&gt; bar :: F a<br>&gt; bar = foo<br><br>The error message:<br>

<br>    Couldn&#39;t match type `F a&#39; with `F a1&#39;<br>    NB: `F&#39; is a type function, and may not be injective<br>    In the expression: foo<br>    In an equation for `bar&#39;: bar = foo<br><br>A terser (but perhaps subtler) example producing the same error:<br>

<br>&gt; baz :: F a<br>&gt; 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 then compare with the given one? Or is there an issue even with type *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&#39;t want to lose the convenience of type synonym families.<br><br>Thanks,  -- Conal<br><br></div>