MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "D.ma" ---
--- scope checking ---
--- type checking ---
type  D : Set
term  D.abs : ^(y0 : ^ D -> D) -> < D.abs y0 : D >
warning: ignoring error: polarity check ++ <= - failed
warning: ignoring error: polarity check ++ <= + failed
term  app : D -> ^ D -> D
{ app (D.abs f) d = f d
}
term  sapp : D -> D
{ sapp x = app x x
}
error during typechecking:
delta
/// checkExpr 0 |- abs (\ x -> sapp x) : D
/// checkForced fromList [] |- abs (\ x -> sapp x) : D
/// checkApp (^(y0 : (^D::() -> D)::()) -> < D.abs y0 : D >) eliminated by \ x -> sapp x
/// checkExpr 0 |- \ x -> sapp x : ^ D -> D
/// checkForced fromList [] |- \ x -> sapp x : ^ D -> D
/// new x : D
/// checkExpr 1 |- sapp x : D
/// inferExpr' sapp x
/// checkApp (D::Tm -> D) eliminated by x
/// inferExpr' x
/// inferExpr: variable x : D may not occur
/// , because of polarity
/// polarity check ^ <= * failed