[Agda] Negative coinductive sized types

[Florian Engel]

Hi all,

I'm trying to implement the ham function from [1]

This is how far I've get so far

  record Stream (i : Size) (A : Set) : Set where
    coinductive
    field
      hd : A
      tl : ∀ {j : Size< i} → Stream j A
  open Stream

  cons : {i : Size} {j : Size< i} {A : Set} → A -> Stream i A → Stream j A
  hd (cons x _)  = x
  tl (cons _ xs) = xs

  leq : {C : Set} → ℕ ∞ → ℕ ∞ → C → C → C
  leq zero    _       t _ = t
  leq (suc x) zero    _ f = f
  leq (suc x) (suc y) t f = leq x y t f

  merge : {i : Size} → Stream i (ℕ ∞) → Stream i (ℕ ∞) → Stream i (ℕ ∞)
  hd (merge xs ys) = min (hd xs) (hd ys)
  tl (merge xs ys) = leq (hd xs) (hd ys)
                         (cons (hd ys) (merge (tl xs) (tl ys)))
                         (cons (hd xs) (merge (tl xs) (tl ys)))

agda cannot solve the size constraints for merge in the tl case because
the output depth of cons is smaller than the input.  I don't understand
why i can't give cons the type

  cons : {i : Size} {j : Size< i} {A : Set} → A -> Stream j A → Stream i A

Shouldn't the minimal depth of the output be larger than the input?

Best regards
Florian

[1] https://www.researchgate.net/publication/220485445_MiniAgda_Integrating_Sized_and_Dependent_Types
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 487 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201103/bcaceb44/attachment.sig>