loopAdmStream-Nat.err

MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "loopAdmStream-Nat.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
type  Stream : ++(A : Set) -> - Size -> Set
term  Stream.cons : .[A : Set] -> .[i : Size] -> ^(head : A) -> ^(tail : Stream A i) -> < Stream.cons i head tail : Stream A $i >
term  head : .[A : Set] -> .[i : Size] -> (cons : Stream A $i) -> A
{ head [A] [i] (Stream.cons [.i] #head #tail) = #head
}
term  tail : .[A : Set] -> .[i : Size] -> (cons : Stream A $i) -> Stream A i
{ tail [A] [i] (Stream.cons [.i] #head #tail) = #tail
}
term  guard : .[j : Size] -> (Stream Nat $j -> Stream Nat #) -> Stream Nat j -> Stream Nat #
{ guard [j] g xs = g (Stream.cons [j] Nat.zero xs)
}
term  f : .[i : Size] -> (Stream Nat i -> Stream Nat #) -> Stream Nat i
error during typechecking:
f
/// clause 1
/// pattern $j
/// checkPattern $j : matching on size, checking that target .[i : Size] -> (Stream Nat i -> Stream Nat #) -> Stream Nat i ends in correct coinductive sized type
/// new i <= #
/// endsInSizedCo: (Stream Nat i -> Stream Nat #) -> Stream Nat i
/// type  Stream Nat i -> Stream Nat #  not lower semi continuous in  i