Uh oh. I just realized I can get non-prenex size abstractions just by wrapping polymorphic sized types in pairs
f: (∀α. τ1) → τ2
f': (∀α. τ1) × ⊤ → τ2
I need pairs to be able to hold size-abstracted functions though because closure-conversion wraps around let-bound possibly sized-abstracted functions. I only meant for prenex sized types to simplify typing so hopefully this doesn't cause any real trouble
I mean Agda basically treats Size like its own special size, so if they can do that, surely I can do this
A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.