On Monday 09 March 2009 11:56:14 am Simon Peyton-Jones wrote:
For what it's worth, here's why. Suppose we have
type family N a :: *
f :: forall a. N a -> Int f = <blah>
g :: forall b. N b -> Int g x = 1 + f x
The defn of 'g' fails with a very similar error to the one above. Here's why. We instantiate the occurrence of 'f' with an as-yet-unknown type 'alpha', so at the call site 'f' has type N alpha -> Int Now, we know from g's type sig that x :: N b. Since f is applies to x, we must have N alpha ~ N b
I think this explains my confusion. I was thinking roughly in terms like, "I need 'N b -> Int'; I have 'forall a. N a -> Int', so instantiate 'a' to 'b'." Not in terms of collecting constraints and unifying after the fact. From the latter perspective the ambiguity makes sense.
This kind of example encapsulates the biggest single difficulty with using type families in practice. What is worse is that THERE IS NO WORKAROUND.
I suppose one can always add arguments like the "Proxy" to functions to disambiguate, but that certainly isn't ideal.
Anyway I hope this helps clarify the issue.
Yes; thanks. -- Dan