MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "IrrHeterogeneousFun.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  good : .[F : Nat -> Set] -> .[f : .[b : Bool] -> (.[T b] -> Nat) -> Nat] -> (g : (n : Nat) -> F (f [Bool.true] ([\ x ->] n))) -> (h : F (f [Bool.false] ([\ x ->] Nat.zero)) -> Bool) -> Bool
{ good [F] [f] g h = h (g Nat.zero)
}
term  good' : .[F : .[b : Bool] -> (.[T b] -> Nat) -> Set] -> (g : F [Bool.false] ([\ x ->] Nat.zero) -> Bool) -> (h : (n : Nat) -> F [Bool.true] ([\ x ->] n)) -> Bool
term  good' = [\ F ->] \ g -> \ h -> g (h Nat.zero)
warning: ignoring error: type Nat has different shape than Bool
term  bad1 : .[F : .[b : Bool] -> (T b -> T b) -> Nat -> Set] -> (g : F [Bool.false] (\ x -> x) Nat.zero -> Bool) -> (h : (n : Nat) -> F [Bool.true] (\ x -> x) n) -> Bool
term  bad1 = [\ F ->] \ g -> \ h -> g (h Nat.zero)
term  f : (b : Bool) -> T b -> T b
{ f Bool.true x = x
; f Bool.false Bool.true = Bool.false
; f Bool.false Bool.false = Bool.true
}
error during typechecking:
bad2
/// checkExpr 0 |- \ F -> \ g -> \ h -> g (h zero) : .[F : .[b : Bool] -> (T b -> T b) -> Nat -> Set] -> (g : F Bool.false (\ x -> f Bool.false x) Nat.zero -> Bool) -> (h : (n : Nat) -> F Bool.true (\ x -> f Bool.true x) n) -> Bool
/// checkForced fromList [] |- \ F -> \ g -> \ h -> g (h zero) : .[F : .[b : Bool] -> (T b -> T b) -> Nat -> Set] -> (g : F Bool.false (\ x -> f Bool.false x) Nat.zero -> Bool) -> (h : (n : Nat) -> F Bool.true (\ x -> f Bool.true x) n) -> Bool
/// new F : (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set)
/// checkExpr 1 |- \ g -> \ h -> g (h zero) : (g : F Bool.false (\ x -> f Bool.false x) Nat.zero -> Bool) -> (h : (n : Nat) -> F Bool.true (\ x -> f Bool.true x) n) -> Bool
/// checkForced fromList [(F,0)] |- \ g -> \ h -> g (h zero) : (g : F Bool.false (\ x -> f Bool.false x) Nat.zero -> Bool) -> (h : (n : Nat) -> F Bool.true (\ x -> f Bool.true x) n) -> Bool
/// new g : ((v0 {Bool.false {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}} {\ x -> f Bool.false x {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}} {Nat.zero {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}})::Tm -> {Bool {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}})
/// checkExpr 2 |- \ h -> g (h zero) : (h : (n : Nat) -> F Bool.true (\ x -> f Bool.true x) n) -> Bool
/// checkForced fromList [(g,1),(F,0)] |- \ h -> g (h zero) : (h : (n : Nat) -> F Bool.true (\ x -> f Bool.true x) n) -> Bool
/// new h : ((n : Nat::Tm) -> F [Bool.true] (\ x -> f Bool.true x) n{g = (v1 Up ((v0 {Bool.false {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}} {\ x -> f Bool.false x {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}} {Nat.zero {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}})::Tm -> {Bool {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}})), F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))})
/// checkExpr 3 |- g (h zero) : Bool
/// inferExpr' g (h zero)
/// checkApp ((v0 {Bool.false {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}} {\ x -> f Bool.false x {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}} {Nat.zero {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}})::Tm -> {Bool {F = (v0 Up (.[b : Bool::Tm] -> (T b -> T b) -> Nat -> Set))}}) eliminated by h zero
/// leqVal' (subtyping)  < h n Nat.zero : F Bool.true (\ x -> f Bool.true x) Nat.zero >  <=+  F Bool.false (\ x -> f Bool.false x) Nat.zero
/// leqVal' (subtyping)  F Bool.true (\ x -> f Bool.true x) Nat.zero  <=+  F Bool.false (\ x -> f Bool.false x) Nat.zero
/// leqVal'  x : Nat -> Nat  <=*  f Bool.false x : Bool -> Bool
/// new x : Nat||Bool
/// leqVal'  x : Nat  <=*  f Bool.false x : Bool
/// type Nat has different shape than Bool