MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "onesStreamUnguarded.ma" ---
--- scope checking ---
--- type checking ---
type  Stream : ++(A : Set) -> - Size -> Set
term  Stream.cons : .[A : Set] -> .[i : Size] -> ^(y1 : A) -> ^(y2 : Stream A i) -> < Stream.cons i y1 y2 : Stream A $i >
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
term  copyFirst : .[i : Size] -> Stream Nat i -> Stream Nat $i
error during typechecking:
copyFirst
/// clause 1
/// pattern $i
/// checkPattern $i : matching on size, checking that target .[i : Size] -> Stream Nat i -> Stream Nat $i ends in correct coinductive sized type
/// new i <= #
/// endsInSizedCo: Stream Nat i -> Stream Nat $i
/// new  : (Stream {Nat {i = v0}} v0)
/// endsInSizedCo: Stream Nat $i
/// endsInSizedCo: target Stream Nat $i of corecursive function is neither a CoSet or codata of size i nor a tuple type