On 1/13/13 3:52 PM, Iavor Diatchki wrote:
On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott <co...@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
