MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "subtyping_erased_wrongdir.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