Proof generated interactively with `:elab` doesn't work.

[cbiffle]

Found in 13045109d058b248a2fc69c786a969b9d14f4b85.

The continued saga of the binary expression evaluator:

module IntroFail

import Pruviloj
import Pruviloj.Induction

||| A Boolean expression.
data BExp : Type where
  BTrue : BExp
  BFalse : BExp
  BAnd : BExp -> BExp -> BExp

||| Evaluation function for Booleans.
beval : BExp -> Bool
beval BTrue = True
beval BFalse = False
beval (BAnd x y) = beval x && beval y

||| An identity transform.
bid : BExp -> BExp
bid (BAnd x y) = BAnd (bid x) (bid y)
bid x = x

attackAndSolve : Elab a -> Elab a
attackAndSolve body = attack *> body <* solve

||| Proof that the identity transform really is one.
bid_id : (b : BExp) -> beval b = beval (bid b)
bid_id b = ?bid_id_rhs

Using the :elab interactive shell I was able to generate this proof:

-IntroFail.bid_id_rhs> :qed
Proof completed!
IntroFail.bid_id_rhs = %runElab (do intro `{{b}}
                                    induction (Var `{{b}}) `andThen` (compute *> try search)
                                    attack
                                    intro `{{x}}
                                    intro `{{ix}}
                                    intro `{{y}}
                                    intro `{{iy}}
                                    rewriteWith (Var `{{ix}})
                                    attack
                                    rewriteWith (Var `{{iy}})
                                    search
                                    repeatUntilFail solve)

However, pasting it into the source code gives:

/home/cbiffle/proj/idris/playground/IntroFail.idr:30:22:
When checking right hand side of IntroFail.bid_id_rhs:
INTERNAL ERROR: Nothing to fill in.
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

I've tried rewriting the proof a couple of different ways, including sticking only to operations I've seen David use and avoiding quoting; same effect. Here's one such version:

IntroFail.bid_id_rhs =
  %runElab (do
           b <- gensym "b"
           intro b
           induction (Var b) `andThen` (compute *> try search)
           attack
           x <- gensym "x"
           ix <- gensym "ix"
           y <- gensym "y"
           iy <- gensym "iy"
           intro x
           intro ix
           intro y
           intro iy
           rewriteWith (Var ix)
           attack
           rewriteWith (Var iy)
           search
           repeatUntilFail solve)

[david-christiansen]

The reason why this fails is that you're solving too much. I should look into making this impossible - but what's happening here is that Idris itself has a hole into which the result of reflected elaboration should be placed. Once the reflected elaboration script is done running, Idris calls solve on that hole, but it's already been solved!

The proof term right before repeatUntilFail solve looks like this:

             ?{hole0} ≈ λ b .
                          ?{BAnd306} ≈ λ x .
                                         λ ix .
                                           λ y .
                                             λ iy .
                                               ?{hole213} ≈ replace Prelude.Bool.Bool
                                                              (IntroFail.beval y)
                                                              (IntroFail.beval
                                                                 (IntroFail.bid y))
                                                              (λ {replaced0} .
                                                                 = Prelude.Bool.Bool
                                                                   Prelude.Bool.Bool
                                                                   (Prelude.Bool.&&
                                                                      (IntroFail.beval
                                                                         x)
                                                                      (Delay LazyEval
                                                                         Prelude.Bool.Bool
                                                                         (IntroFail.beval
                                                                            y)))
                                                                   (Prelude.Bool.&&
                                                                      (IntroFail.beval
                                                                         x)
                                                                      (Delay LazyEval
                                                                         Prelude.Bool.Bool
                                                                         {replaced0})))
                                                              iy
                                                              (Refl Prelude.Bool.Bool
                                                                 (Prelude.Bool.&&
                                                                    (IntroFail.beval
                                                                       x)
                                                                    (Delay LazyEval
                                                                       Prelude.Bool.Bool
                                                                       (IntroFail.beval
                                                                          y)))) .
                                                 replace Prelude.Bool.Bool
                                                   (IntroFail.beval x)
                                                   (IntroFail.beval
                                                      (IntroFail.bid x))
                                                   (λ {replaced0} .
                                                      = Prelude.Bool.Bool
                                                        Prelude.Bool.Bool
                                                        (Prelude.Bool.&&
                                                           (IntroFail.beval x)
                                                           (Delay LazyEval
                                                              Prelude.Bool.Bool
                                                              (IntroFail.beval y)))
                                                        (Prelude.Bool.&& {replaced0}
                                                           (Delay LazyEval
                                                              Prelude.Bool.Bool
                                                              (IntroFail.beval
                                                                 (IntroFail.bid
                                                                    y)))))
                                                   ix
                                                   {hole213} .
                            Pruviloj.Induction.Eliminators.<<elim IntroFail.BExp>> b
                              (λ {subj307} .
                                 = Prelude.Bool.Bool Prelude.Bool.Bool
                                   (IntroFail.beval {subj307})
                                   (IntroFail.beval (IntroFail.bid {subj307})))
                              (Refl Prelude.Bool.Bool Prelude.Bool.True)
                              (Refl Prelude.Bool.Bool Prelude.Bool.False)
                              {BAnd306} .
               {hole0}

There are three guess bindings: {hole0}, {BAnd306}, and {hole213}. Your proof script should be calling solve twice, leaving the guess in {hole0}.

I'll have a ponder over how to prevent this from happening. I can probably isolate the term so that outer holes aren't accessible, but it'll require a bit of thought to get right.

[david-christiansen]

I guess another way to say this is that when you were in the interactive shell, you were dealing with your script alone. When you have a %runElab expression, then it's running in a context and it can affect that context. Your repeatUntilFail solve solved one too many holes when it ran in a context where an extra guess could be solved.

[cbiffle]

Understood. This continues to feel oddly like Forth; I have caused a stack underflow in the implicit hole stack.

[david-christiansen]

It looks like making external holes invisible is a non-starter, because there's not a reasonable way to do that but maintain the visibility of external bindings, which I think Elab scripts should have access to.

I think that the solution is probably to have a kind of access control instead. When starting the execution of an elaborator script, get a list of all visible holes, and then prevent modifications to them in the reflected tactics.

[ahmadsalim]

Still an error in 0.11