MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "BadSizeLambdaCoinductive.ma" ---
--- scope checking ---
--- type checking ---
type  S : -(i : Size) -> Set
term  S.inn : .[i : Size] -> ^(out : .[j < i] -> S j) -> < S.inn out : S i >
term  out : .[i : Size] -> (inn : S i) -> .[j < i] -> S j
{ out [i] (S.inn #out) = #out
}
term  eta : .[i : Size] -> (.[j < i] -> S $j) -> S i
{ eta [i] f .out [j < i] = f [j] .out [j]
}
term  cons : .[i : Size] -> (s : S i) -> S $i
term  cons = [\ i ->] \ s -> S.inn ([\ j ->] s)
term  inf : .[i : Size] -> S i
error during typechecking:
inf
/// clause 1
/// right hand side
/// checkExpr 1 |- eta i (\ j -> cons j (inf j)) : S i
/// inferExpr' eta i (\ j -> cons j (inf j))
/// checkApp ((.[j < v0] -> S $j{i = v0})::Tm -> {S i {i = v0}}) eliminated by \ j -> cons j (inf j)
/// checkExpr 1 |- \ j -> cons j (inf j) : .[j < i] -> S $j
/// checkForced fromList [(i,0)] |- \ j -> cons j (inf j) : .[j < i] -> S $j
/// new j < v0
/// adding size rel. v1 + 1 <= v0
/// cannot add hypothesis v1 + 1 <= v0 because it is not satisfyable under all possible valuations of the current hypotheses