Advice on type families and non-injectivity?

Iavor Diatchki iavor.diatchki at
Sun Jan 13 21:52:14 CET 2013


On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott <conal at> 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).

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Glasgow-haskell-users mailing list