Support introducing instances via implicit parameters

hkmc2/shared/src/main/scala/hkmc2/semantics/ImplicitResolver.scala

@@ -7,6 +7,8 @@ import hkmc2.semantics.Elaborator.State
 import hkmc2.syntax.Ins
 import hkmc2.ErrorReport
 import hkmc2.Message.MessageContext
+import hkmc2.syntax.Tree.TermDef
+import hkmc2.syntax.Fun
 
 case class CtxArgImpl(private val param: Param) extends CtxArg:
 
@@ -42,14 +44,12 @@ class ImplicitResolver(val tl: TraceLogger)
   import ImplicitResolver.ICtx
 
   def resolve(t: Term)(using ictx: ICtx): Unit = 
-  trace[Unit](s"Resolving term: $t", * => s"~> $t"):
     t match
       case blk: Term.Blk => resolveBlk(blk)
       case Term.Tup(elem) => elem.foreach(resolveElem(_))
       case _ => t.subTerms.foreach(resolve(_))
 
   def resolveElem(elem: Elem)(using ictx: ICtx): Unit = 
-  trace[Unit](s"Resolving elem: $elem", * => s"~> $elem"):
     elem match
       case arg @ CtxArgImpl(param) => 
         log(s"Resolving context argument: $param")
@@ -76,16 +76,31 @@ class ImplicitResolver(val tl: TraceLogger)
         log(s"Resolving statement: $stmt")
         given newICtx: ICtx = stmt match
           case t @ TermDefinition(_, Ins, sym, _, sign, _, _, _) => 
-            log(s"Resolving instance $t")
+            log(s"Resolving instance definition $t")
             sign match
               case N =>
                 raise(ErrorReport(msg"Missing signature for instance ${t.toString}" -> N :: Nil))
                 ictx
               case Some(sign) =>
                 ictx + (sign, sym)
-          case _ => ictx
+          case t @ TermDefinition(_, Fun, _, pss, _, _, _, _) =>
+            given newICtx: ICtx = pss
+            .filter(_.flags.ctx)
+            .foldLeft(ictx): (ictx, ps) => 
+              ps.params.foldLeft(ictx): (ictx, p) => 
+                log(s"Resolving instance parameter $p")
+                p.sign match
+                  case None => 
+                    raise(ErrorReport(msg"Missing signature for instance ${t.toString}" -> N :: Nil))
+                    ictx
+                  case Some(sign) => 
+                    ictx + (sign, p.sym)
+            t.subTerms.foreach(resolve(_))
+            ictx
+          case _ => 
+            stmt.subTerms.foreach(resolve(_))
+            ictx
 
-        stmt.subTerms.foreach(resolve(_))
         go(rest)
 
     given newICtx: ICtx = go(blk.stats)(using ictx)