[ fix #3474 ] Fix implicit arguments in interface methods

src/Idris/Elab/Interface.idr

@@ -191,17 +191,22 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
                                       (MkImpTy vfc cn ty_imp))
          let conapp = apply (IVar vfc cname)
                             (map (IBindVar EmptyFC) (map bindName allmeths))
-         let argns = getExplicitArgs 0 sig.type
-         -- eta expand the RHS so that we put implicits in the right place
-         let fnclause = PatClause vfc
-                                  (INamedApp vfc
-                                             (IVar cn.fc cn.val) -- See #3409
-                                             (UN $ Basic "__con")
-                                             conapp
-                                             )
-                                  (mkLam argns
-                                    (apply (IVar EmptyFC (methName sig.name.val))
-                                           (map (IVar EmptyFC) argns)))
+
+         let lhs = INamedApp vfc
+                             (IVar cn.fc cn.val) -- See #3409
+                             (UN $ Basic "__con")
+                             conapp
+         let rhs = IVar EmptyFC (methName sig.name.val)
+
+         -- EtaExpand implicits on both sides:
+         -- First, obtain all the implicit names in the prefix of
+         let piNames = collectImplicitNames sig.type
+         -- Then apply names for each argument to the lhs
+         let lhs = namesToRawImp True piNames lhs
+         -- Do the same for the rhs
+         let rhs = namesToRawImp False piNames rhs
+
+         let fnclause = PatClause vfc lhs rhs
          let fndef = IDef vfc cn.val [fnclause]
          pure [tydecl, fndef]
   where
@@ -219,17 +224,6 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
     applyCon n = let name = UN (Basic "__con") in
                  (n, INamedApp vfc (IVar vfc n) name (IVar vfc name))
 
-    getExplicitArgs : Int -> RawImp -> List Name
-    getExplicitArgs i (IPi _ _ Explicit n _ sc)
-        = MN "arg" i :: getExplicitArgs (i + 1) sc
-    getExplicitArgs i (IPi _ _ _ n _ sc) = getExplicitArgs i sc
-    getExplicitArgs i tm = []
-
-    mkLam : List Name -> RawImp -> RawImp
-    mkLam [] tm = tm
-    mkLam (x :: xs) tm
-       = ILam EmptyFC top Explicit (Just x) (Implicit vfc False) (mkLam xs tm)
-
     bindName : Name -> String
     bindName (UN n) = "__bind_" ++ displayUserName n
     bindName (NS _ n) = bindName n
@@ -238,6 +232,20 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
     methName : Name -> Name
     methName n = UN (Basic $ bindName n)
 
+    collectImplicitNames : RawImp -> List Name
+    collectImplicitNames (IPi _ _ Explicit _        _ ty) = []
+    collectImplicitNames (IPi _ _ _        (Just n) _ ty) = n :: collectImplicitNames ty
+    collectImplicitNames (IPi _ _ _        Nothing  _ ty) = collectImplicitNames ty
+    collectImplicitNames _                                = []
+
+    namesToRawImp : Bool -> List Name -> RawImp -> RawImp
+    namesToRawImp bind (nm@(UN{}) :: xs) fn =
+      namesToRawImp bind xs $ INamedApp vfc fn nm $
+        if bind
+           then IBindVar vfc $ nameRoot nm
+           else IVar vfc nm
+    namesToRawImp _    _                 fn = fn
+
 -- Get the function for chasing a constraint. This is one of the
 -- arguments to the record, appearing before the method arguments.
 getConstraintHint : {vars : _} ->

tests/base/deriving_foldable/expected

