[Agda] Agda with excluded middle is inconsistent

[Nils Anders Danielsson]

On 2010-01-07 11:30, Thorsten Altenkirch wrote:
> congratulations! I didn't know about this problem and I think it is a
> serious issue indeed.

I agree.

> Maybe it is a known issue? Nisse? Ulf?

I don't think so, but there was some scepticism when injectivity of type
constructors was introduced. See the following thread:

 heterogeneous equality
 https://lists.chalmers.se/pipermail/agda/2008/000153.html

I wanted to see how often I have used this feature, so I reverted the
change Ulf mentions in that thread. It turned out that I only had to
modify two functions to make the 168 files of the standard library type
check. If reverting this change really is all that is needed to remove
automatic type constructor injectivity (Ulf?), then I suggest that we
make this feature optional, or remove it entirely.

--
/NAD