> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
