From 340cf980acea3387675ca3a822cbfeefdaaa329b Mon Sep 17 00:00:00 2001
From: Viktor Yudov <me@spcfox.com>
Date: Wed, 22 Jan 2025 09:49:11 +0300
Subject: [PATCH 1/3] [ fix ] Remove lambdas from top-level methods

---
 src/Idris/Elab/Interface.idr                  |  17 +-
 tests/base/deriving_foldable/expected         |   2 +-
 tests/base/deriving_functor/expected          |  14 +-
 tests/base/deriving_show/expected             |   2 +-
 tests/base/deriving_traversable/expected      |   2 +-
 tests/idris2/basic/basic044/expected          |  14 +-
 tests/idris2/error/error018/expected          |   2 +-
 tests/idris2/evaluator/evaluator002/expected  | 150 +++++++++---------
 .../idris2/evaluator/interpreter008/expected  |   6 +-
 .../interactive/interactive042/expected       |  18 +--
 .../interface/interface035/Issue3474.idr      |   2 +
 tests/idris2/interface/interface035/expected  |   1 +
 tests/idris2/interface/interface035/run       |   3 +
 tests/idris2/misc/lazy003/expected            |   6 +-
 14 files changed, 115 insertions(+), 124 deletions(-)
 create mode 100644 tests/idris2/interface/interface035/Issue3474.idr
 create mode 100644 tests/idris2/interface/interface035/expected
 create mode 100644 tests/idris2/interface/interface035/run

diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr
index 35c2d9dc98..3f89252ba9 100644
--- a/src/Idris/Elab/Interface.idr
+++ b/src/Idris/Elab/Interface.idr
@@ -191,17 +191,13 @@ 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)))
+                                  (IVar EmptyFC (methName sig.name.val))
          let fndef = IDef vfc cn.val [fnclause]
          pure [tydecl, fndef]
   where
@@ -219,17 +215,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
diff --git a/tests/base/deriving_foldable/expected b/tests/base/deriving_foldable/expected
index ec503347d8..e199896c2e 100644
--- a/tests/base/deriving_foldable/expected
+++ b/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
diff --git a/tests/base/deriving_functor/expected b/tests/base/deriving_functor/expected
index 01e5b22b93..471584249d 100644
--- a/tests/base/deriving_functor/expected
+++ 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)
diff --git a/tests/base/deriving_show/expected b/tests/base/deriving_show/expected
index 25f3abab7f..1d4505d4ed 100644
--- a/tests/base/deriving_show/expected
+++ b/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
diff --git a/tests/base/deriving_traversable/expected b/tests/base/deriving_traversable/expected
index db9137ffd7..105feda526 100644
--- a/tests/base/deriving_traversable/expected
+++ b/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:13924} = eq} a -> f (EqMap key {{conArg:13924} = 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)
diff --git a/tests/idris2/basic/basic044/expected b/tests/idris2/basic/basic044/expected
index d93f23fa89..dc8d92a3ac 100644
--- a/tests/idris2/basic/basic044/expected
+++ 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)
diff --git a/tests/idris2/error/error018/expected b/tests/idris2/error/error018/expected
index eecd82d312..5fd45f3809 100644
--- a/tests/idris2/error/error018/expected
+++ b/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 | 
diff --git a/tests/idris2/evaluator/evaluator002/expected b/tests/idris2/evaluator/evaluator002/expected
index 9a58fb3c9c..cd5b0dec33 100644
--- a/tests/idris2/evaluator/evaluator002/expected
+++ b/tests/idris2/evaluator/evaluator002/expected
@@ -1,89 +1,89 @@
 1/2: Building Lib (Lib.idr)
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2554}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
-LOG eval.stuck.outofscope:5: Stuck function: {_:2556}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2549}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
+LOG eval.stuck.outofscope:5: Stuck function: {_:2551}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2552}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2552}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2552}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
+LOG eval.stuck.outofscope:5: Stuck function: {_:2560}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2561}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
-LOG eval.stuck.outofscope:5: Stuck function: {_:2565}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2566}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
 LOG eval.stuck.outofscope:5: Stuck function: Prelude.Types.List.reverse
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2585}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
-LOG eval.stuck.outofscope:5: Stuck function: {_:2589}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2590}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2593}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2593}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2580}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
+LOG eval.stuck.outofscope:5: Stuck function: {_:2584}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2585}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2586}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2586}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2586}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2588}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2588}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.accMapAux
 2/2: Building Main (Main.idr)
-LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2590}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2590}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2590}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2594}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2594}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2594}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2597}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2597}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2597}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
 LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2616}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2616}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2611}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2611}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.accMap
 Main> LOG eval.stuck:5: Stuck function: Lib.accMapAux
 LOG eval.stuck:5: Stuck function: Lib.accMapAux
diff --git a/tests/idris2/evaluator/interpreter008/expected b/tests/idris2/evaluator/interpreter008/expected
index 7849d94f57..1bfa48a4f4 100644
--- a/tests/idris2/evaluator/interpreter008/expected
+++ b/tests/idris2/evaluator/interpreter008/expected
@@ -1,6 +1,6 @@
 1/1: Building Issue2041 (Issue2041.idr)
 Error: Unsolved holes:
-Main.{n:820} introduced at: 
+Main.{n:817} introduced at: 
 Issue2041:5:17--5:19
  1 | ex : {n : Nat} -> String
  2 | ex {n} = "hello" ++ show n
@@ -9,8 +9,8 @@ Issue2041:5:17--5:19
  5 | main = putStrLn ex
                      ^^
 
-Main> Encountered unimplemented hole Main.{n:820}
-Warning: compiling hole Main.{n:820}
+Main> Encountered unimplemented hole Main.{n:817}
+Warning: compiling hole Main.{n:817}
 Main> Encountered unimplemented hole Main.{n:4}
 Warning: compiling hole Main.{n:4}
 Main> 
diff --git a/tests/idris2/interactive/interactive042/expected b/tests/idris2/interactive/interactive042/expected
index 385ca5b84e..d431b9d125 100644
--- a/tests/idris2/interactive/interactive042/expected
+++ b/tests/idris2/interactive/interactive042/expected
@@ -12,17 +12,17 @@ Main>  0 m : Nat
 ------------------------------
 help : Vect (S (plus n m)) a
 Main> Main>    a : Nat
-   eq : {a:822} = a
+   eq : {a:819} = a
 ------------------------------
 a : Nat
 Main>  0 m : Nat
  0 a : Type
    x : a
-   xs : Vect {n:871} a
+   xs : Vect {n:868} a
    ys : Vect m a
  0 n : Nat
 ------------------------------
-help : Vect (S (plus {n:871} m)) a
+help : Vect (S (plus {n:868} m)) a
 Main> 
 Bye for now!
 1/1: Building Issue35-2 (Issue35-2.idr)
@@ -39,10 +39,10 @@ Issue35-2:2:13--2:14
 
 1/1: Building Issue35-2 (Issue35-2.idr)
 Error: While processing right hand side of f. When unifying:
-    Either b {b:821}
+    Either b {b:818}
 and:
-    Either {b:821} b
-Mismatch between: {b:821} (implicitly bound at Issue35-2:2:1--2:2) and b.
+    Either {b:818} b
+Mismatch between: {b:818} (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
@@ -51,10 +51,10 @@ Issue35-2:2:13--2:14
 
 1/1: Building Issue35-2 (Issue35-2.idr)
 Error: While processing right hand side of f. When unifying:
-    Prelude.Either b {b:821}
+    Prelude.Either b {b:818}
 and:
-    Prelude.Either {b:821} b
-Mismatch between: {b:821} (implicitly bound at Issue35-2:2:1--2:2) and b.
+    Prelude.Either {b:818} b
+Mismatch between: {b:818} (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
diff --git a/tests/idris2/interface/interface035/Issue3474.idr b/tests/idris2/interface/interface035/Issue3474.idr
new file mode 100644
index 0000000000..49bccd1b08
--- /dev/null
+++ b/tests/idris2/interface/interface035/Issue3474.idr
@@ -0,0 +1,2 @@
+interface Fail1 where
+  f : Type -> {_ : Type} -> Type
diff --git a/tests/idris2/interface/interface035/expected b/tests/idris2/interface/interface035/expected
new file mode 100644
index 0000000000..7a5d041ece
--- /dev/null
+++ b/tests/idris2/interface/interface035/expected
@@ -0,0 +1 @@
+1/1: Building Issue3474 (Issue3474.idr)
diff --git a/tests/idris2/interface/interface035/run b/tests/idris2/interface/interface035/run
new file mode 100644
index 0000000000..397c9aaf55
--- /dev/null
+++ b/tests/idris2/interface/interface035/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Issue3474.idr
diff --git a/tests/idris2/misc/lazy003/expected b/tests/idris2/misc/lazy003/expected
index 4c5174f352..fcc120e3c5 100644
--- a/tests/idris2/misc/lazy003/expected
+++ b/tests/idris2/misc/lazy003/expected
@@ -7,8 +7,8 @@ Refers to: Builtin.Unit
 Flags: covering
 Main> Main.f6
 Arguments []
-Compile time tree: Delay (\u1, {u2:834} => u1)
-Compiled: Delay Lazy (\u1=> \{u2:834}=> u1)
+Compile time tree: Delay (\u1, {u2:831} => u1)
+Compiled: Delay Lazy (\u1=> \{u2:831}=> u1)
 Refers to: Builtin.Unit
 Flags: covering
 Main> Main.switch3
@@ -19,7 +19,7 @@ Compiled: \ {arg:0} => let f = Force Lazy (Main.switch {arg:0}) in
 \{lamc:0}=> case {lamc:0} of
   { Builtin.MkPair {tag = 0} [cons] {e:2} {e:3} => case {e:3} of  { Builtin.MkPair {tag = 0} [cons] {e:6} {e:7} => Builtin.MkPair {tag = 0} [cons] (f {e:2}) (Builtin.MkPair {tag = 0} [cons] (f {e:6}) (f {e:7}))}
   }
-Refers to: Main.case block in switch3, Main.{_:980}, Main.switch, Builtin.Pair, Prelude.Types.Nat
+Refers to: Main.case block in switch3, Main.{_:977}, Main.switch, Builtin.Pair, Prelude.Types.Nat
 Refers to (runtime): Main.switch, Builtin.MkPair
 Flags: covering
 Size change:

From 249fc16834f8731dc22335d1ed5e8eff6911eef7 Mon Sep 17 00:00:00 2001
From: Viktor Yudov <me@spcfox.com>
Date: Wed, 22 Jan 2025 19:05:08 +0300
Subject: [PATCH 2/3] [ fix ] Add eta expand implicits in top-level methods

---
 src/Idris/Elab/Interface.idr                  |  33 +++-
 tests/base/deriving_traversable/expected      |   2 +-
 tests/idris2/evaluator/evaluator002/expected  | 164 +++++++++---------
 .../interface/interface035/Issue3474.idr      |  11 +-
 4 files changed, 119 insertions(+), 91 deletions(-)

diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr
index 3f89252ba9..d848098198 100644
--- a/src/Idris/Elab/Interface.idr
+++ b/src/Idris/Elab/Interface.idr
@@ -191,13 +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 fnclause = PatClause vfc
-                                  (INamedApp vfc
-                                             (IVar cn.fc cn.val) -- See #3409
-                                             (UN $ Basic "__con")
-                                             conapp
-                                             )
-                                  (IVar EmptyFC (methName sig.name.val))
+
+         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 piNames lhs
+         -- Do the same for the rhs
+         let rhs = namesToRawImp piNames rhs
+
+         let fnclause = PatClause vfc lhs rhs
          let fndef = IDef vfc cn.val [fnclause]
          pure [tydecl, fndef]
   where
@@ -223,6 +232,16 @@ 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 : List Name -> RawImp -> RawImp
+    namesToRawImp (nm@(UN{}) :: xs) fn = namesToRawImp xs (INamedApp vfc fn nm (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 : _} ->
diff --git a/tests/base/deriving_traversable/expected b/tests/base/deriving_traversable/expected
index 105feda526..6651d78a3a 100644
--- a/tests/base/deriving_traversable/expected
+++ b/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:13924} = eq} a -> f (EqMap key {{conArg:13924} = 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)
diff --git a/tests/idris2/evaluator/evaluator002/expected b/tests/idris2/evaluator/evaluator002/expected
index cd5b0dec33..bd2b052254 100644
--- a/tests/idris2/evaluator/evaluator002/expected
+++ b/tests/idris2/evaluator/evaluator002/expected
@@ -1,89 +1,89 @@
 1/2: Building Lib (Lib.idr)
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2549}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
-LOG eval.stuck.outofscope:5: Stuck function: {_:2551}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2552}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2552}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2552}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
-LOG eval.stuck.outofscope:5: Stuck function: {_:2560}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2561}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2527}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2528}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2528}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2528}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2528}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2528}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2527}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2527}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2527}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2531}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2528}
+LOG eval.stuck.outofscope:5: Stuck function: {_:2533}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2534}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2534}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2534}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2535}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2536}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2536}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2536}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2536}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2536}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2535}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2535}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2535}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2539}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2539}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2539}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2539}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2539}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2536}
+LOG eval.stuck.outofscope:5: Stuck function: {_:2542}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2543}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2544}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2544}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2544}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2547}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2547}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2547}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2547}
 LOG eval.stuck.outofscope:5: Stuck function: Prelude.Types.List.reverse
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2580}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
-LOG eval.stuck.outofscope:5: Stuck function: {_:2584}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2585}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2586}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2586}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2586}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2588}
-LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2588}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2562}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
+LOG eval.stuck.outofscope:5: Stuck function: {_:2566}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2567}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2568}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2568}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2568}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
+LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.accMapAux
 2/2: Building Main (Main.idr)
-LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2590}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2590}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2590}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2594}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2594}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2594}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2597}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2597}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2597}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2611}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2611}
-LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2572}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2572}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2572}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2576}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2576}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2576}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2579}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2579}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2579}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2582}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2582}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2584}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2582}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2582}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2593}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2593}
+LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2573}
 LOG eval.stuck.outofscope:5: Stuck function: Lib.accMap
 Main> LOG eval.stuck:5: Stuck function: Lib.accMapAux
 LOG eval.stuck:5: Stuck function: Lib.accMapAux
diff --git a/tests/idris2/interface/interface035/Issue3474.idr b/tests/idris2/interface/interface035/Issue3474.idr
index 49bccd1b08..1ede47ae3f 100644
--- a/tests/idris2/interface/interface035/Issue3474.idr
+++ b/tests/idris2/interface/interface035/Issue3474.idr
@@ -1,2 +1,11 @@
+interface Ok1 where
+  fOk : Type -> Type -> Type
+
 interface Fail1 where
-  f : Type -> {_ : Type} -> Type
+  fFail : Type -> {_ : Type} -> Type
+
+interface Ok2 where
+  gOk : (x : Type) -> Type
+
+interface Fail2 where
+  gFail : {x : Type} -> Type

From 74124b848b5c2f5668f2dcc49e62e25ea2ffb675 Mon Sep 17 00:00:00 2001
From: Viktor Yudov <me@spcfox.com>
Date: Wed, 22 Jan 2025 21:47:14 +0300
Subject: [PATCH 3/3] [ fix ] Add `IBindVar` in LHS in eta-expand for
 interfaces

---
 src/Idris/Elab/Interface.idr | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr
index d848098198..43b6ba53b3 100644
--- a/src/Idris/Elab/Interface.idr
+++ b/src/Idris/Elab/Interface.idr
@@ -202,9 +202,9 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
          -- 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 piNames lhs
+         let lhs = namesToRawImp True piNames lhs
          -- Do the same for the rhs
-         let rhs = namesToRawImp piNames rhs
+         let rhs = namesToRawImp False piNames rhs
 
          let fnclause = PatClause vfc lhs rhs
          let fndef = IDef vfc cn.val [fnclause]
@@ -238,9 +238,13 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
     collectImplicitNames (IPi _ _ _        Nothing  _ ty) = collectImplicitNames ty
     collectImplicitNames _                                = []
 
-    namesToRawImp : List Name -> RawImp -> RawImp
-    namesToRawImp (nm@(UN{}) :: xs) fn = namesToRawImp xs (INamedApp vfc fn nm (IVar vfc nm))
-    namesToRawImp _                 fn = fn
+    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.