[ fix, re #3063 ] Fix forgotten reflection values

idris-lang · Dec 21, 2023 · 36132f6 · 36132f6
1 parent 58e5d15
commit 36132f6
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 2 deletions.
diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr
@@ -330,9 +330,9 @@ export
 Reflect a => Reflect (WithDefault a def) where
   reflect fc defs lhs env def
     = onWithDefault
-        (appCon fc defs (reflectionttimp "Default") [Erased fc Placeholder, Erased fc Placeholder])
+        (appCon fc defs (reflectionttimp "DefaultedValue") [Erased fc Placeholder, Erased fc Placeholder])
         (\x => do x' <- reflect fc defs lhs env x
-                  appCon fc defs (reflectionttimp "Value") [Erased fc Placeholder, Erased fc Placeholder, x'])
+                  appCon fc defs (reflectionttimp "SpecifiedValue") [Erased fc Placeholder, Erased fc Placeholder, x'])
         def
 
 export

diff --git a/tests/idris2/reflection/reflection026/Issue3168.idr b/tests/idris2/reflection/reflection026/Issue3168.idr
@@ -0,0 +1,15 @@
+import Language.Reflection
+
+%language ElabReflection
+
+data_decl : List Decl
+data_decl = `[data T = A | B]
+
+record_decl : List Decl
+record_decl = `[record R where]
+
+data_decl' : List Decl
+data_decl' = `[public export data T = A | B]
+
+record_decl' : List Decl
+record_decl' = `[public export record R where]
diff --git a/tests/idris2/reflection/reflection026/expected b/tests/idris2/reflection/reflection026/expected
@@ -0,0 +1 @@
+1/1: Building Issue3168 (Issue3168.idr)
diff --git a/tests/idris2/reflection/reflection026/run b/tests/idris2/reflection/reflection026/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Issue3168.idr
diff --git a/tests/idris2/reflection/reflection026/test.ipkg b/tests/idris2/reflection/reflection026/test.ipkg
@@ -0,0 +1 @@
+package a-test