<div dir="ltr"><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"></span>The only problem I can spot is that szx is <i>not</i> strictly smaller than<span class="gmail_default" style="font-family:arial,helvetica,sans-serif"> max(szf + 1, szx), so the size of the type of app has to be either ↑ (szf ⊔ˢ szx) or ↑ szf ⊔ˢ <span class="gmail_default" style="font-family:arial,helvetica,sans-serif">↑ </span>szx. But even then, with the app case of ⟦_⟧t having either of these sizes, it still doesn't pass the termination check, so I'm not sure what's going there, because I'm pretty confident that szf and szx are both strictly smaller than <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"> ↑ (szf ⊔ˢ szx) and <span class="gmail_default" style="font-family:arial,helvetica,sans-serif">↑ szf ⊔ˢ <span class="gmail_default" style="font-family:arial,helvetica,sans-serif">↑ </span>szx.</span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">It could just be that this isn't something that the size checker can verify. If you pick the first version — that is,<br></span></span></span></div><div><span style="font-family:monospace"><span class="gmail_default"><span class="gmail_default"><span class="gmail_default"><br></span></span></span></span></div><div><span style="font-family:monospace"><span class="gmail_default"><span class="gmail_default"><span class="gmail_default">data Neutral where<br>  var : ∀ {i : Size} {Γ T} → T ∈ Γ → Neutral i Γ T<br>  app : ∀ {szf szx : Size} {Γ S T} → Neutral szf Γ (S ⇒ T) → Value szx Γ S → Neutral (↑ (szf ⊔ˢ szx)) Γ T</span></span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">Then you could "raise" the size of the recursive arguments of <span class="gmail_default" style="font-family:arial,helvetica,sans-serif">⟦_⟧t </span>from szf and szx both to <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">(szf ⊔ˢ szx), so that the app branch is</span></span></span></span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></span></span></span></span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span style="font-family:monospace">⟦_⟧t .{↑ (szf ⊔ˢ szx)} (coerce (app {szf} {szx} f x)) ctx = ⟦_⟧t {szf ⊔ˢ szx} (coerce f) ctx (⟦_⟧t {szf ⊔ˢ szx} x ctx)</span><br></span></span></span></span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></span></span></span></span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">I don't remember if Agda has sized subtyping (I mean, probably, given that this passes termination checking), but for instance (coerce f) has type (Value szf Γ T), which would need to be a subtype of (Value (<span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">szf ⊔ˢ szx) <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"> Γ T), which follows from (szf ≤ <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">szf ⊔ˢ szx), and finally (<span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">szf ⊔ˢ szx ≤ ↑ <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">(szf ⊔ˢ szx)) for termination checking</span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span>.</span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></div><div><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">The original version without the trick just needs (szf ≤ <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">↑ <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">(szf ⊔ˢ szx)) and (szx ≤ <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">↑ <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">(szf ⊔ˢ szx)) though, which holds by transitivity. Is Agda unable to check transitive subsizing relations like that?<br></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></div><br>On Mon, 23 Aug 2021 at 21:07, James Smith <<a href="mailto:james.smith.69781@gmail.com">james.smith.69781@gmail.com</a>> wrote:<br>><br>> I'm trying to learn to use Sized Types to solve a simple non-termination issue. After reading a couple papers (MiniAgda, Equational Reasoning about Formal Languages in Coalgebraic Style) and everything I could find online, I was still confused. I've found a solution that works, but I don't know why my first attempt didn't work. Would love to learn the insight I am missing.<br>><br>> A small lambda toy with separate neutrals and values:<br>><br>>     data Type : Set where<br>>       Nat : Type<br>>       _⇒_ : Type → Type → Type<br>>    <br>>     data Value : List Type → Type → Set<br>>     data Neutral : List Type → Type → Set where<br>>       var : ∀ {Γ T} → T ∈ Γ → Neutral Γ T<br>>       app : ∀ {Γ S T} → Neutral Γ (S ⇒ T) → Value Γ S → Neutral Γ T<br>>  <br>>     data Value where<br>>       coerce : ∀ {Γ T} → Neutral Γ T → Value Γ T<br>>  <br>>     ⟦_⟧T : Type → Set<br>>     ⟦ Nat ⟧T = ℕ<br>>     ⟦ S ⇒ T ⟧T = ⟦ S ⟧T → ⟦ T ⟧T<br>>  <br>>     ⟦_⟧C : List Type → Set<br>>     ⟦_⟧C = Data.List.foldr _×_ ⊤ ∘ Data.List.map ⟦_⟧T<br>>  <br>>     {-# NON_TERMINATING #-}<br>>     ⟦_⟧t : ∀ {Γ T} → Value Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T<br>>     ⟦ (coerce (var (here px))) ⟧t  (fst , _) rewrite px = fst<br>>     ⟦ (coerce (var (there x))) ⟧t  (_ , rest) = ⟦ (coerce (var x)) ⟧t rest<br>>     ⟦ (coerce (app f x)) ⟧t  ctx = (⟦ coerce f ⟧t ctx) (⟦ x ⟧t ctx)<br>><br>> The final app clause is what causes a problem. A mutually recursive function pair works fine:<br>><br>>     ⟦_⟧t-v : ∀ {Γ T} → Value Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T<br>>     ⟦_⟧t-n : ∀ {Γ T} → Neutral Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T<br>>     ⟦ (coerce n) ⟧t-v env = ⟦ n ⟧t-n env<br>>     ⟦ (var (here px)) ⟧t-n  (fst , _) rewrite px = fst<br>>     ⟦ (var (there x)) ⟧t-n  (_ , rest) = ⟦ var x ⟧t-n rest<br>>     ⟦ (app f x) ⟧t-n  ctx = (⟦ f ⟧t-n ctx) (⟦ x ⟧t-v ctx)  <br>><br>> But I want the excuse to learn how to apply Sized Types, so I take a crack at getting rid of NON_TERMINATING by threading a Size index through everything.<br>><br>>   module SizedExample where<br>>     open import Data.Nat<br>>     open import Data.List<br>>     open import Data.List.Membership.Propositional<br>>     open import Data.List.Membership.Propositional.Properties<br>>     open import Data.List.Relation.Unary.Any<br>>     open import Data.Product<br>>     open import Data.Unit<br>>     open import Data.Vec<br>>     open import Function<br>>     open import Relation.Binary.PropositionalEquality<br>>     open import Size<br>>  <br>>     data Type : Set where<br>>       Nat : Type<br>>       _⇒_ : Type → Type → Type<br>>    <br>>     data Value : Size → List Type → Type → Set<br>>     data Neutral : Size → List Type → Type → Set<br>><br>>     data Neutral where<br>>       var : ∀ {i : Size} {Γ T} → T ∈ Γ → Neutral i Γ T<br>>       app : ∀ {szf szx : Size} {Γ S T} → Neutral szf Γ (S ⇒ T) → Value szx Γ S → Neutral ((↑ szf) ⊔ˢ szx) Γ T<br>>  <br>>     data Value where<br>>       coerce : ∀ {sz : Size} {Γ T} → Neutral sz Γ T → Value sz Γ T<br>>  <br>>     ⟦_⟧T : Type → Set<br>>     ⟦ Nat ⟧T = ℕ<br>>     ⟦ S ⇒ T ⟧T = ⟦ S ⟧T → ⟦ T ⟧T<br>>  <br>>     ⟦_⟧C : List Type → Set<br>>     ⟦_⟧C = Data.List.foldr _×_ ⊤ ∘ Data.List.map ⟦_⟧T<br>><br>>     ⟦_⟧t : ∀ {sz Γ T} → Value sz Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T<br>>     ⟦ (coerce (var (here px))) ⟧t (fst , _) rewrite px = fst<br>>     ⟦ (coerce (var (there x))) ⟧t (_ , rest) = ⟦ (coerce (var x)) ⟧t rest<br>>     ⟦_⟧t .{(↑ szf) ⊔ˢ szx} (coerce (app {szf} {szx} f x)) ctx = ⟦_⟧t {szf} (coerce f) ctx (⟦_⟧t {szx} x ctx)  <br>>   <br>> The termination checker rejects the last line. But I don't see why. It looks to me like there's enough information there to see szf and szx are each smaller than their max to let those calls go through. I also tried giving extra headroom for szf in case that helped, but that didn't work either.<br>><br>> A refactor to use Size< on parameters, instead of the max operator on the result, works: <br>><br>> module SizedExample2 where<br>>     open import Data.Nat<br>>     open import Data.List<br>>     open import Data.List.Membership.Propositional<br>>     open import Data.List.Membership.Propositional.Properties<br>>     open import Data.List.Relation.Unary.Any<br>>     open import Data.Product<br>>     open import Data.Unit<br>>     open import Data.Vec<br>>     open import Function<br>>     open import Relation.Binary.PropositionalEquality<br>>     open import Size<br>>  <br>>     data Type : Set where<br>>       Nat : Type<br>>       _⇒_ : Type → Type → Type<br>>    <br>>     data Value : Size → List Type → Type → Set<br>>     data Neutral : Size → List Type → Type → Set<br>><br>>     data Neutral where<br>>       var : ∀ {sz Γ T} → T ∈ Γ → Neutral sz Γ T<br>>       app : ∀ {sz} {szf szx : Size< sz} {Γ S T} → Neutral szf Γ (S ⇒ T) → Value szx Γ S → Neutral sz Γ T<br>>  <br>>     data Value where<br>>       coerce : ∀ {sz Γ T} → Neutral sz Γ T → Value sz Γ T<br>>  <br>>     ⟦_⟧T : Type → Set<br>>     ⟦ Nat ⟧T = ℕ<br>>     ⟦ S ⇒ T ⟧T = ⟦ S ⟧T → ⟦ T ⟧T<br>>  <br>>     ⟦_⟧C : List Type → Set<br>>     ⟦_⟧C = Data.List.foldr _×_ ⊤ ∘ Data.List.map ⟦_⟧T<br>><br>>     ⟦_⟧t : ∀ {sz Γ T} → Value sz Γ T → ⟦ Γ ⟧C → ⟦ T ⟧T<br>>     ⟦ (coerce (var (here px))) ⟧t (fst , _) rewrite px = fst<br>>     ⟦ (coerce (var (there x))) ⟧t (_ , rest) = ⟦ (coerce (var x)) ⟧t rest<br>>     ⟦_⟧t (coerce (app f x)) ctx = ⟦ (coerce f) ⟧t ctx (⟦ x ⟧t ctx)<br>><br>><br>> That makes me suspicious this is like a Size version of needing to avoid computed values in the result position of constructors, but I'm not really sure why the version with the max operator didn't work.<br>><br>> Thanks in advance for any insight.<br>><br>> -James<br>><br>><br>> _______________________________________________<br>> Agda mailing list<br>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>> <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></div>