[ fix ] fix shadowing issue in record elaboration and reflection

src/TTImp/Unelab.idr

@@ -238,14 +238,17 @@ mutual
                                  _ => 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
-                NoSugar True =>
-                   let x' = uniqueLocal vars x in
-                       unelabBinder umode nest fc env x' b
-                                    (compat sc) sc'
-                                    (compat !(getTerm scty))
-                _ => unelabBinder umode nest fc env x b sc sc' !(getTerm scty)
+      = case umode of
+          NoSugar True => do
+            let x' = uniqueLocal vars x
+            let sc : Term (x' :: vars) = compat sc
+            (sc', scty) <- unelabTy umode nest (b :: env) sc
+            unelabBinder umode nest fc env x' b
+                         (compat sc) sc'
+                         (compat !(getTerm scty))
+          _ => do
+            (sc', scty) <- unelabTy umode nest (b :: env) sc
+            unelabBinder umode nest fc env x b sc sc' !(getTerm scty)
     where
       next : Name -> Name
       next (MN n i) = MN n (i + 1)

tests/idris2/data/record021/Issue3501.idr

@@ -0,0 +1,7 @@
+import Data.Vect
+record Foo (th : Vect n a) where
+  nIsZero     : n === 0
+  vectIsEmpty : (th ===)
+                 $ replace {p = \ n => Vect n a} (sym nIsZero)
+                 $ Nil
+

tests/idris2/data/record021/expected

@@ -1 +1,2 @@
 1/1: Building RecordParam (RecordParam.idr)
+1/1: Building Issue3501 (Issue3501.idr)

tests/idris2/data/record021/run

@@ -1,3 +1,4 @@
 . ../../../testutils.sh
 
 check RecordParam.idr
+check Issue3501.idr

tests/idris2/reflection/reflection033/QuotingShadowed.idr

@@ -0,0 +1,100 @@
+module QuotingShadowed
+
+import Data.Vect
+
+import Language.Reflection
+
+%language ElabReflection
+
+X : (Nat -> Nat) -> Type
+X f = Vect (f 2) Unit
+
+--------------------------
+--- Shadowing using UN ---
+--------------------------
+
+-- (x : Nat) -> (y : X (\x -> S x)) -> Nat
+tyExpr : TTImp
+tyExpr =
+  IPi EmptyFC MW ExplicitArg (Just `{x}) `(Prelude.Types.Nat) $
+  IPi EmptyFC MW ExplicitArg (Just `{y}) (
+    IApp EmptyFC `(QuotingShadowed.X) $
+      ILam EmptyFC MW ExplicitArg (Just $ UN $ Basic "x") `(Prelude.Types.Nat) $
+        IApp EmptyFC `(Prelude.Types.S) $ IVar EmptyFC `{x}
+  ) $
+  `(Prelude.Types.Nat)
+
+ty : Elab Type
+ty = check tyExpr
+
+T : Type
+T = %runElab ty
+
+f : T
+f n [(), (), ()] = 4
+
+--------------------------------
+--- Pseudo-shadowing with MN ---
+--------------------------------
+
+tyExpr' : TTImp
+tyExpr' =
+  IPi EmptyFC MW ExplicitArg (Just `{x}) `(Prelude.Types.Nat) $
+  IPi EmptyFC MW ExplicitArg (Just `{y}) (
+    IApp EmptyFC `(QuotingShadowed.X) $
+      ILam EmptyFC MW ExplicitArg (Just $ MN "x" 0) `(Prelude.Types.Nat) $
+        IApp EmptyFC `(Prelude.Types.S) $ IVar EmptyFC `{x}
+  ) $
+  `(Prelude.Types.Nat)
+
+ty' : Elab Type
+ty' = check tyExpr'
+
+T' : Type
+T' = %runElab ty'
+
+f' : T'
+f' Z     [()]     = 4
+f' (S x) (()::xs) = S $ f' x xs
+
+--------------------------------
+--- Requoted the one with UN ---
+--------------------------------
+
+tyExpr'' : TTImp
+tyExpr'' = %runElab quote T
+
+ty'' : Elab Type
+ty'' = check tyExpr''
+
+T'' : Type
+T'' = %runElab ty''
+
+f'' : T''
+f'' n [(), (), ()] = 4
+
+-- check that T'' has really `MN _ 0` --
+
+N'' : Nat
+N'' = case tyExpr'' of
+        (IPi _ _ _ _ _ $ IPi _ _ _ _ (IApp _ _ $ ILam _ _ _ (Just n) _ _) _) =>
+          case n of
+            UN _     => 1
+            MN "x" 0 => 2
+            _        => 3
+        _ => 0
+
+n''value : N'' = 2
+n''value = Refl
+
+--------------------
+--- Printing out ---
+--------------------
+
+%runElab logSugaredTerm "shdw" 0 "tyExpr  " tyExpr
+%runElab logSugaredTerm "shdw" 0 "tyExpr' " tyExpr'
+%runElab logSugaredTerm "shdw" 0 "tyExpr''" tyExpr''
+
+%runElab logSugaredTerm "shdw" 0 "quoted T  " !(quote T  )
+%runElab logSugaredTerm "shdw" 0 "quoted T' " !(quote T' )
+%runElab logSugaredTerm "shdw" 0 "quoted T''" !(quote T'')

tests/idris2/reflection/reflection033/expected

@@ -0,0 +1,7 @@
+1/1: Building QuotingShadowed (QuotingShadowed.idr)
+LOG shdw:0: tyExpr  : (x : Nat) -> (y : X (\x => S x)) -> Nat
+LOG shdw:0: tyExpr' : (x : Nat) -> (y : X (\{x:0} => S x)) -> Nat
+LOG shdw:0: tyExpr'': (x : Nat) -> (y : X (\{x:0} => S {x:0})) -> Nat
+LOG shdw:0: quoted T  : (x : Nat) -> (y : X (\{x:0} => S {x:0})) -> Nat
+LOG shdw:0: quoted T' : (x : Nat) -> (y : X (\{x:0} => S x)) -> Nat
+LOG shdw:0: quoted T'': (x : Nat) -> (y : X (\{x:0} => S {x:0})) -> Nat

tests/idris2/reflection/reflection033/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check --show-machine-names QuotingShadowed.idr