MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "subtyping_erased.ma" ---
--- scope checking ---
--- type checking ---
error during typechecking:
id
/// checkExpr 0 |- \ A -> \ x -> x : .[A : Set] -> (.[A] -> A) -> A -> A
/// checkForced fromList [] |- \ A -> \ x -> x : .[A : Set] -> (.[A] -> A) -> A -> A
/// new A : Set
/// checkExpr 1 |- \ x -> x : (.[A] -> A) -> A -> A
/// checkForced fromList [(A,0)] |- \ x -> x : (.[A] -> A) -> A -> A
/// new x : (.[v0::Tm] -> {A {A = v0}})
/// checkExpr 2 |- x : A -> A
/// leqVal' (subtyping)  .[xSing# : A] -> < x xSing# : A >  <=+  A -> A
/// subtyping .[xSing# : A] -> < x xSing# : A >  <=+  A -> A failed