MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "loopBounded.ma" ---
--- scope checking ---
--- type checking ---
type  Empty : Set
type  Unit : Set
term  Unit.unit : < Unit.unit : Unit >
type  Maybe : ++(A : Set) -> Set
term  Maybe.nothing : .[A : Set] -> < Maybe.nothing : Maybe A >
term  Maybe.just : .[A : Set] -> ^(a : A) -> < Maybe.just a : Maybe A >
type  Nat : + Size -> Set
{ Nat i = Maybe (.[j < i] & Nat j)
}
pattern zero = nothing
pattern suc i n = just (i, n)
term  pred : .[i : Size] -> Nat $i -> Nat i
{ pred [i] Maybe.nothing = Maybe.nothing
; pred [i] (Maybe.just ([j < $i], n)) = n
}
term  wfix : .[A : Size -> Set] -> (f : .[i : Size] -> (.[j < i] -> A j) -> A i) -> .[i : Size] -> A i
{ wfix [A] f [i] = f [i] (wfix [A] f)
}
term  fix : .[A : Size -> Set] -> (f : .[i : Size] -> A i -> A $i) -> .[i : Size] -> A i
block fails as expected, error message:
fix
/// clause 1
/// right hand side
/// checkExpr 3 |- f i (fix A f) : A i
/// inferExpr' f i (fix A f)
/// checkApp ((v0 v2)::Tm -> {A $i {i = v2, A = (v0 Up (Size -> Set))}}) eliminated by fix A f
/// leqVal' (subtyping)  .[i : Size] -> < fix [A ] (f i ) i : A i >  <=+  A i
/// leqApp: head mismatch .[i : Size] -> < fix [A ] (f i ) i : A i > != A
type  A : -(i : Size) -> Set
type  A = \ i -> (Nat # -> Nat i) -> Nat #
term  fix : (f : .[i : Size] -> A i -> A $i) -> .[i : Size] -> A i
error during typechecking:
fix
/// clause 1
/// right hand side
/// checkExpr 2 |- f i (fix f i) : (Nat # -> Nat i) -> Nat #
/// inferExpr' f i (fix f i)
/// checkApp ((((Nat #)::Tm -> {Nat i {i = v1}})::Tm -> {Nat # {i = v1}})::Tm -> {A $i {i = v1}}) eliminated by fix f i
/// checkGuard |i| < |i|
/// lexSizes: no descent detected