[ fix #3670 ] Instantiate holes with correct PiInfo (#3672)

* [ fix ] Unification error in implementation elaboration

* update CHANGELOG_NEXT

* [ admin ] Include issue number in changelog text

---------

Co-authored-by: Thomas E. Hansen <[email protected]>

Author: dunhamsteve

CHANGELOG_NEXT.md

@@ -30,19 +30,17 @@ should target this file (`CHANGELOG_NEXT`).
   - `Libraries.Data.List.Quantifiers.Extra.tabulate`.
   - `Libraries.Utils.Binary.nonEmptyRev`
   - `Libraries.Utils.String.dotSep`
+* Fixes an issue when unifying labmda terms with implicits (#3670)
+* The compiler now warns the user when `impossible` clauses are ignored. This
+  typically happens when a numeric literal or an ambiguous name appears in an
+  `impossible` clause.
 
 ### Building/Packaging changes
 
 * Fix parsing of capitalised package names containing hyphens.
 
 ### Backend changes
 
-### Compiler changes
-
-* The compiler now warns the user when `impossible` clauses are ignored. This
-  typically happens when a numeric literal or an ambiguous name appears in an
-  `impossible` clause.
-
 #### RefC Backend
 
 * Fixed an issue to do with `alligned_alloc` not existing on older MacOS

src/Core/Unify.idr

@@ -565,9 +565,9 @@ tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
             List (Var newvars) ->
             IVars vs newvars -> Term newvars -> Term vs ->
             Core (Maybe (Term vs))
-    mkDef (v :: vs) vars soln (Bind bfc x (Pi fc c _ ty) sc)
+    mkDef (v :: vs) vars soln (Bind bfc x (Pi fc c info ty) sc)
        = do sc' <- mkDef vs (ICons (Just v) vars) soln sc
-            pure $ (Bind bfc x (Lam fc c Explicit (Erased bfc Placeholder)) <$> sc')
+            pure $ (Bind bfc x (Lam fc c info (Erased bfc Placeholder)) <$> sc')
     mkDef vs vars soln (Bind bfc x b@(Let _ c val ty) sc)
        = do mbsc' <- mkDef vs (ICons Nothing vars) soln sc
             flip traverseOpt mbsc' $ \sc' =>

tests/idris2/basic/basic076/Issue3670.idr

@@ -0,0 +1,36 @@
+import Data.Vect
+
+public export
+data Chain : (len : Nat) -> (t : Nat -> Type -> Type)
+  -> (item : Type)
+  -> (m : forall a, b, c . t a c -> t b c -> Type)
+  -> (input : t a' item) -> (output : t b' item) -> Type where
+  Same : {m : forall a, b, c . t a c -> t b c -> Type} -> Chain 0 t item m x x
+  Apply : {m : forall a, b, c . t a c -> t b c -> Type}
+    -> (prev : Chain len t item m input intermediate) -> (modification : m intermediate output)
+    -> Chain (S len) t item m input output
+
+public export
+interface LawfulChain (t : Nat -> Type -> Type)
+  (m : forall a, b, c . t a c -> t b c -> Type) | m where
+  apply : (input : t len_input item)
+    -> {0 output : t len_output item} -> (chain : Chain len_chain t item m input output)
+    -> t len_output item
+  applyCorrect : (input : t len_input item)
+    -> {0 output : t len_output item} -> (chain : Chain len_chain t item m input output)
+    -> (apply input chain) = output
+
+public export
+data Modification : Vect n item -> Vect m item -> Type where
+  Insert : {0 prev : Vect n item} -> (idx : Fin (S n)) -> (it : item)
+    -> Modification prev (insertAt idx it prev)
+  Delete : {0 prev : Vect (S n) item} -> (idx : Fin (S n))
+    -> Modification prev (deleteAt idx prev)
+
+public export
+LawfulChain Vect Modification where
+  apply input Same = input
+  apply input (Apply prev (Insert idx it)) = insertAt idx it (apply input prev)
+  apply input (Apply prev (Delete idx)) = deleteAt idx (apply input prev)
+  applyCorrect input chain = ?applyCorrect_rhs
+

tests/idris2/basic/basic076/expected

@@ -0,0 +1 @@
+1/1: Building Issue3670 (Issue3670.idr)

tests/idris2/basic/basic076/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Issue3670.idr