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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users