<div dir="ltr">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.<br>
<br>Here's a simple example:<br><br>> {-# LANGUAGE TypeFamilies #-}<br>><br>> type family F a<br>><br>> foo :: F a<br>> foo = undefined<br>><br>> bar :: F a<br>> bar = foo<br><br>The error message:<br>
<br> Couldn't match type `F a' with `F a1'<br> NB: `F' is a type function, and may not be injective<br> In the expression: foo<br> In an equation for `bar': bar = foo<br><br>A terser (but perhaps subtler) example producing the same error:<br>
<br>> baz :: F a<br>> 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't want to lose the convenience of type synonym families.<br><br>Thanks, -- Conal<br><br></div>