Advice on type families and non-injectivity?

[Iavor Diatchki]

Hello,


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, and so one could just skip
the `a` parameter?   Anyway, if there was a way to assert something like
that about a type-function, than there would be no problem.   When
something like that happens (i.e., GHC figures out that it does not know
how to instantiate a type variable, but it is sure that the actual
instantiation does not matter), GHC instantiates the variable a special
type called `Any`, which has a very polymorphic kind.

By the way, Simon recently reworked the ambiguity checker in GHC, and now
HEAD correctly rejects `foo` as being ambiguous (the new ambiguity check
uses exactly what's in your example: a value `f :: S` is ambiguous, if `g
:: S; g = f` results in an error).

-Iavor
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130113/dc678992/attachment-0001.htm>