@@ -65,7 +65,7 @@ LOG derive.foldable.clauses:1:
   foldMapIVect : {0 m : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> IVect {n = m} a -> b
   foldMapIVect f (MkIVect x2) = foldMap f x2
 LOG derive.foldable.clauses:1: 
-  foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5699} = eq} a -> b
+  foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5696} = eq} a -> b
   foldMapEqMap f (MkEqMap x3) = foldMap (foldMap f) x3
 LOG derive.foldable.clauses:1: 
   foldMapTree : {0 l : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> Tree l a -> b

tests/base/deriving_functor/expected

@@ -21,7 +21,7 @@ LOG derive.functor.clauses:1:
 LOG derive.functor.clauses:1: 
   mapBigTree : {0 a, b : Type} -> (a -> b) -> BigTree a -> BigTree b
   mapBigTree f (End x1) = End (f x1)
-  mapBigTree f (Branch x1 x2 x3) = Branch x1 (map f x2) (\ {arg:4042} => mapBigTree f (x3 {arg:4042}))
+  mapBigTree f (Branch x1 x2 x3) = Branch x1 (map f x2) (\ {arg:4039} => mapBigTree f (x3 {arg:4039}))
   mapBigTree f (Rose x1) = Rose (map (assert_total (mapBigTree f)) x1)
 LOG derive.functor.clauses:1: 
   mapMatrix : {0 m, n : _} -> {0 a, b : Type} -> (a -> b) -> Matrix m n a -> Matrix m n b
@@ -59,7 +59,7 @@ LOG derive.functor.clauses:1:
 LOG derive.functor.clauses:1: 
   mapFree : {0 f : _} -> {0 a, b : Type} -> (a -> b) -> Free f a -> Free f b
   mapFree f (Pure x2) = Pure (f x2)
-  mapFree f (Bind x3 x4) = Bind x3 (\ {arg:5071} => mapFree f (x4 {arg:5071}))
+  mapFree f (Bind x3 x4) = Bind x3 (\ {arg:5068} => mapFree f (x4 {arg:5068}))
 LOG derive.functor.assumption:10: I am assuming that the parameter m is a Functor
 LOG derive.functor.clauses:1: 
   mapMaybeT : {0 m : _} -> Functor m => {0 a, b : Type} -> (a -> b) -> MaybeT m a -> MaybeT m b
@@ -75,20 +75,20 @@ LOG derive.functor.clauses:1:
   mapIVect : {0 m : _} -> {0 a, b : Type} -> (a -> b) -> IVect {n = m} a -> IVect {n = m} b
   mapIVect f (MkIVect x2) = MkIVect (map f x2)
 LOG derive.functor.clauses:1: 
-  mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5684} = eq} a -> EqMap key {{conArg:5684} = eq} b
+  mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5681} = eq} a -> EqMap key {{conArg:5681} = eq} b
   mapEqMap f (MkEqMap x3) = MkEqMap (map (map f) x3)
 LOG derive.functor.clauses:1: 
   mapCont : {0 r : _} -> {0 a, b : Type} -> (a -> b) -> Cont r a -> Cont r b
-  mapCont f (MkCont x2) = MkCont (\ {arg:6040} => x2 (\ {arg:6042} => {arg:6040} (f {arg:6042})))
+  mapCont f (MkCont x2) = MkCont (\ {arg:6037} => x2 (\ {arg:6039} => {arg:6037} (f {arg:6039})))
 LOG derive.functor.clauses:1: 
   mapCont2 : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2 r e a -> Cont2 r e b
-  mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6132} => \ {arg:6139} => x3 {arg:6132} (\ {arg:6141} => {arg:6139} (f {arg:6141})))
+  mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6129} => \ {arg:6136} => x3 {arg:6129} (\ {arg:6138} => {arg:6136} (f {arg:6138})))
 LOG derive.functor.clauses:1: 
   mapCont2' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2' r e a -> Cont2' r e b
-  mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6246} => x3 (mapFst (\ t => \ {arg:6248} => t (f {arg:6248})) {arg:6246}))
+  mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6243} => x3 (mapFst (\ t => \ {arg:6245} => t (f {arg:6245})) {arg:6243}))
 LOG derive.functor.clauses:1: 
   mapCont2'' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2'' r e a -> Cont2'' r e b
-  mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6370} => x3 (Delay (mapFst (\ t => \ {arg:6373} => t (Delay (f {arg:6373}))) {arg:6370})))
+  mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6367} => x3 (Delay (mapFst (\ t => \ {arg:6370} => t (Delay (f {arg:6370}))) {arg:6367})))
 LOG derive.functor.clauses:1: 
   mapWithImplicits : {0 a, b : Type} -> (a -> b) -> WithImplicits a -> WithImplicits b
   mapWithImplicits f (MkImplicit {x = x1} x2) = MkImplicit {x = f x1} (f x2)

