[ elab ] Make `%runElab` expressions have unrestricted quantity

[buzden]

According to #1436, we can't have a runtime-values of types like forall a. List a -> Nat. But consider we need to pass a list of types including one like above to an elaboration script. Now we don't have such an ability. This PR enables it.

Anyway, elaboration scripts work during compilation, why not them to have an access to erased values?

[buzden]

What happens if you write an elab script that returns \x => x at type (0 _ : a) -> a? Are you able to use it to implement

escape : (0 _ : a) -> a
escape = %runElab myscript

?

No! I've changed rig of input of %runElab, not of its result.

---

This code

escScr : Elab $ (0 _ : a) -> a
escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x)

esc : (0 _ : a) -> a
esc = %runElab escScr

expectedly gives an error:

Error: While processing right hand side of esc. x is not accessible in this context.

RunElab0:19:65--19:66
 17 |
 18 | escScr : Elab $ (0 _ : a) -> a
 19 | escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x)
                                                                      ^

And even declaration like

escDecl : Name -> Elab Unit
escDecl name = declare [                                              
                 IDef EmptyFC name [                   
                   PatClause EmptyFC
                     -- lhs
                     (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x"))
                     -- rhs
                     `(x)
                 ]  
               ] 

%runElab escDecl `{esc}

expectedly fails with

Error: While processing right hand side of esc. x is not accessible in this context.

RunElab0:31:24--31:25
 27 |                    PatClause EmptyFC
 28 |                      -- lhs
 29 |                      (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x"))
 30 |                      -- rhs
 31 |                      `(x)
                             ^

while expectedly typechecking for

0 esc' : (0 _ : a) -> a

%runElab escDecl `{esc'}

I can add those above as an additional test case.

[buzden]

I disagree that bringing erased values to non-erased context should be impossible for elaboration scripts. Moreover, they should sometimes do this in some sence: consider an elaboration script for derivation of default Show implementations: it brings constructor names to runtime, this is bringing erased (in some sence) values to the runtime.

That's why I think your test that expects "escaping" to fail, should not pass. The fact that it passes looks like a bug to me. Moreover, I ran into similar bug when during quoting instead of passed value a part of elaboration script was quoted. But for now I didn't manage to make a minimal example showing this for reporting as an issue. This bug seems to appear when %runElab is used for expressions and does not appear when it's used for declarations.

Anyway, this bug is irrelevant to this PR.

[andrevidela]

@buzden I'm not sure what you are replying to but I think I can bring in some intuition about what is happening with erased quantities. Especially your statement

bringing erased values to non-erased context should be [allowed] for elaboration scripts.

erased means the value never appears at runtime, that also means that it should be allowed to be used at compile-time just fine. Since elaborator scripts are executing at compile time it feels natural to expect them to have access to erased multiplicity values. However, the values they have access to cannot be part of computations that appear at runtime. Think of the following example:

0 erased : String
erased = "Ikari"

computeOrder: String -> String
computeOrder = "Get in the robot " ++

main : IO ()
main = putStrLn (computerOrder erased)

you wouldn't expect this program to typecheck, but you would expect the following to work

main : IO ()
main = putStrLn (computerOrder "Shinji")

The only difference between those two programs is that we have inlined the call to erased in the second one. How is this related to elaboration? it's because this kind of operation can be done with elaborator reflection since it just takes a tree and returns another tree. This puts us in either of two positions:

• The program transformation from the first program to the second one is legal, elaboration should have access to erased values, and the linearity checker is wrong to make n inaccessible
• The program transformation is incorrect, elaboration should not have access to erased values, linearity checker is correct to avoid leaking erased values

Like every complex issue, the real answer is "it depends", what this tree operation represents is "a program that is executable at compile type but might result in a different runtime representation". Because the runtime representation is changed the multiplicty cannot be 0 but because it's accessible exclusively at compile-time, it should be allowed to be 0-ish. So we are looking at a different kind of resource tracking if we want to make this property explicit, one that can describe "compile-time only" operations but can have an effect on the runtime.

TBD if something like that ever shows up (I'm working on it but I have also lots of other things going on :)). In the meantime, making n inaccessible makes it consistent with the rest of the design around quantities, that is: erased values never leak into the runtime

PS: If you want the explanation without runtime/compile time intuition, page 3 of the QTT paper, the App rule makes it clear that you can never have anything be 0 and not have either the function be marked as 0 or it's argument be marked as 0 due to σ ′ = 0 ⇔ (π = 0 ∨ σ = 0)

[buzden]

@andrevidela Thank you for the detailed elaboration on this. Let me just clarify that my original sentence had the meaning that I personally agree with the first position you list, i.e. I personally think that

• The program transformation from the first program to the second one is legal, elaboration should have access to erased values, and the linearity checker is wrong to make n inaccessible

Now I see that there is another opinion, it was not obvious. I thought of erased values not as those which are prohibited to be at runtime, but as those which by default are not present at runtime (but could if something forces this).

After your brought both options explicitly, I've thought that maybe we need two kinds of elaboration scripts, of "safe" and "unsafe" flavours, one being unable to bring erased values to runtime, the other being able to do so. The problem is amplified by the fact that elaboration scripts can produce values that are meant to be present only at runtime, as it's shown in #2088.

My mistake was to start this discussion in this PR because this PR does not change what is accessed to elaboration script during %runElab. This PR only makes us able to have elaboration script values to be erased.

[gallais]

I think this change blurs / is due to a blurring of the line between erased values and staging. I'm not comfortable making a decision on this. I guess we could ask @edwinb to weigh in.

[andrevidela]

Sorry for the late reply, in my experience with QTT and different semantics for quantity semirings there is a clear distinction between staging semantics and use semantics. It is true that the waters are muddied for things like elaborator reflection but what this indicates is that more research is needed in order to make things work correctly.

@buzden I suggest we talk about this on discord, I have a lot of work in progress in this area and we can probably find a middle ground between what we need to provide as a toolkit and what is an acceptable feature in terms of type safety

[gallais]

Okay I think I have come around to this. Particularly because quote already has type:

quote : (0 _ : val) -> m TTImp

Once the merge conflict has fixed I am happy to merge it.

[gallais]

I tried to fix the evaluation issue we are getting in elab-util but could not find the issue. :/

[buzden]

but could not find the issue. :/

What do you mean? Do you mean you didn't find the cause?

A couple of experiments from me: I changed existing bot to top in ProcessRunElab and it suddenly did not change anything (the original cause was changing ElabMode from InExpr to InType, but it seems that the reason is different anyway).

Then I added every namespace from allImported to nestedNS like here and suddenly errors changed: the original script that did not reduce to Elab did this, but after that I had the following errors (I haven't worked them out yet).

[gallais]

Sorry, my wording was poor: I could not find a fix for the build issue.

[buzden]

Fresh news! I found out that this non-reducing behaviour happens only in failing block and only when quantity is omega (i.e., it works not only for 0, but for 1 too). @gallais, as an author of the failing block checks, can this information give you any clue on what's going on?

~~Oh, and I added a shorter test that shows the strange behaviour of elab-util failing as reflection022. UPD: sorry, reflection022 is not very correct yet (it reveals another bug), I need to rework it a bit. But information above is still valid.~~

[gallais]

Very interesting. The main code for the typechecking phase is in processFailing in TTImp.ProcessDecls.

Could it be that a hole was delayed and we hit it in checkDelayedHoles? Should we instead try to rerun the delayed problems in case they're now solvable?

[buzden]

Could it be that a hole was delayed and we hit it in checkDelayedHoles?

Once I allowed typechecker to see all imports publicly and I indeed got ?delayed instead of the whole elaboration script (but that was not under the failing block): https://github.com/buzden/Idris2/actions/runs/5820206080/job/15781485413#step:5:52

[buzden]

Just for a record: the reason of this quantity-related behaviour of underreduction is found by @AlgebraicWolf, but it is not obvious how to make all this work without reducing too much. The problem and directions of solution have been discussed on the latest weekly meeting in Discord, and are investigated at the moment.