MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "StreamDupl.ma" ---
--- scope checking ---
--- type checking ---
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  evens : .[A : Set] -> .[i : Size] -> .[j : Size] -> Stream A (i + j) -> Stream A i
error during typechecking:
evens
/// clause 1
/// pattern cons .(i + j + 1) a (cons .(i + j) b as)
/// unifyIndices [(Dec {thePolarity = .}Set::Set,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = *}v0::Tm,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = *}v0::Tm,Dec {thePolarity = ++}),(Dec {thePolarity = *}(Stream v0 v5)::(),Dec {thePolarity = ++})] |- < Stream.cons $.(i + j) a (Stream.cons .(i + j) b as) : Stream A $$.(i + j) > ?<=+ Stream A ($i + j)
/// unifyIndices [(Dec {thePolarity = .}Set::Set,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = *}v0::Tm,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = *}v0::Tm,Dec {thePolarity = ++}),(Dec {thePolarity = *}(Stream v0 v5)::(),Dec {thePolarity = ++})] |- Stream A $$.(i + j) ?<=+ Stream A ($i + j)
/// inst [(Dec {thePolarity = .}Set::Set,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = *}v0::Tm,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = *}v0::Tm,Dec {thePolarity = ++}),(Dec {thePolarity = *}(Stream v0 v5)::(),Dec {thePolarity = ++})] |- $$.(i + j) ?<=- $(i + j) : Size
/// inst [(Dec {thePolarity = .}Set::Set,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = *}v0::Tm,Dec {thePolarity = ++}),(Dec {thePolarity = .}Size::Size,Dec {thePolarity = ++}),(Dec {thePolarity = *}v0::Tm,Dec {thePolarity = ++}),(Dec {thePolarity = *}(Stream v0 v5)::(),Dec {thePolarity = ++})] |- $.(i + j) ?<=- i + j : Size
/// inst: leqVal ($ v5) ?<=- (v2 + v1) : Size failed
/// leqVal'  $.(i + j)  <=-  i + j : Size
/// leSize $.(i + j) <=- i + j
/// leSize' i + j <= $.(i + j)
/// leSize: i + j <= .(i + j) + 1 failed