On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones
There is a real difficulty here with type-checking 'bar'. (And that difficulty is why 'foo' is also rejected.)
This seems, to me, like a somewhat round-about way to express the problem. Iavor's explanation (which approach I have also found useful to explain the behavior of type functions in the past) captures the ambiguity in both descriptions:
foo :: (T a ~ b) => b foo = undefined
That this is ambiguous should be obvious. Accepting such a definition could presumably be used to generate values of undefined type; for example, I could get a generic instance
foo :: T Int
whether or not T Int is defined in my program! This also, to me, seems to make it clear that past GHC's acceptance of foo was in error. /g -- Sent from my mail client.