tests/base/deriving_show/expected

@@ -81,7 +81,7 @@ LOG derive.show.clauses:1:
 LOG derive.show.assumption:10: I am assuming that the parameter key can be shown
 LOG derive.show.assumption:10: I am assuming that the parameter val can be shown
 LOG derive.show.clauses:1: 
-  showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5120} = eq} val -> String
+  showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5117} = eq} val -> String
   showPrecEqMap d (MkEqMap x0) = showCon d "MkEqMap" (showArg x0)
 LOG derive.show.clauses:1: 
   showPrecX : Prec -> X -> String

tests/base/deriving_traversable/expected

@@ -65,7 +65,7 @@ LOG derive.traversable.clauses:1:
   traverseIVect : {0 m : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> IVect {n = m} a -> f (IVect {n = m} b)
   traverseIVect f (MkIVect x2) = MkIVect <$> (traverse f x2)
 LOG derive.traversable.clauses:1: 
-  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13929} = eq} a -> f (EqMap key {{conArg:13929} = eq} b)
+  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13906} = eq} a -> f (EqMap key {{conArg:13906} = eq} b)
   traverseEqMap f (MkEqMap x3) = MkEqMap <$> (traverse (traverse f) x3)
 LOG derive.traversable.clauses:1: 
   traverseTree : {0 l : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree l a -> f (Tree l b)

tests/idris2/basic/basic044/expected

@@ -117,33 +117,33 @@ Target type : ({arg:1} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:3:
 $resolved6
 $resolved7
-Target type : ?Vec.{a:4569}_[]
+Target type : ?Vec.{a:4541}_[]
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:4:
 (($resolved3 ((:: (fromInteger 0)) Nil)) Nil)
 (($resolved4 ((:: (fromInteger 0)) Nil)) Nil)
 (($resolved5 ((:: (fromInteger 0)) Nil)) Nil)
-Target type : (Vec.Vec ?Vec.{a:4569}_[] ?Vec.{n:4568}_[])
+Target type : (Vec.Vec ?Vec.{a:4541}_[] ?Vec.{n:4540}_[])
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:5:
 (($resolved3 (fromInteger 0)) Nil)
 (($resolved4 (fromInteger 0)) Nil)
 (($resolved5 (fromInteger 0)) Nil)
-Target type : ?Vec.{a:4572}_[]
+Target type : ?Vec.{a:4544}_[]
 LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
   ($resolved1 0)
   ($resolved2 0)
-With default. Target type : ?Vec.{a:4574}_[]
+With default. Target type : ?Vec.{a:4546}_[]
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:7:
 $resolved6
 $resolved7
-Target type : (Vec.Vec ?Vec.{a:4574}_[] ?Vec.{n:4573}_[])
+Target type : (Vec.Vec ?Vec.{a:4546}_[] ?Vec.{n:4545}_[])
 LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
   ($resolved1 0)
   ($resolved2 0)
-With default. Target type : ?Vec.{a:4573}_[]
+With default. Target type : ?Vec.{a:4545}_[]
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:8:
 $resolved6
 $resolved7
-Target type : (Vec.Vec ?Vec.{a:4572}_[] ?Vec.{n:4571}_[])
+Target type : (Vec.Vec ?Vec.{a:4544}_[] ?Vec.{n:4543}_[])
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:5:
 (($resolved4 (fromInteger 0)) Nil)
 Target type : (Prelude.Basics.List Prelude.Types.Nat)

tests/idris2/error/error018/expected

@@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7
 
 1/1: Building Issue1031-4 (Issue1031-4.idr)
 Error: While processing left hand side of nice. Unsolved holes:
-Main.{dotTm:815} introduced at: 
+Main.{dotTm:812} introduced at: 
 Issue1031-4:4:6--4:10
  1 | %default total
  2 |