MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "UlfsCounterexample2.ma" ---
--- scope checking ---
--- type checking ---
type  Bool : Set
term  Bool.true : < Bool.true : Bool >
term  Bool.false : < Bool.false : Bool >
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
type  T : ^ Bool -> Set
term  T.nat : ^(y0 : Nat) -> < T.nat y0 : T Bool.true >
term  T.bool : ^(y0 : Bool) -> < T.bool y0 : T Bool.false >
term  bad : .[F : Nat -> Set] -> ^(f : .[x : Bool] -> T x -> Nat) -> (g : (n : Nat) -> F (f [Bool.true] (T.nat n))) -> (h : F (f [Bool.false] (T.bool Bool.false)) -> Bool) -> Bool
error during typechecking:
bad
/// clause 1
/// right hand side
/// checkExpr 4 |- h (g zero) : Bool
/// inferExpr' h (g zero)
/// checkApp ((v0 {f [Bool.false] (T.bool Bool.false) {g = (v2 Up ((n : Nat::Tm) -> F (f [Bool.true] (T.nat n)){f = (v1 Up (.[x : Bool::Tm] -> T x -> Nat{F = (v0 Up (Nat::Tm -> Set))})), F = (v0 Up (Nat::Tm -> Set))})), f = (v1 Up (.[x : Bool::Tm] -> T x -> Nat{F = (v0 Up (Nat::Tm -> Set))})), F = (v0 Up (Nat::Tm -> Set))}})::Tm -> {Bool {g = (v2 Up ((n : Nat::Tm) -> F (f [Bool.true] (T.nat n)){f = (v1 Up (.[x : Bool::Tm] -> T x -> Nat{F = (v0 Up (Nat::Tm -> Set))})), F = (v0 Up (Nat::Tm -> Set))})), f = (v1 Up (.[x : Bool::Tm] -> T x -> Nat{F = (v0 Up (Nat::Tm -> Set))})), F = (v0 Up (Nat::Tm -> Set))}}) eliminated by g zero
/// leqVal' (subtyping)  < g n Nat.zero : F (f x  [Bool.true] (T.nat Nat.zero)) >  <=+  F (f x  [Bool.false] (T.bool Bool.false))
/// leqVal' (subtyping)  F (f x  [Bool.true] (T.nat Nat.zero))  <=+  F (f x  [Bool.false] (T.bool Bool.false))
/// leqVal'  f Bool.true (T.nat Nat.zero)  <=*  f Bool.false (T.bool Bool.false) : Nat
/// leqVal'  T.nat Nat.zero : T Bool.true  <=*  T.bool Bool.false : T Bool.false
/// leqVal': head mismatch T.nat{y0 = Nat.zero{}} != T.bool{y0 = Bool.false{}}