MiniAgda-0.2014.1.9: test/fail/CheatSubtypingPos.err
MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "CheatSubtypingPos.ma" ---
--- scope checking ---
--- type checking ---
error during typechecking:
MakePos
/// checkExpr 0 |- \ F -> F : (- Set -> Set) -> + Set -> Set
/// checkForced fromList [] |- \ F -> F : (- Set -> Set) -> + Set -> Set
/// new F : (-Set -> Set)
/// checkExpr 1 |- F : + Set -> Set
/// leqVal' (subtyping) -(xSing# : Set) -> < F xSing# : Set > <=+ + Set -> Set
/// subtyping -(xSing# : Set) -> < F xSing# : Set > <=+ + Set -> Set failed