Type functions and ambiguity

[Dan Doel]

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