loopBadTypesHidden.err

--- opening "loopBadTypesHidden.ma" ---
--- scope checking ---
--- type checking ---
type  SNat : + Size -> Set
term  SNat.zero : .[s!ze : Size] -> .[i < s!ze] -> SNat s!ze
term  SNat.zero : .[i : Size] -> < SNat.zero i : SNat $i >
term  SNat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ SNat i -> SNat s!ze
term  SNat.succ : .[i : Size] -> ^(y1 : SNat i) -> < SNat.succ i y1 : SNat $i >
type  Maybe : ++(A : Set) -> Set
term  Maybe.nothing : .[A : Set] -> < Maybe.nothing : Maybe A >
term  Maybe.just : .[A : Set] -> ^(y0 : A) -> < Maybe.just y0 : Maybe A >
type  Nat : Set
type  Nat = SNat #
term  shift_case : .[i : Size] -> Maybe (SNat $i) -> Maybe (SNat i)
{ shift_case [i] Maybe.nothing = Maybe.nothing
; shift_case [.i] (Maybe.just (SNat.zero [i])) = Maybe.nothing
; shift_case [.i] (Maybe.just (SNat.succ [i] x)) = Maybe.just x
}
term  shift : .[i : Size] -> (Nat -> Maybe (SNat $i)) -> Nat -> Maybe (SNat i)
term  shift = [\ i ->] \ f -> \ n -> shift_case [i] (f (SNat.succ [#] n))
term  inc : Nat -> Maybe Nat
term  inc = \ n -> Maybe.just (SNat.succ [#] n)
type  Unit : Set
term  Unit.unit : < Unit.unit : Unit >
type  loopType : Unit -> Set
{ loopType un!t = .[i : Size] -> SNat i -> (Nat -> Maybe (SNat i)) -> Unit
}
type  loopCaseType : Unit -> Set
{ loopCaseType un!t = .[i : Size] -> (Nat -> Maybe (SNat i)) -> Maybe (SNat i) -> Unit
}
term  loop : (u : Unit) -> loopType u
term  loop_case : (u : Unit) -> loopCaseType u
error during typechecking:
checking type of loop for admissibility
/// new un!t : _
/// new i : _
/// new f : _
/// new i <= #
/// admType: checking ((SNat v3)::Tm -> {(Nat -> Maybe (SNat i)) -> Unit {i = v3, un!t = v0}}) admissible in v3
/// new  : (SNat v3)
/// admType: checking (((SNat #)::Tm -> {Maybe (SNat i) {i = v3, un!t = v0}})::Tm -> {Unit {i = v3, un!t = v0}}) admissible in v3
/// type  SNat # -> Maybe (SNat i)  not lower semi continuous in  i