Advice on type families and non-injectivity?
J. Garrett Morris
jgmorris at cs.pdx.edu
Mon Jan 14 21:59:20 CET 2013
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.
Sent from my mail client.
More information about the Glasgow-haskell-users