[Agda] Negative coinductive sized types

[Florian Engel]

Unfortunately, with this type, agda still can't solve the size constraint
in merge.  I suppose this is because the destructor tl gives back a
stream with some size smaller than its input stream, but it don't know
how much smaller.  I think if i could define the stream type like the
following it should work.

   codata Stream (A : Set) : Size → Set where
     hd : Stream A i → A
     tl : Stream A (↑ i) → Stream A i

Is something like that possible?

Nils Anders Danielsson writes:

> On 2020-11-03 21:27, Florian Engel wrote:
>> 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
>
> The following type works:
>
>   {i : Size} {A : Set} → A → Stream i A → Stream (↑ i) A

-------------- 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/20201104/36455a4b/attachment.sig>