MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "PolarityWrongCast.ma" ---
--- scope checking ---
--- type checking ---
type  DNeg : Set -> + Set -> Set
type  DNeg = \ B -> \ A -> (A -> B) -> B
type  Empty : Set
type  Nat : + Size -> Set
term  Nat.zero : .[s!ze : Size] -> .[i < s!ze] -> Nat s!ze
term  Nat.zero : .[i : Size] -> < Nat.zero i : Nat $i >
term  Nat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ Nat i -> Nat s!ze
term  Nat.succ : .[i : Size] -> ^(y1 : Nat i) -> < Nat.succ i y1 : Nat $i >
type  Id : Nat # -> ++ Set -> Set
{ Id (Nat.zero [.#]) A = A
; Id (Nat.succ [.#] n) A = A
}
error during typechecking:
kast
/// checkExpr 0 |- \ i -> \ n -> \ x -> x : .[i : Size] -> .[n : Nat i] -> Id n (Nat #) -> Id n (Nat i)
/// checkForced fromList [] |- \ i -> \ n -> \ x -> x : .[i : Size] -> .[n : Nat i] -> Id n (Nat #) -> Id n (Nat i)
/// new i <= #
/// checkExpr 1 |- \ n -> \ x -> x : .[n : Nat i] -> Id n (Nat #) -> Id n (Nat i)
/// checkForced fromList [(i,0)] |- \ n -> \ x -> x : .[n : Nat i] -> Id n (Nat #) -> Id n (Nat i)
/// new n : (Nat v0)
/// checkExpr 2 |- \ x -> x : Id n (Nat #) -> Id n (Nat i)
/// checkForced fromList [(n,1),(i,0)] |- \ x -> x : Id n (Nat #) -> Id n (Nat i)
/// new x : (Id v1 {Nat # {n = v1, i = v0}})
/// checkExpr 3 |- x : Id n (Nat i)
/// leqVal' (subtyping)  < x : Id n (Nat #) >  <=+  Id n (Nat i)
/// leqVal' (subtyping)  Id n (Nat #)  <=+  Id n (Nat i)
/// leqVal'  Nat #  <=+  Nat i : Set
/// leqVal'  #  <=+  i : Size
/// leSize # <=+ i
/// leSize' # <= i
/// leSize: # + 0 <= i failed