[ unelab ] Properly unelaborate metavariables originating from %search (#3055)

* [ unelab ] Properly unelaborate `%search`

* [ test ] Added regression test that checks quotation of `%search`

src/TTImp/Unelab.idr

@@ -229,11 +229,15 @@ mutual
   unelabTy' umode nest env (Meta fc n i args)
       = do defs <- get Ctxt
            let mkn = nameRoot n
+           def <- lookupDefExact (Resolved i) (gamma defs)
+           let term = case def of
+                              (Just (BySearch _ d _)) => ISearch fc d
+                              _ => IHole fc mkn
            Just ty <- lookupTyExact (Resolved i) (gamma defs)
                | Nothing => case umode of
                                  ImplicitHoles => pure (Implicit fc True, gErased fc)
-                                 _ => pure (IHole fc mkn, gErased fc)
-           pure (IHole fc mkn, gnf env (embed ty))
+                                 _ => pure (term, gErased fc)
+           pure (term, gnf env (embed ty))
   unelabTy' umode nest env (Bind fc x b sc)
       = do (sc', scty) <- unelabTy umode nest (b :: env) sc
            case umode of

tests/Main.idr

@@ -250,7 +250,8 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing
        "reflection005", "reflection006", "reflection007", "reflection008",
        "reflection009", "reflection010", "reflection011", "reflection012",
        "reflection013", "reflection014", "reflection015", "reflection016",
-       "reflection017", "reflection018", "reflection019", "reflection020"]
+       "reflection017", "reflection018", "reflection019", "reflection020",
+       "reflection021"]
 
 idrisTestsWith : TestPool
 idrisTestsWith = MkTestPool "With abstraction" [] Nothing

tests/idris2/reflection021/QuoteSearch.idr

@@ -0,0 +1,22 @@
+module QuoteSearch
+
+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

tests/idris2/reflection021/expected

@@ -0,0 +1,2 @@
+1/1: Building QuoteSearch (QuoteSearch.idr)
+LOG 0: Quoted term:: %search

tests/idris2/reflection021/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check QuoteSearch.idr