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