Introduce implicit resolution pass

hkmc2/jvm/src/test/scala/hkmc2/MLsDiffMaker.scala

@@ -6,6 +6,7 @@ import mlscript.utils.*, shorthands.*
 import utils.*
 
 import hkmc2.semantics.Elaborator
+import hkmc2.semantics.ImplicitResolver
 
 
 abstract class MLsDiffMaker extends DiffMaker:
@@ -34,11 +35,14 @@ abstract class MLsDiffMaker extends DiffMaker:
   val silent = NullaryCommand("silent")
   val dbgElab = NullaryCommand("de")
   val dbgParsing = NullaryCommand("dp")
+  val dbgResolving = NullaryCommand("dr")
 
   val showParse = NullaryCommand("p")
   val showParsedTree = DebugTreeCommand("pt")
   val showElab = NullaryCommand("el")
   val showElaboratedTree = DebugTreeCommand("elt")
+  val showResolve = NullaryCommand("r")
+  val showResolvedTree = DebugTreeCommand("rt")
   val showLoweredTree = NullaryCommand("lot")
   val ppLoweredTree = NullaryCommand("slot")
   val showContext = NullaryCommand("ctx")
@@ -56,6 +60,7 @@ abstract class MLsDiffMaker extends DiffMaker:
     override def dbg: Bool =
       dbgParsing.isSet
       || dbgElab.isSet
+      || dbgResolving.isSet
       || debug.isSet
 
   val etl = new TraceLogger:
@@ -68,9 +73,13 @@ abstract class MLsDiffMaker extends DiffMaker:
       // * Perhaps this should be the default behavior of TraceLogger.
       if doTrace then super.trace(pre, post)(thunk)
       else thunk
+
+  val rtl = new TraceLogger:
+    override def doTrace = dbgResolving.isSet
+    override def emitDbg(str: String): Unit = output(str)
 
   var curCtx = Elaborator.State.init
-
+  var curICtx = ImplicitResolver.ICtx.empty
 
   override def run(): Unit =
     if file =/= preludeFile then importFile(preludeFile, verbose = false)
@@ -187,6 +196,16 @@ abstract class MLsDiffMaker extends DiffMaker:
     showElaboratedTree.get.foreach: post =>
       output(s"Elaborated tree:")
       output(e.showAsTree(using post))
+
+    val resolver = ImplicitResolver(rtl)
+    curICtx = resolver.resolveBlk(e)(using curICtx)
+
+    if showResolve.isSet then
+      output(s"Resolved: ${e.showDbg}")
+    showResolvedTree.get.foreach: post =>
+      output(s"Resolved tree:")
+      output(e.showAsTree(using post))
+
     processTerm(e, inImport = false)
 
 

hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala

@@ -420,13 +420,13 @@ class BBTyper(using elState: Elaborator.State, tl: TL, scope: Scope):
             effBuff += eff
             ctx += sym -> rhsTy
             goStats(stats)
-          case TermDefinition(_, Fun, sym, ps :: Nil, sig, Some(body), _, _, _) :: stats =>
+          case TermDefinition(_, Fun, sym, ps :: Nil, _, sig, Some(body), _, _, _) :: stats =>
             typeFunDef(sym, Term.Lam(ps, body), sig, ctx)
             goStats(stats)
-          case TermDefinition(_, Fun, sym, Nil, sig, Some(body), _, _, _) :: stats =>
+          case TermDefinition(_, Fun, sym, Nil, _, sig, Some(body), _, _, _) :: stats =>
             typeFunDef(sym, body, sig, ctx)  // * may be a case expressions
             goStats(stats)
-          case TermDefinition(_, Fun, sym, _, S(sig), None, _, _, _) :: stats =>
+          case TermDefinition(_, Fun, sym, _, _, S(sig), None, _, _, _) :: stats =>
             ctx += sym -> typeType(sig)
             goStats(stats)
           case (clsDef: ClassDef) :: stats =>

hkmc2/shared/src/main/scala/hkmc2/codegen/Lowering.scala

@@ -82,6 +82,14 @@ class Lowering(using TL, Raise, Elaborator.State):
             case sem.Fld(flags, value, asc) =>
               TODO("Other argument forms")
             case spd: Spd => true -> spd.term
+            case ca: sem.CtxArg => ca.term match
+              case S(t) => 
+                false -> t
+              case N => 
+                // All contextual arguments should have been
+                // populated by implicit resolution before lowering.
+                // Fail silently.
+                false -> Term.Error
           val l = new TempSymbol(S(t))
             def rec(as: Ls[Bool -> st], asr: Ls[Arg]): Block = as match
               case Nil => k(Call(fr, asr.reverse)(isMlsFun))
@@ -103,6 +111,7 @@ class Lowering(using TL, Raise, Elaborator.State):
         subTerm(prefix): p =>
           conclude(Select(p, nme)(sel.sym))
       case _ => subTerm(f)(conclude)
