From ab3862798b044c68c6b9b9425f054928d700a553 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Tue, 23 Nov 2021 02:51:18 +0300
Subject: [PATCH] [ fix ] Use right reflection constructor name for unambiguing
 `with`

---
 src/TTImp/Reflect.idr                      |  2 +-
 tests/Main.idr                             |  1 +
 tests/idris2/reflection013/WithUnambig.idr | 12 ++++++++++++
 tests/idris2/reflection013/expected        |  1 +
 tests/idris2/reflection013/run             |  4 ++++
 5 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 tests/idris2/reflection013/WithUnambig.idr
 create mode 100644 tests/idris2/reflection013/expected
 create mode 100755 tests/idris2/reflection013/run

diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr
index f842bd907..0a7571095 100644
--- a/src/TTImp/Reflect.idr
+++ b/src/TTImp/Reflect.idr
@@ -633,7 +633,7 @@ mutual
         = do fc' <- reflect fc defs lhs env tfc
              ns' <- reflect fc defs lhs env ns
              t' <- reflect fc defs lhs env t
-             appCon fc defs (reflectionttimp "WithUnambigNames") [fc', ns', t']
+             appCon fc defs (reflectionttimp "IWithUnambigNames") [fc', ns', t']
 
   export
   Reflect IFieldUpdate where
diff --git a/tests/Main.idr b/tests/Main.idr
index 33ff5cde9..93ec07136 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -215,6 +215,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
        "reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",
        "reflection009", "reflection010", "reflection011", "reflection012",
+       "reflection013",
        -- The 'with' rule
        "with001", "with002", "with004", "with005", "with006",
        -- with-disambiguation
diff --git a/tests/idris2/reflection013/WithUnambig.idr b/tests/idris2/reflection013/WithUnambig.idr
new file mode 100644
index 000000000..fb319b441
--- /dev/null
+++ b/tests/idris2/reflection013/WithUnambig.idr
@@ -0,0 +1,12 @@
+import Language.Reflection
+
+x : TTImp
+x = `(with Prelude.Nil [])
+
+%language ElabReflection
+
+x' : Elab (List Nat)
+x' = check x
+
+l : List Nat
+l = 1 :: %runElab x'
diff --git a/tests/idris2/reflection013/expected b/tests/idris2/reflection013/expected
new file mode 100644
index 000000000..47483d206
--- /dev/null
+++ b/tests/idris2/reflection013/expected
@@ -0,0 +1 @@
+1/1: Building WithUnambig (WithUnambig.idr)
diff --git a/tests/idris2/reflection013/run b/tests/idris2/reflection013/run
new file mode 100755
index 000000000..05d35edea
--- /dev/null
+++ b/tests/idris2/reflection013/run
@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check WithUnambig.idr
+