MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "inconsistentAssumption.ma" ---
--- scope checking ---
--- type checking ---
type  SNat : + Size -> Set
term  SNat.zero : .[s!ze : Size] -> .[i < s!ze] -> SNat s!ze
term  SNat.zero : .[i : Size] -> < SNat.zero i : SNat $i >
term  SNat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ SNat i -> SNat s!ze
term  SNat.succ : .[i : Size] -> ^(y1 : SNat i) -> < SNat.succ i y1 : SNat $i >
type  Eq : ^(A : Set) -> ^(a : A) -> ^ A -> Set
term  Eq.refl : .[A : Set] -> .[a : A] -> < Eq.refl : Eq A a a >
term  subst : .[A : Set] -> .[P : A -> Set] -> (i : A) -> (j : A) -> Eq A i j -> P i -> P j
{ subst [A] [P] i .i Eq.refl p = p
}
error during typechecking:
type of h
/// not a type: (ass : (i : Size) -> Eq Size $i i) -> (i : Size) -> SNat i -> SNat #
/// inferExpr' (ass : (i : Size) -> Eq Size $i i) -> (i : Size) -> SNat i -> SNat #
/// inferExpr' (i : Size) -> Eq Size $i i
/// new i <= #
/// inferExpr' Eq Size $i i
/// inferExpr' Eq Size $i
/// inferExpr' Eq Size
/// checkApp (^(A : Set) -> ^(a : A) -> ^ A -> Set) eliminated by Size
/// leqVal' (subtyping)  < Size : TSize >  <=+  Set
/// leqVal' (subtyping)  TSize  <=+  Set
/// universe test TSize <= Set failed