+    case st.TyApp(lhs, _) => term(lhs)(k)
     case st.Blk(Nil, res) => term(res)(k)
     case st.Blk(Lit(Tree.UnitLit(true)) :: stats, res) =>
       subTerm(st.Blk(stats, res))(k)
@@ -131,6 +140,12 @@ class Lowering(using TL, Raise, Elaborator.State):
             val (paramLists, bodyBlock) = setupFunctionDef(td.params, bod, S(td.sym.nme))
             Define(FunDefn(td.sym, paramLists, bodyBlock),
               term(st.Blk(stats, res))(k))
+          case syntax.Ins =>
+            // Implciit instances are not parameterized for now.
+            assert(td.params.isEmpty)
+            subTerm(bod)(r =>
+              Define(ValDefn(td.owner, syntax.ImmutVal, td.sym, r),
+                term(st.Blk(stats, res))(k)))
       // case cls: ClassDef =>
       case cls: ClassLikeDef =>
         reportAnnotations(cls, cls.annotations)

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

@@ -180,10 +180,11 @@ extends Importer:
       else Term.SynthSel(trm, Ident("class"))(mem.clsTree.orElse(mem.modTree).map(_.symbol))
     case _ => trm
 
-  def term(tree: Tree, inAppPrefix: Bool = false): Ctxl[Term] =
+  def term(tree: Tree, inAppPrefix: Bool = false, inTyAppPrefix: Bool = false): Ctxl[Term] =
   trace[Term](s"Elab term ${tree.showDbg}", r => s"~> $r"):
     def maybeModuleMethodApp(t: Term): Ctxl[Term] =
-      if !inAppPrefix then moduleMethodApp(t)
+      if !inAppPrefix && !inTyAppPrefix 
+      then moduleMethodApp(t)
       else t
     tree.desugared match
     case Bra(k, e) =>
@@ -250,8 +251,8 @@ extends Importer:
         case N =>
           raise(ErrorReport(msg"Name not found: $name" -> tree.toLoc :: Nil))
           Term.Error
-    case TyApp(lhs, targs) =>
-      Term.TyApp(term(lhs), targs.map {
+    case TyApp(lhs, targs) => maybeModuleMethodApp:
+      Term.TyApp(term(lhs, inTyAppPrefix = true), targs.map {
         case Modified(Keyword.`in`, inLoc, arg) => Term.WildcardTy(S(term(arg)), N)
         case Modified(Keyword.`out`, outLoc, arg) => Term.WildcardTy(N, S(term(arg)))
         case Tup(Modified(Keyword.`in`, inLoc, arg1) :: Modified(Keyword.`out`, outLoc, arg2) :: Nil) =>
@@ -725,10 +726,10 @@ extends Importer:
           case trm => raise(WarningReport(msg"Terms in handler block do nothing" -> trm.toLoc :: Nil))
 
         val tds = elabed.stats.map {
-          case td @ TermDefinition(owner, Fun, sym, params, sign, body, resSym, flags, annotations) =>
+          case td @ TermDefinition(owner, Fun, sym, params, tparams, sign, body, resSym, flags, annotations) =>
             params.reverse match
               case ParamList(_, value :: Nil, _) :: newParams =>
-                val newTd = TermDefinition(owner, Fun, sym, newParams.reverse, sign, body, resSym, flags, annotations)
+                val newTd = TermDefinition(owner, Fun, sym, newParams.reverse, tparams, sign, body, resSym, flags, annotations)
                 S(HandlerTermDefinition(value.sym, newTd))
               case _ => 
                 raise(ErrorReport(msg"Handler function is missing resumption parameter" -> td.toLoc :: Nil))
@@ -778,7 +779,9 @@ extends Importer:
             val tdf = ctx.nest(N).givenIn:
               // * Add type parameters to context
               val (tps, newCtx1) = td.typeParams match
-                case S(t) => typeParams(t)
+                case S(t) => 
+                  val (tps, ctx) = typeParams(t)
+                  (S(tps), ctx)
                 case N => (N, ctx)
               // * Add parameters to context
               val (pss, newCtx) =
@@ -801,7 +804,7 @@ extends Importer:
                   case Nil if k is Fun =>
                     ParamList(ParamListFlags.empty, Nil, N) :: Nil
                   case _ => pss
-              val tdf = TermDefinition(owner, k, sym, real_pss, s, b, r, 
+              val tdf = TermDefinition(owner, k, sym, real_pss, tps, s, b, r, 
                 TermDefFlags.empty.copy(isModMember = isModMember), annotations)
               sym.defn = S(tdf)
 
@@ -1043,7 +1046,7 @@ extends Importer:
   def computeVariances(s: Statement): Unit =
     val trav = VarianceTraverser()
     def go(s: Statement): Unit = s match
-      case TermDefinition(_, k, sym, pss, sign, body, r, _, _) =>
+      case TermDefinition(_, k, sym, pss, _, sign, body, r, _, _) =>
         pss.foreach(ps => ps.params.foreach(trav.traverseType(S(false))))
         sign.foreach(trav.traverseType(S(true)))
         body match