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@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 [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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users