[Haskell-cafe] Strange type error with associated type synonyms

[Simon Peyton-Jones]

| But the core part of my suggestion (which this example was meant
| to help explain) remains attractive, at least to me: somewhere during
| type inference, GHC *does* unify the *apparently free* 'd' with an
| internal type variable (lets call it 'd1, as in the type error message)

You are speculating about the *algorithm*.  I rather doubt that exposing more of the algorithm to users is going to be helpful; the whole point of a declarative description of the type system is that it specifies which programs are typeable without giving the nitty gritty of an algorithm.

Even I, who implemented GHC's current algorithm, cannot follow your algorithmic explanation.

| that has no explicit counterpart in source code or type signature,
| so the inferred type should not be
|
|         f' :: forall d. (Fun d) => Memo d a -> Memo d a -- (1)
|
| but rather
|
|         f' :: forall d. (Fun d,d~d1) => Memo d a -> Memo d a -- (2)

What is this d1?  Where is it bound?

| All I'm suggesting is that the type *printed* by GHCi does not
| really represent the type *inferred* by GHCi (or else there should
| not be any attempt to match the *free* 'd' against some unknown
| 'd1', as the error message says), and that there might be ways to
| make the discrepancy explicit, by printing the inferred type differently.

I believe that it *does* really represent the type inferred by GHC, in fact.

Simon