[ re #3314, #34 ] Tighten the location information for implicits

When implicitly binding a variable, use the location of the head
function/constructor that expects it. This way we can differentiate
multiple implicits bound on the same LHS.

Note that this does not resolve the issue 34: there the location
is then further muddled by the fact that where-bound functions
are lifted to the toplevel.

src/TTImp/Elab/App.idr

@@ -187,7 +187,8 @@ mutual
            metaval <- metaVar fc argRig env nm metaty
            let fntm = App fc tm metaval
            fnty <- sc defs (toClosure defaultOpts env metaval)
-           when (bindingVars elabinfo) $ update EST $ addBindIfUnsolved nm argRig Implicit env metaval metaty
+           when (bindingVars elabinfo) $ update EST $
+             addBindIfUnsolved nm (getLoc (getFn tm)) argRig Implicit env metaval metaty
            checkAppWith rig elabinfo nest env fc
                         fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
 
@@ -220,7 +221,7 @@ mutual
                    metaval <- metaVar fc argRig env nm metaty
                    let fntm = App fc tm metaval
                    fnty <- sc defs (toClosure defaultOpts env metaval)
-                   update EST $ addBindIfUnsolved nm argRig AutoImplicit env metaval metaty
+                   update EST $ addBindIfUnsolved nm (getLoc (getFn tm)) argRig AutoImplicit env metaval metaty
                    checkAppWith rig elabinfo nest env fc
                                 fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
            else do defs <- get Ctxt
@@ -277,7 +278,7 @@ mutual
                    metaval <- metaVar fc argRig env nm metaty
                    let fntm = App fc tm metaval
                    fnty <- sc defs (toClosure defaultOpts env metaval)
-                   update EST $ addBindIfUnsolved nm argRig AutoImplicit env metaval metaty
+                   update EST $ addBindIfUnsolved nm (getLoc (getFn tm)) argRig AutoImplicit env metaval metaty
                    checkAppWith rig elabinfo nest env fc
                                 fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
            else do defs <- get Ctxt

src/TTImp/Elab/Check.idr

@@ -64,7 +64,8 @@ Eq ElabOpt where
 public export
 data ImplBinding : List Name -> Type where
      NameBinding : {vars : _} ->
-                   RigCount -> PiInfo (Term vars) -> (elabAs : Term vars) -> (expTy : Term vars) ->
+                   FC -> RigCount -> PiInfo (Term vars) ->
+                   (elabAs : Term vars) -> (expTy : Term vars) ->
                    ImplBinding vars
      AsBinding : {vars : _} ->
                  RigCount -> PiInfo (Term vars) -> (elabAs : Term vars) -> (expTy : Term vars) ->
@@ -74,12 +75,12 @@ data ImplBinding : List Name -> Type where
 export
 covering
 Show (ImplBinding vars) where
-  show (NameBinding c p tm ty) = show (tm, ty)
+  show (NameBinding _ c p tm ty) = show (tm, ty)
   show (AsBinding c p tm ty pat) = show (tm, ty) ++ "@" ++ show tm
 
 export
 bindingMetas : ImplBinding vars -> NameMap Bool
-bindingMetas (NameBinding c p tm ty) = getMetas ty
+bindingMetas (NameBinding _ c p tm ty) = getMetas ty
 bindingMetas (AsBinding c p tm ty pat)
     = insertAll (toList (getMetas ty)) (getMetas pat)
   where
@@ -90,24 +91,24 @@ bindingMetas (AsBinding c p tm ty pat)
 -- Get the type of an implicit name binding
 export
 bindingType : ImplBinding vars -> Term vars
-bindingType (NameBinding _ _ _ ty) = ty
+bindingType (NameBinding _ _ _ _ ty) = ty
 bindingType (AsBinding _ _ _ ty _) = ty
 
 -- Get the term (that is, the expanded thing it elaborates to, of the name
 -- applied to the context) from an implicit binding
 export
 bindingTerm : ImplBinding vars -> Term vars
-bindingTerm (NameBinding _ _ tm _) = tm
+bindingTerm (NameBinding _ _ _ tm _) = tm
 bindingTerm (AsBinding _ _ tm _ _) = tm
 
 export
 bindingRig : ImplBinding vars -> RigCount
-bindingRig (NameBinding c _ _ _) = c
+bindingRig (NameBinding _ c _ _ _) = c
 bindingRig (AsBinding c _ _ _ _) = c
 
 export
 bindingPiInfo : ImplBinding vars -> PiInfo (Term vars)
-bindingPiInfo (NameBinding _ p _ _) = p
+bindingPiInfo (NameBinding _ _ p _ _) = p
 bindingPiInfo (AsBinding _ p _ _ _) = p
 
 -- Current elaboration state (preserved/updated throughout elaboration)
@@ -130,7 +131,7 @@ record EState (vars : List Name) where
                   -- bound yet. Record how they're bound (auto-implicit bound
                   -- pattern vars need to be dealt with in with-application on
                   -- the RHS)
