<div dir="ltr"><div><div><div><div><div><div><div>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.<br><br></div>I only found some rules at slide 9 of a 2008 presentation.<br><a href="http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf">http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf</a><br></div><div>(Should size be a parameter or an index?)<br></div><div><br></div>At 2011 coinduction subtyping wasn't supported. <br><a href="https://lists.chalmers.se/pipermail/agda/2011/003127.html">https://lists.chalmers.se/pipermail/agda/2011/003127.html</a><br><br>I believe/hope that it does now.<br><br></div>In 2015, Conor was failing at Sized types, an interesting email title for a professor :)<br><a href="https://lists.chalmers.se/pipermail/agda/2015/007603.html">https://lists.chalmers.se/pipermail/agda/2015/007603.html</a><br><br></div>in which it is pointed that there are two Sized types' syntaxes, that could lead into problems.<br><br></div>It would help if someone pointed to possible pitfalls with using Sized types.<br><br></div>I am having problems with Sized types as well. Most probably, because I do not understand how they work.<br><br></div>(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.)<br></div>