[Agda] Negative coinductive sized types

[Nils Anders Danielsson]

On 2020-11-04 19:29, Florian Engel wrote:
> Unfortunately, with this type, agda still can't solve the size constraint
> in merge.

Your code is not self-contained, but I suspect that you can fix your
problem by giving cons the following type signature:

   {i : Size} {A : Set} → A → Stream i A → Stream i A

-- 
/NAD