[Haskell-cafe] Re: Non-termination of type-checking

[Stefan Monnier]

> And I'm pretty sure that there's no way to convince Agda that F = R,
> or  something similar, because, despite the fact that Agda has
> injective type  constructors like GHC (R x = R y => x = y), it doesn't
> let you make the  inference R Unit = F Unit => R = F. Of course, in
> Agda, one could arguably say that it's true, because Agda has no type
> case, so there's (I'm pretty sure) no  way to write an F such that
> R T = F T, but R U /= F U, for some U /= T.

It's easy to construct an F that is different from R but agrees with
R for the case of Unit: F = λ _ -> R Unit
So there's a good reason why Agda doesn't let F and R unify: it would
really be completely wrong.


        Stefan