Advice on type families and non-injectivity?

J. Garrett Morris jgmorris at
Mon Jan 14 21:59:20 CET 2013

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


Sent from my mail client.

More information about the Glasgow-haskell-users mailing list