Advice on type families and non-injectivity?

[J. Garrett Morris]

On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> 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.