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