Unfold escaping levels when reading back values

[brendanzab]

This occurs because we are attempting to use ‘glued evaluation’ for local variables, not just top-level definitions. For example we run into a runtime panic when trying to print an error message for the following term:

record {
    Elem = String,
    elem = record {},
} : Record {
    Elem : Type,
    elem : Elem,
}

We'd like to render an error message for record {} which is expected to be of type String. The type we are checking against is:

Value::Unstuck(Head::Local(LocalLevel(0)), [], Value::Stuck(Head::Global("String"), []))

So we'd assume we could render an error like:

error: mismatched types
  ┌─ examples/escaping-local.pi:3:12
  │
3 │     elem = record {},
  │            ^^^^^^^^^ expected `Elem`, found `Record {}`

But instead we actually get an unwrap panic in read_back_spine with Unfold::None because LocalLevel(0) is bound in the record type, but not in record term itself.

To remedy this we now check that the level is valid relative to the environment size, and unfolding if not. This results in the following error message (note that we now render String instead of attempting to render the original binding):

error: mismatched types
  ┌─ examples/escaping-local.pi:3:12
  │
3 │     elem = record {},
  │            ^^^^^^^^^ expected `String`, found `Record {}`

I fear this might be a band-aid solution however. We might need to use fresh ids for local variables in values instead of levels (like in Sixty does), in order to be absolutely sure that we don't accidentally compare variable that originate from different scopes.

[brendanzab]

@AndrasKovacs: not sure if you'd run into anything like this in the past with your work on glued evaluation? @ollef says on #pikelet:matrix.org that he ran up against something similar in sixty, but can't remember why!

[ollef]

Here's the relevant code in Sixty: https://github.com/ollef/sixty/blob/7294718c1287ab0d5d28bd298ad4b70e76d6366b/src/Core/Readback.hs#L33

The reason for doing this, IIRC, is that when you have variables with values you sometimes have to readback a value but without binding that variable. It's something that'd be perfectly fine without gluing locals, but if you allow locals in your glued values they might end up escaping if you don't unfold them during readback as you do here.

[brendanzab]

Yeah, I remember reading that in the sixty source when trying to understand your flavour of gluing, not understanding it, and just going without!

[AndrasKovacs]

This does not look like a problem with local gluing, rather it's about record expression scoping. My solution would be the following. In record {Elem = String, elem = record {}}, I'd allow record {} to refer to Elem as a definition (in general). So checking the expression goes like:

t1 <- check cxt String Type 
t2 <- check (cxt, Elem := t1) (record {}) Elem

So t2 is checked in the context which defines Elem, and the error is also thrown there, where the glued value is clearly valid.

I generally dislike escape checks and fresh name generation. Every term and and value is valid in a specific scope and moving them to larger (weakening) or smaller scopes (strengthening) are specific operations which may or may not be total or happen in constant time. It is essential to be clear about the cost and semantics of weakening and strengthening. Introducing ambiguity or hacks to scoping makes something which is already extremely complex even harder to handle, and certainly less efficient as well.

[ollef]

In my case the escaping definitions came from pattern matching elaboration, because the algorithm I use (https://jesper.sikanda.be/posts/elaborating-dependent-copattern-matching.html) introduces variables that are sometimes neither in the surface term or the core term.

[brendanzab]

Thanks for commenting!

In record {Elem = String, elem = record {}}, I'd allow record {} to refer to Elem as a definition (in general). So checking the expression goes like:

To be honest I'm planning to move to this approach anyway! So this is good news! Like gluing itself, this seems to be useful for users as well as the computer! It also has the appeal of making record terms look more like lambdas, which aids my future goals in other ways. 😉

Just wondering if this would show up for sigma types too - like, often the rules for pairs don't allow the second element to refer to the first element.

[brendanzab]

@ollef Would be possible to let bind the introduced variables in the elaborated core language? Might that help avoid the issue? I'd like to implement that paper too so I'm also interested in any solutions you come up with!

[ollef]

That doesn't sound implausible!

[brendanzab]

Closed by #230, which implements @AndrasKovacs' suggestion. 😃

[brendanzab]

Hmm, I'm actually running into escaping locals in the types of function eliminations as well! This seems to be the source of the bug found in https://github.com/pikelet-lang/pikelet/pull/230#discussion_r502153985. For example, given the following function elimination:

(fun A a => a : Fun (A : Type) -> A -> A) S32

I'd expect to synthesize S32 -> S32. But instead I synthesize the following type:

FunctionType(
    Unstuck(
        Local(LocalLevel(0)),
        [],
        LazyValue(OnceCell(
            Stuck(Global("S32", UniverseOffset(0)), []),
        )),
    ),
    Closure {
        universe_offset: UniverseOffset(0),
        values: Locals[
            Stuck(Global("S32", UniverseOffset(0)), []),
        ],
        term: Local(LocalIndex(1)),
    },
)

Note the escaping level, Local(LocalLevel(0)), in the annotation of the function type. This was bound when I applied the S32 to the ⟨[], A -> A⟩ closure, but is now no longer present!

[brendanzab]

Note that the naive patch-job of an escape check in this PR doesn't actually solve the issue when other bindings are in scope, echoing what Andras was talking about before. For example in the prelude.pi example I get:

error: mismatched types
  ┌─ examples/prelude.pi:7:42
  │
7 │     compose = fun A B C => dep-compose A (always B) (always (always C)),
  │                                          ^^^^^^^^^^ expected `Fun (t : dep-compose) -> Type`, found `Fun (B-1 : Type) -> Fun (t : always) -> Fun (t-1 : dep-compose) -> always`

Here the type of always B is misbound due to local bindings being present in the record term. Ie. the input type points to dep-compose, rather than B.