[Agda] I am failing at Sized types 2.

[Apostolis Xekoukoulotakis]

I was wondering if Andreas or someone else could write down the rules that
determine the typechecking behavior of Sized types. It would be nice if it
pointed to their limitations as well, with simple examples.

I only found some rules at slide 9 of a 2008 presentation.
http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf
(Should size be a parameter or an index?)

At 2011 coinduction subtyping wasn't supported.
https://lists.chalmers.se/pipermail/agda/2011/003127.html

I believe/hope that it does now.

In 2015, Conor was failing at Sized types, an interesting email title for a
professor :)
https://lists.chalmers.se/pipermail/agda/2015/007603.html

in which it is pointed that there are two Sized types' syntaxes, that could
lead into problems.

It would help if someone pointed to possible pitfalls with using Sized
types.

I am having problems with Sized types as well. Most probably, because I do
not understand how they work.

(I have a data type that depends on Sized types that change size from one
constructor to the other of that particular data type. The Sized types have
parts which are coinductive, similarly to the Delay monad from Abel's
paper.)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170112/7deb8e51/attachment.html>