Holes at unerased quantity produce bad code

[dunhamsteve]

Steps to Reproduce

The compiler produces produces bad scheme code for the following:

total
fun : Nat -> Nat
fun k = ?fun_rhs

total
fun_proof : (x : Nat) -> fun x = x + 2
fun_proof x = Refl

main : IO ()
main = do
  let x = fun 42
  putStrLn . show $ x

The scheme output is:

(define Main-fun_rhs (lambda (ext-0) (+ ext-0 2)))
(define Main-fun (lambda (arg-0) (Main-fun_rhs 'erased)))

Here ?fun_rhs is being solved when checking the Refl and then substituted into fun with 'erased as an argument instead of arg-0. This also happens when _ or ? is used in place of ?fun_rhs.

Observed Behavior

The code compiles without error or warning and crashes with Exception in +: erased is not a number (and s similar message on javasacript).

Expected Behavior

I believe correct code should be produced or a warning / error should be presented. I'm not sure if we intend for named holes to be solved. I see a SolvedNameHole error in Idris, but it is never thrown.

If _ and ? are allowed to be used at a non-erased quantity, we should get the arguments right. Otherwise, we should emit an error when they are used at a non-erased quantity.

Are named holes allowed to be solved? And are we allowed to use _ and ? to be used in unerased contexts?

[kontheocharis]

It should be a compile-time error since fun_rhs is being solved in irrelevant position but is originally relevant. Since holes in Idris can at least survive across a module (maybe also across modules? idk), the linearity check should happen on a module level, rather than on a definition level. From my limited understanding of the codebase, currently this is done after elaborating each definition.

[kontheocharis]

Also in general, metas can be relevant even in the absence of _ and ? (for example, unrestricted implicits create such metas)

[spcfox]

the linearity check should happen on a module level, rather than on a definition level

I expect that by the time linearity is checked, all meta-variables will have been resolved. We also build a case tree there. If a function contains unresolved metas, it will be compiled incorrectly.

[spcfox]

I think we could have postponed compiling the definition if there were still unresolved metavariables in it.

[dunhamsteve]

Yeah, it looks like the args on the unsolved metas are erased (and replaced with an erased value in the app) when the runtime tree is compiled. If this were not done, then user holes can cause linearity errors.

https://github.com/idris-lang/Idris2/blob/8c970f1baa75d0ab34d19429a2e05e8f52ff8b96/src/Core/LinearCheck.idr#L218-L220

We can't postpone in all cases of unsolved holes, since user holes like ?fun_rhs are expected to remain unsolved. It looks like the code assumes there is never an attempt to solve them: https://github.com/idris-lang/Idris2/blob/8c970f1baa75d0ab34d19429a2e05e8f52ff8b96/src/TTImp/Elab/Hole.idr#L47-L51

An alternative to postponing would be to freeze any non-erased holes that are still unsolved when the function is compiled, marking them as unsolvable. But I don't think there is a mechanism to do this in Idris.

[spcfox]

We can't postpone in all cases of unsolved holes, since user holes like ?fun_rhs are expected to remain unsolved. It looks like the code assumes there is never an attempt to solve them:

Yes, I meant that _ and ? should remain unresolved. Moreover, I think that if there are user holes in the code, other metas can remain unresolved (potentially, we don't have enough information). I experimented with this a little, but without postponement, a lot of code breaks.

https://github.com/spcfox/Idris2/commit/c61077b0b38096c0321e7d668893542c160c497a

An alternative to postponing would be to freeze any non-erased holes that are still unsolved when the function is compiled, marking them as unsolvable. But I don't think there is a mechanism to do this in Idris.

I think we don't need to separate erased holes because we can still get a compile time tree with metavariables. I would build a case tree only after resolving all holes. But we can't do that at the end of the module because functions can be called in other function types. In any case, this requires adding a non-trivial mechanism.

[spcfox]

I'm not sure if we intend for named holes to be solved. I see a SolvedNameHole error in Idris, but it is never thrown.

I tried to deny the solving of user-defined holes.https://github.com/idris-lang/Idris2/commit/6699ce1acd77da12b7ddfdbb82f48ee7aef4e631

It works, but breaks interactive035. Proof search uses the definition if the hole is solved by unification, and this solution is better than what proof search could get (here it will suggest n). https://github.com/idris-lang/Idris2/blob/6f537291904e26f104cea931d1602e65d39f188a/src/TTImp/Interactive/ExprSearch.idr#L187-L190 I also believe that user holes should remain as such. Maybe we should keep the solution, but not use it during compilation?

[dunhamsteve]

That makes sense. I think the issue is that it's not the most general unifier, but I don't think that's an issue when we're solving something and presenting it to the user for approval. (And %search probably isn't mgu either.)

I believe the case at the top of this bug wouldn't happen if we're blocking top level definitions with unsolved metas.

In any case, this requires adding a non-trivial mechanism.

I see there is a Delayed mechanism for deferring top level definitions, could that be leveraged here?

[spcfox]

I see there is a Delayed mechanism for deferring top level definitions, could that be leveraged here?

In my view, it doesn’t really fit very well, but it might be possible.

[kontheocharis]

How will delaying help here? The issue is that the linearity check doesn't catch this usage pattern, not that the hole hasn't been solved yet.

[spcfox]

During linearity checking, the body contains a hole, so the linear checker does not know what will be used there. We need to run it after resolving all metavariables.

[kontheocharis]

Right I see, so delay the linearity checking, not the codegen?

[spcfox]

The body of the function is important not only for linear checkeer. We use it to construct the compile-time case tree (used during normalisation and totality checking) https://github.com/idris-lang/Idris2/blob/6f537291904e26f104cea931d1602e65d39f188a/src/TTImp/ProcessDef.idr#L1001-L1003 and the run-time tree (used for code generation) https://github.com/idris-lang/Idris2/blob/6f537291904e26f104cea931d1602e65d39f188a/src/TTImp/ProcessDef.idr#L1051-L1052

I think we expect that once processDef has finished, all the structures are correct, so they need to be built after the holes have been solved.

[dunhamsteve]

The generation of the runtime case tree would need to be delayed. There is function called linearCheck that in addition to checking linearity, returns a term with Erased inserted for quantity zero arguments. It the case in this issue, it sees that the hole is unsolved and to make progress it assumes all of the arguments are unused. It returns an application of that meta to to the value erased instead of the variable. Later, when the scheme code is generated, the solution to the meta (\x => x + 2) is inlined, applied to erased, and we get erased + 2. (Changing it to not assume the arguments are unused does resolve the issue above, but it doesn't solve the issue in #3680, and it breaks linearity checking elsewhere.)

I think we immediately need the compile time case tree, because it is used in normalization. I wonder if we could continue to build the compile time tree, but save building the runtime trees until the end of the module. (That might be simpler than delaying it case-by-case.)

[dunhamsteve]

And just to clarify, I assume kontheocharis' observation above, that this shouldn't be solved in the first place, is correct. But currently, even if the meta is solved with a proper RigW expression, the compiler has already committed to a runtime code tree where ?fun_rhs doesn't use its argument and is applied to 'erased. So I think that needs to be addressed in addition to whether we are allowed to solve the meta with an erased values.