I'm trying to understand the paper ΠΣ: Dependent Types without the Sugar by implementing an interpreter and type checker for the language. In doing so, I've seen that the
unfold t as x -> u syntax for recursive definitions (syntax is defined in Section 2.1) binds a variable, but I don't see why that's needed. None of the examples in the paper actually use the variable binding -- they all use a shorthand form
unfold t (meaning
unfold t as x -> x).
I do see that the type checking rule for it (from section 5) uses the variable binding, but I don't understand the implications of this. As far as I can tell
unfold t as x -> u is entirely equivalent to
let x = unfold t in u.
Can someone provide an example of when the variable binding is helpful or necessary? Is there some term that type-checks with the long form of
unfold but not with the short form and