Advice on type families and non-injectivity?

[Richard Eisenberg]

Hi Conal,

I agree that your initial example is a little puzzling, and I'm glad that the new ambiguity checker prevents both definitions, not just one.

However, your initial question seems broader than just this example. I have run into this problem (wanting injective type functions) several times myself, and have been successful at finding workarounds. But, I can't think of any unifying principle or solid advice. If you can post more information about your problem, perhaps I or others can contribute.

For what it's worth, the desire for injective type functions has been entered as ticket #6018 in the GHC Trac, but I see you're already on the cc: list. I believe Simon PJ has given serious thought to implementing this feature and may have even put in some very basic code toward this end.

Richard

On Jan 13, 2013, at 2:10 PM, Conal Elliott <conal at conal.net> wrote:

> 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
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users