[ unelab ] Properly unelaborate metavariables originating from %search

[AlgebraicWolf]

Description

Thanks to @madman-bob for discovering this issue.

Consider the following code snippet that checks the value of %search and immediately quotes the checked value, logs it and runs an elaboration script that defines y : Nat to be the sum of the quoted value with itself.

import Language.Reflection

%language ElabReflection

x : Elab Nat
x = check `(%search)

defy : Elab ()
defy = do
    let fc = EmptyFC

    val <- quote !x
    logTerm "" 0 "Quoted term:" val

    declare [
        IClaim fc MW Private [] (MkTy fc fc (UN (Basic "y")) (IVar fc (UN (Basic "Nat")))),
        IDef fc (UN (Basic "y")) [PatClause fc (IVar fc (UN (Basic "y"))) (IApp fc (IApp fc (IVar fc (UN (Basic "+"))) val) val)]
    ]

%runElab defy

When checking the value, %search gets elaborated into a metavariable. Currently, when unelaboration occurs during quotation, all metavariables get turned into holes, so the quoted value becomes ?search, as shown in the log:

> idris2 --check SearchExample.idr
1/1: Building SearchExample (SearchExample.idr)
LOG 0: quoted: ?search

After that, y gets defined as ?search + ?search, leading to a compilation error:

> idris2 --check SearchExample.idr
1/1: Building SearchExample (SearchExample.idr)
LOG 0: quoted: ?search
Error: Error during reflection: While processing right hand side
of y. SearchExample.search is already defined.

SearchExample:10:13--10:20
 06 |
 07 | %language ElabReflection
 08 |
 09 | x : Elab Nat
 10 | x = check `(%search)
                  ^^^^^^^

This PR fixes the issue by unelaborating metavariables into ISearch instead of IHole in case the metavariable corresponds to a definition constructed with BySearch.

[gallais]

This is consistent with the current handling of holes.

In the future however I would like it if we could have a more general principle
allowing us to use the same hole in multiple locations to explicitly denote the
fact we mean all of these yet unknown terms to be equal to each other.