[Agda] Agda with excluded middle is inconsistent

[Noam Zeilberger]

On Thu, Jan 7, 2010 at 6:17 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> For a pragmatic solution, I suggest to consider the problem of injective
> type constructors in a simply-typed setting and then extrapolate to a
> dependently typed setting.

In SML, as in Agda, datatype *constructors* are injective, type
*definitions* are not.  Here is an example:

type 'a ninja = unit		(* non-injective type definition *)
datatype 'a inja = Foo of unit	(* injective datatype constructor *)

(* bar1 and bar2 restrict the type argument of ninja and inja *)
fun bar1 (_ : bool ninja) = 0
fun bar2 (_ : bool inja) = 0

(* now, t1 will obviously type check... *)
val t1 = bar1 (() : bool ninja)
(* but so will t2, by expanding the definition of "int nina" ... *)
val t2 = bar1 (() : int ninja)

(* likewise, t3 wil obviously type check... *)
val t3 = bar2 (Foo() : bool inja)
(* but t4 does not! *)
val t4  = bar2 (Foo() : int inja)

(* Error: operator and operand don't agree [tycon mismatch]
  operator domain: bool inja
  operand:         int inja
  in expression:
    bar2 (Foo (): int inja) *)