Type functions and ambiguity
dan.doel at gmail.com
Mon Mar 9 12:46:01 EDT 2009
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.
More information about the Glasgow-haskell-users