Hi Iavor, Thanks for the remarks. so there is really no way for GHC to figure out what is the intended value

for `a`.

Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`? -- Conal On Sun, Jan 13, 2013 at 11:39 AM, Iavor Diatchki wrote:

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

On 1/13/13 3:52 PM, Iavor Diatchki wrote:

On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott wrote:

...

...

so there is really no way for GHC to figure out what is the intended value for `a`.

Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`?

Wouldn't that make `F` a constant type family,

I don't see why. If we translate this to dependent type notation we get: ((a::*) -> F a) == ((b::*) -> F b) This equality should hold in virtue of alpha-conversion. What F is, is irrelevant; the only thing that matters is that it has kind *->*. In particular, it doesn't matter whether F is arbitrary, injective, parametric, constant, etc. The problem is that the above isn't the equation GHC sees. GHC sees: F a == F b and it can't infer any correlation between a and b, where one of those is universally quantified in the context (the definition of bar) and the other is something we need to fabricate to hand off to the polymorphic value (the call to foo). Of course, in this particular case it *ought* to be fine, by parametricity in the definition of foo. That is, since we merely need to come up with some b, any b, such that F b is the type we need (namely: F a), the a we have will suffice for that. So if we're explicit about type passing, the following is fine: foo :: forall b. F b bar :: forall a. F a bar = /\a -> foo @a The problem is that while the a is sufficient it's not (in general) necessary. And that's the ambiguity GHC is complaining about. GHC can't see that foo is parametric in b, and therefore that a is as good as any other type. -- Live well, ~wren

Thanks, Jake! This suggestion helped a lot. -- Conal On Sun, Jan 13, 2013 at 1:59 PM, Jake McArthur wrote:

I have a trick that loses a little convenience, but may still be more convenient than data families.

{-# LANGUAGE TypeFamilies #-}

import Data.Tagged

type family F a

foo :: Tagged a (F a) foo = Tagged undefined

bar :: Tagged a (F a) bar = foo

This allows you to use the same newtype wrapper consistently, regardless of what the type instance actually is; one of the inconveniences of data families is the need to use different constructors for different types.

On Sun, Jan 13, 2013 at 2:10 PM, Conal Elliott 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

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe