Advice on type families and non-injectivity?

[Conal Elliott]

Hi Christian,

Given "bar :: Bool", I can't see how one could go from "Bool" to "F a =
> Bool" and determine "a" uniquely.
>

The same question applies to "foo :: Bool", right? Yet no error message
there.

Regards, - Conal

On Sun, Jan 13, 2013 at 11:36 AM, Christian Höner zu Siederdissen <
choener at tbi.univie.ac.at> wrote:

> Hi,
>
> How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how
> one could go from "Bool" to "F a = Bool" and determine "a" uniquely.
>
> My question is not completely retorical, if there is an answer I would
> like to know it :-)
>
> Gruss,
> Christian
>
>
> * Conal Elliott <conal at conal.net> [13.01.2013 20:13]:
> >    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/31a65dda/attachment.htm>