-  bindIfUnsolved : List (Name, RigCount,
+  bindIfUnsolved : List (Name, FC, RigCount,
                           (vars' ** (Env Term vars', PiInfo (Term vars'),
                                      Term vars', Term vars', Thin outer vars')))
                   -- names to add as unbound implicits if they are still holes
@@ -203,8 +204,8 @@ weakenedEState {e}
   where
     wknTms : (Name, ImplBinding vs) ->
              (Name, ImplBinding (n :: vs))
-    wknTms (f, NameBinding c p x y)
-        = (f, NameBinding c (map weaken p) (weaken x) (weaken y))
+    wknTms (f, NameBinding fc c p x y)
+        = (f, NameBinding fc c (map weaken p) (weaken x) (weaken y))
     wknTms (f, AsBinding c p x y z)
         = (f, AsBinding c (map weaken p) (weaken x) (weaken y) (weaken z))
 
@@ -260,14 +261,14 @@ strengthenedEState {n} {vars} c e fc env
 
     strTms : Defs -> (Name, ImplBinding (n :: vars)) ->
              Core (Name, ImplBinding vars)
-    strTms defs (f, NameBinding c p x y)
+    strTms defs (f, NameBinding fc c p x y)
         = do xnf <- normaliseHoles defs env x
              ynf <- normaliseHoles defs env y
              case (shrinkPi p (Drop Refl),
                    removeArg xnf,
                    shrink ynf (Drop Refl)) of
                (Just p', Just x', Just y') =>
-                    pure (f, NameBinding c p' x' y')
+                    pure (f, NameBinding fc c p' x' y')
                _ => throw (BadUnboundImplicit fc env f y)
     strTms defs (f, AsBinding c p x y z)
         = do xnf <- normaliseHoles defs env x
@@ -322,7 +323,7 @@ concrete defs env _ = pure False
 export
 updateEnv : {new : _} ->
             Env Term new -> Thin new vars ->
-            List (Name, RigCount,
+            List (Name, FC, RigCount,
                    (vars' ** (Env Term vars', PiInfo (Term vars'),
                               Term vars', Term vars', Thin new vars'))) ->
             EState vars -> EState vars
@@ -334,12 +335,12 @@ updateEnv env sub bif st
 
 export
 addBindIfUnsolved : {vars : _} ->
-                    Name -> RigCount -> PiInfo (Term vars) ->
+                    Name -> FC -> RigCount -> PiInfo (Term vars) ->
                     Env Term vars -> Term vars -> Term vars ->
                     EState vars -> EState vars
-addBindIfUnsolved hn r p env tm ty st
+addBindIfUnsolved hn fc r p env tm ty st
     = { bindIfUnsolved $=
-         ((hn, r, (_ ** (env, p, tm, ty, subEnv st))) ::)} st
+         ((hn, fc, r, (_ ** (env, p, tm, ty, subEnv st))) ::)} st
 
 clearBindIfUnsolved : EState vars -> EState vars
 clearBindIfUnsolved = { bindIfUnsolved := [] }

src/TTImp/Elab/ImplicitBind.idr

@@ -54,7 +54,7 @@ mkOuterHole loc rig n topenv Nothing
          u <- uniVar loc
          ty <- metaVar loc erased env nm (TType loc u)
          log "elab.implicits" 10 $ "Made metavariable for type of " ++ show n ++ ": " ++ show nm
-         put EST (addBindIfUnsolved nm rig Explicit topenv (thin ty sub) (TType loc u) est)
+         put EST (addBindIfUnsolved nm loc rig Explicit topenv (thin ty sub) (TType loc u) est)
          tm <- implBindVar loc rig env n ty
          pure (thin tm sub, thin ty sub)
 
@@ -133,34 +133,34 @@ bindUnsolved {vars} fc elabmode _
          defs <- get Ctxt
          let bifs = bindIfUnsolved est
          log "elab.implicits" 5 $ "Bindable unsolved implicits: " ++ show (map fst bifs)
-         traverse_ (mkImplicit defs (outerEnv est) (subEnv est)) (bindIfUnsolved est)
+         traverse_ (mkImplicit defs (outerEnv est) (subEnv est)) bifs
   where
     makeBoundVar : {outer, vs : _} ->
-                   Name -> RigCount -> PiInfo (Term vs) -> Env Term outer ->
+                   Name -> FC -> RigCount -> PiInfo (Term vs) -> Env Term outer ->
                    Thin outer vs -> Thin outer vars ->
                    Term vs -> Core (Term vs)
-    makeBoundVar n rig p env sub subvars expected
+    makeBoundVar n loc rig p env sub subvars expected
         = case shrink expected sub of
                Nothing => do tmn <- toFullNames expected
                              throw (GenericMsg fc ("Can't bind implicit " ++ show n ++ " of type " ++ show tmn))
                Just exp' =>
                     do impn <- genVarName (nameRoot n)
                        tm <- metaVar fc rig env impn exp'
                        let p' : PiInfo (Term vars) = forgetDef p
-                       update EST { toBind $= ((impn, NameBinding rig p'
+                       update EST { toBind $= ((impn, NameBinding loc rig p'
                                                         (thin tm subvars)
                                                         (thin exp' subvars)) ::) }
                        pure (thin tm sub)
 
     mkImplicit : {outer : _} ->
                  Defs -> Env Term outer -> Thin outer vars ->
-                 (Name, RigCount, (vars' **
+                 (Name, FC, RigCount, (vars' **
                      (Env Term vars', PiInfo (Term vars'), Term vars', Term vars', Thin outer vars'))) ->
                  Core ()
-    mkImplicit defs outerEnv subEnv (n, rig, (vs ** (env, p, tm, exp, sub)))
+    mkImplicit defs outerEnv subEnv (n, loc, rig, (vs ** (env, p, tm, exp, sub)))
         = do Just (Hole _ _) <- lookupDefExact n (gamma defs)
                   | _ => pure ()
-             bindtm <- makeBoundVar n rig p outerEnv
+             bindtm <- makeBoundVar n loc rig p outerEnv
                                     sub subEnv
                                     !(normaliseHoles defs env exp)
              logTerm "elab.implicits" 5 ("Added unbound implicit") bindtm
@@ -261,15 +261,15 @@ bindImplVars {vars} fc mode gam env imps_in scope scty
                Bounds new -> (tm : Term vs) -> (ty : Term vs) ->
                (Term (new ++ vs), Term (new ++ vs))
     getBinds [] bs tm ty = (refsToLocals bs tm, refsToLocals bs ty)
-    getBinds {new} ((n, metan, NameBinding c p _ bty) :: imps) bs tm ty
+    getBinds {new} ((n, metan, NameBinding loc c p _ bty) :: imps) bs tm ty
         = let (tm', ty') = getBinds imps (Add n metan bs) tm ty
               bty' = refsToLocals bs bty in
               case mode of
                    PI c =>
                       (Bind fc _ (Pi fc c Implicit bty') tm',
                        TType fc (MN "top" 0))
                    _ =>
-                      (Bind fc _ (PVar fc c (map (weakenNs (sizeOf bs)) p) bty') tm',
+                      (Bind fc _ (PVar loc c (map (weakenNs (sizeOf bs)) p) bty') tm',
                        Bind fc _ (PVTy fc c bty') ty')
     getBinds ((n, metan, AsBinding c _ _ bty bpat) :: imps) bs tm ty
         = let (tm', ty') = getBinds imps (Add n metan bs) tm ty
@@ -348,13 +348,13 @@ getToBind {vars} fc elabmode impmode env excepts
          pure res'
   where
     normBindingTy : Defs -> ImplBinding vars -> Core (ImplBinding vars)
-    normBindingTy defs (NameBinding c p tm ty)
+    normBindingTy defs (NameBinding loc c p tm ty)
         = do case impmode of
                   COVERAGE => do tynf <- nf defs env ty
                                  when !(isEmpty defs env tynf) $
                                     throw (InternalError "Empty pattern in coverage check")
                   _ => pure ()
-             pure $ NameBinding c p tm !(normaliseType defs env ty)
+             pure $ NameBinding loc c p tm !(normaliseType defs env ty)
     normBindingTy defs (AsBinding c p tm ty pat)
         = do case impmode of
                   COVERAGE => do tynf <- nf defs env ty
@@ -456,8 +456,8 @@ checkBindVar rig elabinfo nest env fc str topexp
                         PI _ => setInvertible fc n
                         _ => pure ()
                    log "elab.implicits" 5 $ "Added Bound implicit " ++ show (n, (rig, tm, exp, bty))
-                   update EST { boundNames $= ((n, NameBinding rig Explicit tm exp) ::),
-                                toBind $= ((n, NameBinding rig Explicit tm bty) :: ) }
+                   update EST { boundNames $= ((n, NameBinding fc rig Explicit tm exp) ::),
+                                toBind $= ((n, NameBinding fc rig Explicit tm bty) :: ) }
 
                    log "metadata.names" 7 $ "checkBindVar is adding ↓"
                    addNameType fc (UN str) env exp
@@ -483,7 +483,7 @@ checkBindVar rig elabinfo nest env fc str topexp
     updateRig n c ((bn, r) :: bs)
         = if n == bn
              then case r of
-                  NameBinding _ p tm ty => (bn, NameBinding c p tm ty) :: bs
+                  NameBinding loc _ p tm ty => (bn, NameBinding loc c p tm ty) :: bs
                   AsBinding _ p tm ty pat => (bn, AsBinding c p tm ty pat) :: bs
              else (bn, r) :: updateRig n c bs
 

src/TTImp/Elab/Term.idr

@@ -224,7 +224,7 @@ checkTerm rig elabinfo nest env (Implicit fc b) (Just gexpty)
          when (b && bindingVars elabinfo) $
             do expty <- getTerm gexpty
                -- Explicit because it's an explicitly given thing!
-               update EST $ addBindIfUnsolved nm rig Explicit env metaval expty
+               update EST $ addBindIfUnsolved nm fc rig Explicit env metaval expty
          pure (metaval, gexpty)
 checkTerm rig elabinfo nest env (Implicit fc b) Nothing
     = do nmty <- genName "implicit_type"
@@ -234,7 +234,7 @@ checkTerm rig elabinfo nest env (Implicit fc b) Nothing
          metaval <- metaVar fc rig env nm ty
          -- Add to 'bindIfUnsolved' if 'b' set
          when (b && bindingVars elabinfo) $
-            update EST $ addBindIfUnsolved nm rig Explicit env metaval ty
+            update EST $ addBindIfUnsolved nm fc rig Explicit env metaval ty
          pure (metaval, gnf env ty)
 checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp
     = do -- enter the scope -> add unambiguous names

tests/idris2/error/error028/expected

@@ -11,5 +11,5 @@ Issue3313:5:18--5:23
                       ^^^^^
 
 Possible correct results:
-    conArg (implicitly bound at Issue3313:5:1--5:23)
-    conArg (implicitly bound at Issue3313:5:1--5:23)
+    conArg (implicitly bound at Issue3313:5:7--5:10)
+    conArg (implicitly bound at Issue3313:5:1--5:5)

tests/idris2/error/error029/Issue34.idr

@@ -0,0 +1,9 @@
+data T : Type -> Type where
+  Leaf : T a
+  Node : Ord a => a -> T a -> T a -> T a
+
+zipWith : (a -> a -> a) -> T a -> T a -> T a
+zipWith f Leaf _ = Leaf
+zipWith f _ Leaf = Leaf
+zipWith f (Node x lx rx) (Node y ly ry)
+  = Node (f x y) (zipWith f lx ly) (zipWith f rx ry)

tests/idris2/error/error029/expected

@@ -0,0 +1,15 @@
+1/1: Building Issue34 (Issue34.idr)
+Error: While processing right hand side of zipWith. Multiple solutions found in search of:
+    Ord a
+
+Issue34:9:5--9:53
+ 5 | zipWith : (a -> a -> a) -> T a -> T a -> T a
+ 6 | zipWith f Leaf _ = Leaf
+ 7 | zipWith f _ Leaf = Leaf
+ 8 | zipWith f (Node x lx rx) (Node y ly ry)
+ 9 |   = Node (f x y) (zipWith f lx ly) (zipWith f rx ry)
+         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Possible correct results:
+    conArg (implicitly bound at Issue34:8:12--8:16)
+    conArg (implicitly bound at Issue34:8:27--8:31)

tests/idris2/error/error029/run

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

tests/idris2/interactive/interactive042/expected

@@ -30,7 +30,7 @@ Error: While processing right hand side of f. When unifying:
     Either b b
 and:
     Either b b
-Mismatch between: b (implicitly bound at Issue35-2:2:1--2:14) and b.
+Mismatch between: b (implicitly bound at Issue35-2:2:1--2:2) and b.
 
 Issue35-2:2:13--2:14
  1 | f : { a, b : Type } -> Either a b -> Either b a
@@ -42,7 +42,7 @@ Error: While processing right hand side of f. When unifying:
     Either b {b:826}
 and:
     Either {b:826} b
-Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:14) and b.
+Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:2) and b.
 
 Issue35-2:2:13--2:14
  1 | f : { a, b : Type } -> Either a b -> Either b a
@@ -54,7 +54,7 @@ Error: While processing right hand side of f. When unifying:
     Prelude.Either b {b:826}
 and:
     Prelude.Either {b:826} b
-Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:14) and b.
+Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:2) and b.
 
 Issue35-2:2:13--2:14
  1 | f : { a, b : Type } -> Either a b -> Either b a

tests/idris2/interface/interface016/expected

@@ -10,5 +10,5 @@ TwoNum:4:7--4:8
            ^
 
 Possible correct results:
-    conArg (implicitly bound at TwoNum:4:3--4:8)
-    conArg (implicitly bound at TwoNum:2:1--4:8)
+    conArg (implicitly bound at TwoNum:4:3--4:4)
+    conArg (implicitly bound at TwoNum:2:1--2:2)