[Haskell-cafe] Advice on type families and non-injectivity?

[wren ng thornton]

On 1/13/13 3:52 PM, Iavor Diatchki wrote:
> On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott <conal at conal.net> 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