MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "UlfsCounterexample.ma" ---
--- scope checking ---
--- type checking ---
type  Bool : Set
term  Bool.true : < Bool.true : Bool >
term  Bool.false : < Bool.false : Bool >
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
type  T : Bool -> Set
{ T Bool.true = Nat
; T Bool.false = Bool
}
term  bad : .[F : Nat -> Set] -> .[f : .[x : Bool] -> T x -> Nat] -> (g : (n : Nat) -> F (f [Bool.true] n)) -> (h : F (f [Bool.false] Bool.false) -> Bool) -> Bool
error during typechecking:
bad
/// clause 1
/// right hand side
/// checkExpr 4 |- h (g zero) : Bool
/// inferExpr' h (g zero)
/// checkApp ((v0 {f [Bool.false] Bool.false {g = (v2 Up ((n : Nat::Tm) -> F (f [Bool.true] n){f = (v1 Up (.[x : Bool::Tm] -> T x -> Nat{F = (v0 Up (Nat::Tm -> Set))})), F = (v0 Up (Nat::Tm -> Set))})), f = (v1 Up (.[x : Bool::Tm] -> T x -> Nat{F = (v0 Up (Nat::Tm -> Set))})), F = (v0 Up (Nat::Tm -> Set))}})::Tm -> {Bool {g = (v2 Up ((n : Nat::Tm) -> F (f [Bool.true] n){f = (v1 Up (.[x : Bool::Tm] -> T x -> Nat{F = (v0 Up (Nat::Tm -> Set))})), F = (v0 Up (Nat::Tm -> Set))})), f = (v1 Up (.[x : Bool::Tm] -> T x -> Nat{F = (v0 Up (Nat::Tm -> Set))})), F = (v0 Up (Nat::Tm -> Set))}}) eliminated by g zero
/// leqVal' (subtyping)  < g n Nat.zero : F (f x  [Bool.true] Nat.zero) >  <=+  F (f x  [Bool.false] Bool.false)
/// leqVal' (subtyping)  F (f x  [Bool.true] Nat.zero)  <=+  F (f x  [Bool.false] Bool.false)
/// leqVal'  f Bool.true Nat.zero  <=*  f Bool.false Bool.false : Nat
/// leqVal'  Nat.zero : Nat  <=*  Bool.false : Bool
/// type Nat has different shape than Bool