Let bindings in module telescopes crash Agda.Interaction.BasicOps

[asr]

MWE of an issue privately reported by @mechvel:

open import Data.Nat

module Foo (let foo = zero) where

-- When asking for the contents of the module `bar` (which it isn't
-- defined) via C-c C-o, I got the the internal error:

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Interaction/BasicOps.hs:866

[andreasabel]

The code fixing #317 no longer works, as we have let-bindings in module parameters. Also, it would not work with parameter-refinement.

The proper way to fix this issue would be to represent let-bindings also in the section telescopes in internal syntax. Then one could, for instance, also ask for the value of zero interactively, with C-c C-n zero.

The quicker way to partially repair this is to store with LocalVar in the scope checker whether it is a let-bound variable, and delete all let-bound variables from the scope for interactive commands (since we do not have their types nor their definitions). The remaining locals can then be matched with the section telescope (assuming it has not be reordered).

[andreasabel]

Example not using the std-lib:

{-# OPTIONS -v interaction.top:20 #-}

open import Agda.Primitive

module _ (let foo = lzero) (A : Set) where

-- C-c C-o bar

[andreasabel]

I am fixing this by dropping let-bound variables from the telescope when preparing the context for top-level command execution.
Resolves the original issue, but referring to foo is still broken, yields an unbound-variable panic.