Advice on type families and non-injectivity?

[Iavor Diatchki]

Hello Conal,

The issue with your example is that it is ambiguous, so GHC can't figure
out how to instantiate the use of `foo`.   It might be easier to see why
this is if you write it in this form:

> foo :: (F a ~ b) => b
> foo = ...

Now, we can see that only `b` appears on the RHS of the `=>`, so there is
really no way for GHC to figure out what is the intended value for `a`.
 Replacing `a` with a concrete type (such as `Bool`) eliminates the
problem, because now GHC does not need to come up with a value for `a`.
Another way to eliminate the ambiguity would be if `F` was injective---then
we'd know that `b` uniquely determines `a` so again there would be no
ambiguity.

If `F` is not injective, however, the only workaround would be to write the
type in such a way that the function arguments appear in the signature
directly (e.g., something like 'a -> F a' would be ok).

-Iavor








On Sun, Jan 13, 2013 at 11:10 AM, 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130113/7d49c8cb/attachment.htm>