diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala
index f2b2e610d5..d22df4460a 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala
@@ -407,13 +407,13 @@ class BBTyper(using elState: Elaborator.State, tl: TL):
             effBuff += eff
             nestCtx += sym -> rhsTy
             goStats(stats)
-          case TermDefinition(_, Fun, sym, ParamList(_, ps) :: Nil, sig, Some(body), _) :: stats =>
+          case TermDefinition(_, Fun, sym, ParamList(_, 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 =>
diff --git a/hkmc2/shared/src/main/scala/hkmc2/codegen/Lowering.scala b/hkmc2/shared/src/main/scala/hkmc2/codegen/Lowering.scala
index c2b38db9c0..b808e1d751 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/codegen/Lowering.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/codegen/Lowering.scala
@@ -68,6 +68,7 @@ class Lowering(using TL, Raise, Elaborator.State):
       case Tup(fs) =>
         val as = fs.map:
           case sem.Fld(sem.FldFlags.empty, value, N) => value
+          case sem.Fld(sem.FldFlags(false, false, false, true), value, N) => value
           case sem.Fld(flags, value, asc) =>
             TODO("Other argument forms")
         val l = new TempSymbol(summon[Elaborator.State].nextUid, S(t))
diff --git a/hkmc2/shared/src/main/scala/hkmc2/codegen/js/JSBuilder.scala b/hkmc2/shared/src/main/scala/hkmc2/codegen/js/JSBuilder.scala
index 3fc098f5cc..b9c86e748b 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/codegen/js/JSBuilder.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/codegen/js/JSBuilder.scala
@@ -187,7 +187,7 @@ class JSBuilder extends CodeBuilder:
                     } + ")""""
                 }; }"""
               } #}  # }"
-            if clsDefn.kind is syntax.Mod then
+            if (clsDefn.kind is syntax.Mod) || (clsDefn.kind is syntax.Obj) then
               val clsTmp = summon[Scope].allocateName(new semantics.TempSymbol(0/*TODO rm this useless param*/, N, sym.nme+"$"+"class"))
               clsDefn.owner match
               case S(owner) =>
diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala
index 7de34a13b7..3649378c3e 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala
@@ -259,7 +259,34 @@ extends Importer:
       term(rhs)
     case tree @ App(lhs, rhs) =>
       val sym = FlowSymbol("‹app-res›", nextUid)
-      Term.App(term(lhs), term(rhs))(tree, sym)
+      val lt = term(lhs)
+      val rt = term(rhs)
+
+      // Check if module arguments match module parameters
+      val args = rt match
+        case Term.Tup(fields) => S(fields)
+        case _ => N
+      val params = lt.symbol
+        .collect:
+          case sym: BlockMemberSymbol => sym.trmTree
+        .flatten
+        .collect:
+          case td: TermDef => td.paramLists.headOption
+        .flatten
+      for
+        (args, params) <- (args zip params)
+        (arg, param) <- (args zip params.fields)
+      do 
+        val argMod = arg.flags.mod
+        val paramMod = param match
+          case Tree.TypeDef(Mod, _, N, N) => true
+          case _ => false
+        if argMod && !paramMod then raise:
+          ErrorReport:
+            msg"Only module parameters may receive module arguments (values)." -> 
+            arg.toLoc :: Nil
+      
+      Term.App(lt, rt)(tree, sym)
     case Sel(pre, nme) =>
       val preTrm = term(pre)
       val sym = resolveField(nme, preTrm.symbol, nme)
@@ -300,6 +327,8 @@ extends Importer:
       Term.Throw(term(body))
     case Modified(Keyword.`do`, kwLoc, body) =>
       Term.Blk(term(body) :: Nil, unit)
+    case TypeDef(Mod, head, N, N) =>
+      term(head)
     case Tree.Region(id: Tree.Ident, body) =>
       val sym = VarSymbol(id, nextUid)
       val nestCtx = ctx + (id.name -> sym)
@@ -354,7 +383,12 @@ extends Importer:
   def fld(tree: Tree): Ctxl[Fld] = tree match
     case InfixApp(lhs, Keyword.`:`, rhs) =>
       Fld(FldFlags.empty, term(lhs), S(term(rhs)))
-    case _ => Fld(FldFlags.empty, term(tree), N)
+    case _ => 
+      val t = term(tree)
+      val flags = FldFlags.empty
+      if ModuleChecker.evalsToModule(t) 
+      then Fld(flags.copy(mod = true), t, N)
+      else Fld(flags, t, N)
   
   def unit: Term.Lit = Term.Lit(UnitLit(true))
   
@@ -385,7 +419,10 @@ extends Importer:
           raise(ErrorReport(msg"Multiple declarations of symbol '$name'" -> N ::
             decls.map(msg"declared here" -> _.toLoc)))
         val sig = decls.collectFirst:
-          case td if td.signature.isDefined => td.signature.get
+          case td
+            if td.annotatedResultType.isDefined
+            && td.paramLists.isEmpty
+            => td.annotatedResultType.get
         sig.foreach: sig =>
           newSignatureTrees += name -> sig
     
@@ -503,29 +540,61 @@ extends Importer:
           case R(id) =>
             val sym = members.getOrElse(id.name, die)
             val owner = ctx.outer
+            val isModMember = owner.exists(_.isInstanceOf[ModuleSymbol])
             val tdf = ctx.nest(N).givenIn:
               // * Add type parameters to context
               val (tps, newCtx1) = td.typeParams match
                 case S(t) => typeParams(t)
                 case N => (N, ctx)
               // * Add parameters to context
-              val (pss, newCtx) = 
+              val (pss, newCtx) =
                 td.paramLists.foldLeft(Ls[ParamList](), newCtx1):
                   case ((pss, ctx), ps) => 
                     val (qs, newCtx) = params(ps)(using ctx)
                     (pss :+ ParamList(ParamListFlags.empty, qs), newCtx)
+              // * Elaborate signature
+              val st = td.annotatedResultType.orElse(newSignatureTrees.get(id.name))
+              val s = st.map(term(_)(using newCtx))
               val b = rhs.map(term(_)(using newCtx))
               val r = FlowSymbol(s"‹result of ${sym}›", nextUid)
-              val tdf = TermDefinition(owner, k, sym, pss,
-                td.signature.orElse(newSignatureTrees.get(id.name)).map(term), b, r)
+              val tdf = TermDefinition(owner, k, sym, pss, s, b, r, 
+                TermDefFlags.empty.copy(isModMember = isModMember))
               sym.defn = S(tdf)
+              
+              // indicates if the function really returns a module
+              val em = b.exists(ModuleChecker.evalsToModule)
+              // indicates if the function marks its result as "module"
+              val mm = st match
+                case Some(TypeDef(Mod, _, N, N)) => true
+                case _ => false
+              
+              // checks rules regarding module methods
+              s match
+                case N if em => raise:
+                  ErrorReport:
+                    msg"Function returning module values must have explicit return types." ->
+                    td.head.toLoc :: Nil
+                case S(t) if em && ModuleChecker.isTypeParam(t) => raise:
+                  ErrorReport:
+                    msg"Function returning module values must have concrete return types." ->
+                    td.head.toLoc :: Nil
+                case S(_) if em && !mm => raise:
+                  ErrorReport:
+                    msg"The return type of functions returning module values must be prefixed with module keyword." ->
+                    td.head.toLoc :: Nil
+                case S(_) if mm && !isModMember => raise:
+                  ErrorReport:
+                    msg"Only module methods may return module values." ->
+                    td.head.toLoc :: Nil
+                case _ => ()
+              
               tdf
             go(sts, tdf :: acc)
           case L(d) =>
             raise(d)
             go(sts, acc)
       case (td @ TypeDef(k, head, extension, body)) :: sts =>
-        assert((k is Als) || (k is Cls) || (k is Mod), k)
+        assert((k is Als) || (k is Cls) || (k is Mod) || (k is Obj), k)
         val nme = td.name match
           case R(id) => id
           case L(d) =>
@@ -577,7 +646,7 @@ extends Importer:
               semantics.TypeDef(alsSym, tps, extension.map(term), N)
             alsSym.defn = S(d)
             d
-        case Mod =>
+        case k: (Mod.type | Obj.type) =>
           val clsSym = td.symbol.asInstanceOf[ModuleSymbol] // TODO: improve `asInstanceOf`
           val owner = ctx.outer
           newCtx.nest(S(clsSym)).givenIn:
@@ -588,7 +657,7 @@ extends Importer:
                 // case S(t) => block(t :: Nil)
                 case S(t) => ???
                 case N => (new Term.Blk(Nil, Term.Lit(UnitLit(true))), ctx)
-              ModuleDef(owner, clsSym, tps, ps, ObjBody(bod))
+              ModuleDef(owner, clsSym, tps, ps, k, ObjBody(bod))
             clsSym.defn = S(cd)
             cd
         case Cls =>
@@ -612,7 +681,6 @@ extends Importer:
         // TODO: pass abstract to `go`
         go(body :: sts, acc)
       case Modified(Keyword.`declare`, absLoc, body) :: sts =>
-        ???
         // TODO: pass declare to `go`
         go(body :: sts, acc)
       case (result: Tree) :: Nil =>
@@ -631,8 +699,18 @@ extends Importer:
     if ctx.outer.isDefined then TermSymbol(k, ctx.outer, id)
     else VarSymbol(id, nextUid)
   
-  def param(t: Tree): Ctxl[Ls[Param]] = t.param.map: (p, t) =>
-    Param(FldFlags.empty, fieldOrVarSym(ParamBind, p), t.map(term))
+  def param(t: Tree): Ctxl[Ls[Param]] = t match
+    case TypeDef(Mod, inner, N, N) =>
+      val ps = param(inner).map(p => p.copy(flags = p.flags.copy(mod = true)))
+      for p <- ps if p.flags.mod do p.sign match
+        case N =>
+          raise(ErrorReport(msg"Module parameters must have explicit types." -> t.toLoc :: Nil))
+        case S(ret) if ModuleChecker.isTypeParam(ret) => 
+          raise(ErrorReport(msg"Module parameters must have concrete types." -> t.toLoc :: Nil))
+        case _ => ()
+      ps
+    case _ => t.param.map: (p, t) =>
+      Param(FldFlags.empty, fieldOrVarSym(ParamBind, p), t.map(term))
   
   def params(t: Tree): Ctxl[(Ls[Param], Ctx)] = t match
     case Tup(ps) =>
@@ -681,7 +759,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
@@ -699,11 +777,36 @@ extends Importer:
     while trav.changed do
       trav.changed = false
       go(s)
+  
+  object ModuleChecker:
+    
+    /** Checks if a term is a reference to a type parameter. */
+    def isTypeParam(t: Term): Bool = t.symbol
+      .filter(_.isInstanceOf[VarSymbol])
+      .flatMap(_.asInstanceOf[VarSymbol].decl)
+      .exists(_.isInstanceOf[TyParam])
     
+    /** Checks if a term evaluates to a module value. */
+    def evalsToModule(t: Term): Bool = 
+      def isModule(t: Tree): Bool = t match
+        case TypeDef(Mod, _, _, _) => true
+        case _ => false
+      def returnsModule(t: TermDef): Bool = t.annotatedResultType match
+        case S(TypeDef(Mod, _, N, N)) => true
+        case _ => false
+      t match
+        case Term.Blk(_, res) => evalsToModule(res)
+        case Term.App(lhs, rhs) => lhs.symbol match
+          case S(sym: BlockMemberSymbol) => sym.trmTree.exists(returnsModule)
+          case _ => false
+        case t => t.symbol match
+          case S(sym: BlockMemberSymbol) => sym.modTree.exists(isModule)
+          case _ => false
+  
   class VarianceTraverser(var changed: Bool = true) extends Traverser:
     override def traverseType(pol: Pol)(trm: Term): Unit = trm match
       case Term.TyApp(lhs, targs) =>
-        lhs.symbol.flatMap(_.asTpe) match
+        lhs.symbol.flatMap(sym => sym.asTpe orElse sym.asMod) match
           case S(sym: ClassSymbol) =>
             sym.defn match
             case S(td: ClassDef) =>
@@ -715,6 +818,17 @@ extends Importer:
                   if !tp.isCovariant then traverseType(pol.!)(targ)
             case N =>
               // TODO(sym->sym.uid)
+          case S(sym: ModuleSymbol) =>
+            sym.defn match
+            case S(td: ModuleDef) =>
+              if td.tparams.sizeCompare(targs) =/= 0 then
+                raise(ErrorReport(msg"Wrong number of type arguments" -> trm.toLoc :: Nil)) // TODO BE
+              td.tparams.zip(targs).foreach:
+                case (tp, targ) =>
+                  if !tp.isContravariant then traverseType(pol)(targ)
+                  if !tp.isCovariant then traverseType(pol.!)(targ)
+            case N =>
+              // TODO(sym->sym.uid)
           case S(sym: TypeAliasSymbol) =>
             // TODO dedup with above...
             sym.defn match
diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala
index f6810b4cd6..0c55b67a4b 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala
@@ -96,7 +96,7 @@ class BlockMemberSymbol(val nme: Str, val trees: Ls[Tree]) extends MemberSymbol[
   def clsTree: Opt[Tree.TypeDef] = trees.collectFirst:
     case t: Tree.TypeDef if t.k is Cls => t
   def modTree: Opt[Tree.TypeDef] = trees.collectFirst:
-    case t: Tree.TypeDef if t.k is Mod => t
+    case t: Tree.TypeDef if (t.k is Mod) || (t.k is Obj) => t
   def alsTree: Opt[Tree.TypeDef] = trees.collectFirst:
     case t: Tree.TypeDef if t.k is Als => t
   def trmTree: Opt[Tree.TermDef] = trees.collectFirst:
diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala
index ae1f3b642f..bf0ec27275 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala
@@ -3,6 +3,7 @@ package semantics
 
 import mlscript.utils.*, shorthands.*
 import syntax.*
+import scala.collection.mutable.Buffer
 
 
 final case class QuantVar(sym: VarSymbol, ub: Opt[Term], lb: Opt[Term])
@@ -104,7 +105,7 @@ sealed trait Statement extends AutoLocated:
     case RegRef(reg, value) => reg :: value :: Nil
     case Assgn(lhs, rhs) => lhs :: rhs :: Nil
     case Deref(term) => term :: Nil
-    case TermDefinition(_, k, _, ps, sign, body, res) =>
+    case TermDefinition(_, k, _, ps, sign, body, res, _) =>
       ps.toList.flatMap(_.subTerms) ::: sign.toList ::: body.toList
     case cls: ClassDef =>
       cls.paramsOpt.toList.flatMap(_.flatMap(_.subTerms)) ::: cls.body.blk :: Nil
@@ -123,6 +124,7 @@ sealed trait Statement extends AutoLocated:
     case t: Tup => t.tree :: Nil
     case l: Lam => l.params.map(_.sym.id) ::: l.body :: Nil
     case t: App => t.tree :: Nil
+    case Sel(pre, nme) => pre :: nme :: Nil
     case SelProj(prefix, cls, proj) => prefix :: cls :: proj :: Nil
     case _ =>
       subTerms // TODO more precise (include located things that aren't terms)
@@ -171,7 +173,7 @@ sealed trait Statement extends AutoLocated:
     case CompType(lhs, rhs, pol) => s"${lhs.showDbg} ${if pol then "|" else "&"} ${rhs.showDbg}"
     case Error => "<error>"
     case Tup(fields) => fields.map(_.showDbg).mkString("[", ", ", "]")
-    case TermDefinition(_, k, sym, ps, sign, body, res) => s"${k.str} ${sym}${
+    case TermDefinition(_, k, sym, ps, sign, body, res, flags) => s"${flags} ${k.str} ${sym}${
       ps.map(_.showDbg).mkString("")
     }${sign.fold("")(": "+_.showDbg)}${
       body match
@@ -188,6 +190,15 @@ final case class LetDecl(sym: LocalSymbol) extends Statement
 
 final case class DefineVar(sym: LocalSymbol, rhs: Term) extends Statement
 
+final case class TermDefFlags(isModMember: Bool):
+  def showDbg: Str = 
+    val flags = Buffer.empty[String]
+    if isModMember then flags += "module"
+    flags.mkString(" ")
+  override def toString: String = "‹" + showDbg + "›"
+
+object TermDefFlags { val empty: TermDefFlags = TermDefFlags(false) }
+
 final case class TermDefinition(
     owner: Opt[InnerSymbol],
     k: TermDefKind,
@@ -196,6 +207,7 @@ final case class TermDefinition(
     sign: Opt[Term],
     body: Opt[Term],
     resSym: FlowSymbol,
+    flags: TermDefFlags,
 ) extends Companion
 
 case class ObjBody(blk: Term.Blk):
@@ -226,9 +238,14 @@ sealed abstract class ClassLikeDef extends TypeLikeDef:
   val body: ObjBody
 
 
-case class ModuleDef(owner: Opt[InnerSymbol], sym: ModuleSymbol, tparams: Ls[TyParam], paramsOpt: Opt[Ls[Param]], body: ObjBody) extends ClassLikeDef with Companion:
-  self =>
-  val kind: ClsLikeKind = Mod
+case class ModuleDef(
+  owner: Opt[InnerSymbol], 
+  sym: ModuleSymbol, 
+  tparams: Ls[TyParam], 
+  paramsOpt: Opt[Ls[Param]], 
+  kind: ClsLikeKind,
+  body: ObjBody,
+) extends ClassLikeDef with Companion
 
 
 sealed abstract class ClassDef extends ClassLikeDef:
@@ -278,8 +295,14 @@ case class TypeDef(
 
 
 // TODO Store optional source locations for the flags instead of booleans
-final case class FldFlags(mut: Bool, spec: Bool, genGetter: Bool):
-  def showDbg: Str = (if mut then "mut " else "") + (if spec then "spec " else "") + (if genGetter then "val " else "")
+final case class FldFlags(mut: Bool, spec: Bool, genGetter: Bool, mod: Bool):
+  def showDbg: Str = 
+    val flags = Buffer.empty[String]
+    if mut then flags += "mut"
+    if spec then flags += "spec"
+    if genGetter then flags += "gen"
+    if mod then flags += "module"
+    flags.mkString(" ")
   override def toString: String = "‹" + showDbg + "›"
 
 final case class Fld(flags: FldFlags, value: Term, asc: Opt[Term]) extends FldImpl
@@ -303,7 +326,7 @@ final case class Param(flags: FldFlags, sym: LocalSymbol & NamedSymbol, sign: Op
   // def showDbg: Str = flags.showDbg + sym.name + ": " + sign.showDbg
   def showDbg: Str = flags.showDbg + sym + sign.fold("")(": " + _.showDbg)
 
-object FldFlags { val empty: FldFlags = FldFlags(false, false, false) }
+object FldFlags { val empty: FldFlags = FldFlags(false, false, false, false) }
 
 final case class ParamListFlags(ctx: Bool):
   def showDbg: Str = (if ctx then "ctx " else "")
diff --git a/hkmc2/shared/src/main/scala/hkmc2/syntax/Keyword.scala b/hkmc2/shared/src/main/scala/hkmc2/syntax/Keyword.scala
index aea7c20635..69e03eee88 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/syntax/Keyword.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/syntax/Keyword.scala
@@ -93,7 +93,8 @@ object Keyword:
   val `super` = Keyword("super", N, N)
   val `new` = Keyword("new", N, curPrec) // TODO: check the prec
   // val `namespace` = Keyword("namespace", N, N)
-  val `module` = Keyword("module", N, N)
+  val `module` = Keyword("module", N, curPrec)
+  val `object` = Keyword("object", N, curPrec)
   val `open` = Keyword("open", N, curPrec)
   val `type` = Keyword("type", N, N)
   val `where` = Keyword("where", N, N)
diff --git a/hkmc2/shared/src/main/scala/hkmc2/syntax/ParseRule.scala b/hkmc2/shared/src/main/scala/hkmc2/syntax/ParseRule.scala
index ff7a88fe20..80cf92659c 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/syntax/ParseRule.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/syntax/ParseRule.scala
@@ -271,6 +271,7 @@ object ParseRule:
     Kw(`class`)(typeDeclBody(Cls)),
     Kw(`trait`)(typeDeclBody(Trt)),
     Kw(`module`)(typeDeclBody(Mod)),
+    Kw(`object`)(typeDeclBody(Obj)),
     Kw(`open`):
       ParseRule("'open' keyword")(
         exprOrBlk(ParseRule("'open' declaration")(End(()))){
diff --git a/hkmc2/shared/src/main/scala/hkmc2/syntax/Tree.scala b/hkmc2/shared/src/main/scala/hkmc2/syntax/Tree.scala
index 8e62f3fc80..b7258fead0 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/syntax/Tree.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/syntax/Tree.scala
@@ -203,6 +203,7 @@ case object Trt extends TypeDefKind("trait") with ObjDefKind
 case object Mxn extends TypeDefKind("mixin")
 case object Als extends TypeDefKind("type alias")
 case object Mod extends TypeDefKind("module") with ClsLikeKind
+case object Obj extends TypeDefKind("object") with ClsLikeKind
 
 
 
@@ -215,7 +216,7 @@ trait TypeOrTermDef:
   
   def head: Tree
   
-  lazy val (symbName, name, paramLists, typeParams, signature)
+  lazy val (symbName, name, paramLists, typeParams, annotatedResultType)
       : (Opt[Tree], Diagnostic \/ Ident, Ls[Tup], Opt[TyTup], Opt[Tree]) =
     def rec(t: Tree, symbName: Opt[Tree]): 
       (Opt[Tree], Diagnostic \/ Ident, Ls[Tup], Opt[TyTup], Opt[Tree]) = 
@@ -231,7 +232,7 @@ trait TypeOrTermDef:
       // fun f[T](n1: Int): Int
       // fun f[T](n1: Int)(nn: Int): Int
       case InfixApp(Apps(App(id: Ident, typeParams: TyTup), paramLists), Keyword.`:`, ret) =>
-        (symbName, R(id), paramLists, S(typeParams), N)
+        (symbName, R(id), paramLists, S(typeParams), S(ret))
       
       case InfixApp(Jux(lhs, rhs), Keyword.`:`, ret) =>
         rec(InfixApp(rhs, Keyword.`:`, ret), S(lhs))
@@ -275,7 +276,7 @@ trait TypeDefImpl extends TypeOrTermDef:
   
   lazy val symbol = k match
     case Cls => semantics.ClassSymbol(this, name.getOrElse(Ident("<error>")))
-    case Mod => semantics.ModuleSymbol(this, name.getOrElse(Ident("<error>")))
+    case Mod | Obj => semantics.ModuleSymbol(this, name.getOrElse(Ident("<error>")))
     case Als => semantics.TypeAliasSymbol(name.getOrElse(Ident("<error>")))
     case Trt | Mxn => ???
   
diff --git a/hkmc2/shared/src/main/scala/hkmc2/utils/utils.scala b/hkmc2/shared/src/main/scala/hkmc2/utils/utils.scala
index fce0cf38a0..c60fa81c06 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/utils/utils.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/utils/utils.scala
@@ -20,6 +20,7 @@ extension (s: String)
     .mkString("\"", "", "\"")
 
 
+import hkmc2.semantics.TermDefFlags
 import hkmc2.semantics.FldFlags
 import scala.collection.mutable.Buffer
 import mlscript.utils.StringOps
@@ -36,12 +37,17 @@ extension (t: Product)
       case Nil => "Nil"
       case xs: List[_] => "Ls of \n" + xs.iterator.map(aux(_)).mkString("\n").indent("  ")
       case s: String => s.escaped
-      case FldFlags(mut, spec, genGetter) =>
+      case TermDefFlags(mod) =>
+        val flags = Buffer.empty[String]
+        if mod then flags += "module"
+        flags.mkString("(", ", ", ")")
+      case FldFlags(mut, spec, genGetter, mod) =>
         val flags = Buffer.empty[String]
         if mut then flags += "mut"
         if spec then flags += "spec"
         if genGetter then flags += "gen"
-        if flags.isEmpty then "()" else flags.mkString("(", ", ", ")")
+        if mod then flags += "module"
+        flags.mkString("(", ", ", ")")
       case Loc(start, end, origin) =>
         val (sl, _, sc) = origin.fph.getLineColAt(start)
         val (el, _, ec) = origin.fph.getLineColAt(end)
diff --git a/hkmc2/shared/src/test/mlscript-compile/Option.mls b/hkmc2/shared/src/test/mlscript-compile/Option.mls
index d9fd67aeb6..59edab71fd 100644
--- a/hkmc2/shared/src/test/mlscript-compile/Option.mls
+++ b/hkmc2/shared/src/test/mlscript-compile/Option.mls
@@ -9,7 +9,7 @@ open Predef
 module Option with ...
 
 class Some(value)
-module None
+object None
 
 fun isDefined(x) = if x is
   Some then true
diff --git a/hkmc2/shared/src/test/mlscript-compile/Stack.mls b/hkmc2/shared/src/test/mlscript-compile/Stack.mls
index 8a55364f18..08e20e6793 100644
--- a/hkmc2/shared/src/test/mlscript-compile/Stack.mls
+++ b/hkmc2/shared/src/test/mlscript-compile/Stack.mls
@@ -5,7 +5,7 @@
 module Stack with ...
 
 class (::) Cons[A](head: A, tail)
-module Nil
+object Nil
 
 fun isEmpty(xs) = xs is Nil
 
diff --git a/hkmc2/shared/src/test/mlscript/basics/GenericClasses.mls b/hkmc2/shared/src/test/mlscript/basics/GenericClasses.mls
index 16a624b9ae..2b989aa2c3 100644
--- a/hkmc2/shared/src/test/mlscript/basics/GenericClasses.mls
+++ b/hkmc2/shared/src/test/mlscript/basics/GenericClasses.mls
@@ -31,7 +31,7 @@ class Foo[A] with
 class Foo[A](x: Foo[A, A])
 //│ ╔══[ERROR] Wrong number of type arguments
 //│ ║  l.31: 	class Foo[A](x: Foo[A, A])
-//│ ╙──      	                    ^^^^
+//│ ╙──      	                ^^^^^^^^
 
 :fixme
 :e
@@ -39,5 +39,5 @@ class Foo[A](x: Bar[A])
 class Bar(x: Foo[Int])
 //│ ╔══[ERROR] Wrong number of type arguments
 //│ ║  l.38: 	class Foo[A](x: Bar[A])
-//│ ╙──      	                    ^
+//│ ╙──      	                ^^^^^
 
diff --git a/hkmc2/shared/src/test/mlscript/basics/ModuleMethods.mls b/hkmc2/shared/src/test/mlscript/basics/ModuleMethods.mls
new file mode 100644
index 0000000000..38d2821420
--- /dev/null
+++ b/hkmc2/shared/src/test/mlscript/basics/ModuleMethods.mls
@@ -0,0 +1,94 @@
+:js
+
+class C with
+  // regular method foo
+  fun foo(x) = x
+
+module M with
+  // module method foo
+  fun foo(x) = x
+  // module method self
+  fun self(): module M = M
+
+:e
+fun f1(module m)
+//│ ╔══[ERROR] Module parameters must have explicit types.
+//│ ║  l.14: 	fun f1(module m)
+//│ ╙──      	              ^
+
+:e
+fun f2[T](module m: T)
+//│ ╔══[ERROR] Module parameters must have concrete types.
+//│ ║  l.20: 	fun f2[T](module m: T)
+//│ ╙──      	                 ^^^^
+
+:e
+module N with
+  fun f3() = M
+//│ ╔══[ERROR] Function returning module values must have explicit return types.
+//│ ║  l.27: 	  fun f3() = M
+//│ ╙──      	      ^^^^
+
+:e
+module N with
+  fun f4[T](): module T = M
+//│ ╔══[ERROR] Function returning module values must have concrete return types.
+//│ ║  l.34: 	  fun f4[T](): module T = M
+//│ ╙──      	      ^^^^^^^^^^^^^^^^^
+
+:e
+module N with
+  fun f5(): M = M
+//│ ╔══[ERROR] The return type of functions returning module values must be prefixed with module keyword.
+//│ ║  l.41: 	  fun f5(): M = M
+//│ ╙──      	      ^^^^^^^
+
+
+fun f6(m: M) = m
+
+:e
+f6(M)
+//│ ╔══[ERROR] Only module parameters may receive module arguments (values).
+//│ ║  l.50: 	f6(M)
+//│ ╙──      	   ^
+//│ = M { class: [class M] }
+
+:e
+f6(M.self())
+//│ ╔══[ERROR] Only module parameters may receive module arguments (values).
+//│ ║  l.57: 	f6(M.self())
+//│ ╙──      	   ^^^^^^^^
+//│ = M { class: [class M] }
+
+:e
+fun f7(): module M
+//│ ╔══[ERROR] Only module methods may return module values.
+//│ ║  l.64: 	fun f7(): module M
+//│ ╙──      	    ^^^^^^^^^^^^^^
+
+
+:todo // should be an error
+:e
+fun f8(module m: M) = m
+
+:e
+fun f9(module m: M): module M = m
+//│ ╔══[ERROR] Only module methods may return module values.
+//│ ║  l.75: 	fun f9(module m: M): module M = m
+//│ ╙──      	    ^^^^^^^^^^^^^^^^^^^^^^^^^
+
+module Test with
+  fun ok1(module m: M): module M = m
+
+let ok1 = Test.ok1
+//│ ok1 = [Function: ok1]
+
+module N with
+  fun ok2(): module M = M
+
+ok1(M)
+//│ = M { class: [class M] }
+
+ok1(M.self())
+//│ = M { class: [class M] }
+
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls
index ff242227c5..138bc7b901 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls
@@ -110,7 +110,9 @@ fun h: [C] -> ([A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B
 
 :e
 bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A
-//│ ═══[ERROR] Cannot type non-function term Sel(Ref(globalThis:block#16),Ident(bazbaz)) as (<α>35_2) ->{⊥} (forall α34_3: α34_3) ->{⊥} <α>35_2
+//│ ╔══[ERROR] Cannot type non-function term Sel(Ref(globalThis:block#16),Ident(bazbaz)) as (<α>35_2) ->{⊥} (forall α34_3: α34_3) ->{⊥} <α>35_2
+//│ ║  l.112: 	bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A
+//│ ╙──       	^^^^^^
 //│ Type: forall α33_2: (α33_2) ->{⊥} (forall α34_3: α33_2 -> α33_2) ->{⊥} α33_2
 //│ Where:
 //│   α33_2 <: Int
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls
index 60e3733f79..8f016cb360 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls
@@ -118,7 +118,9 @@ fun baz(z) =
 
 :e
 baz: Int -> (([A] -> A -> A), Int) -> Int
-//│ ═══[ERROR] Cannot type non-function term Sel(Ref(globalThis:block#17),Ident(baz)) as (Int) ->{⊥} (forall α25_2: (α25_2) ->{⊥} α25_2, Int) ->{⊥} Int
+//│ ╔══[ERROR] Cannot type non-function term Sel(Ref(globalThis:block#17),Ident(baz)) as (Int) ->{⊥} (forall α25_2: (α25_2) ->{⊥} α25_2, Int) ->{⊥} Int
+//│ ║  l.120: 	baz: Int -> (([A] -> A -> A), Int) -> Int
+//│ ╙──       	^^^
 //│ Type: ⊥
 
 
@@ -128,7 +130,7 @@ baz(42)
 :e
 baz(42): (([A] -> A -> A), Int) -> Int
 //│ ╔══[ERROR] Cannot type non-function term App(Sel(Ref(globalThis:block#17),Ident(baz)),Tup(List(Fld(‹›,Lit(IntLit(42)),None)))) as (forall α26_2: (α26_2) ->{⊥} α26_2, Int) ->{⊥} Int
-//│ ║  l.129: 	baz(42): (([A] -> A -> A), Int) -> Int
+//│ ║  l.131: 	baz(42): (([A] -> A -> A), Int) -> Int
 //│ ╙──       	^^^^^^^
 //│ Type: ⊥
 
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls b/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls
index 02164a7b70..cc6c72e4ab 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbErrors.mls
@@ -40,6 +40,8 @@ inc("oops")
 fun inc(x) = x + 1
 inc : Int
 //│ ╔══[ERROR] Type error in selection with expected type Int
+//│ ║  l.41: 	inc : Int
+//│ ║        	^^^
 //│ ╙── because: cannot constrain  α12_1 -> Int  <:  Int
 //│ Type: Int
 
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls
index 16e8e71f22..73df402a63 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls
@@ -34,7 +34,9 @@ g(foo)
 
 :e
 y `=> (let t = run(x `=> x `+ y) in y)
-//│ ═══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ║  l.36: 	y `=> (let t = run(x `=> x `+ y) in y)
+//│ ╙──      	                            ^
 //│ Type: CodeBase[out α26_3 -> α26_3, ⊥, ?]
 
 class C[A](m: A, n: A -> Int)
@@ -67,6 +69,8 @@ f(g)(foo)
 :fixme // ???
 f(g)(bar)
 //│ ╔══[ERROR] Type error in selection with expected type α52_1
+//│ ║  l.70: 	f(g)(bar)
+//│ ║        	     ^^^
 //│ ╟── because: cannot constrain  C[Int]  <:  α52_1
 //│ ╟── because: cannot constrain  C[in D( Int ) out D( Int )]  <:  α52_1
 //│ ╟── because: cannot constrain  C[in D( Int ) out D( Int )]  <:  ¬C[in D() out ¬⊥] ∨ C[in D( Int ) out ¬⊥ ∧ α55_1]
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls
index 3437ec7f8d..70b4cd98d8 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls
@@ -7,7 +7,7 @@ fun power(x) = case
   0 then `1.0
   n then x `*. power(x)(n - 1)
 power
-//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@33),Lit(IntLit(0)),Else(Quoted(Lit(DecLit(1.0))))),Let(n@34,Ref(caseScrut@33),Else(Quoted(App(Ref(builtin:*),Tup(List(Fld(‹›,Unquoted(Ref(x@32)),None), Fld(‹›,Unquoted(App(App(Sel(Ref(globalThis:block#0),Ident(power)),Tup(List(Fld(‹›,Ref(x@32),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n@34),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),None)))))))) (of class hkmc2.semantics.Split$Cons)
+//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@34),Lit(IntLit(0)),Else(Quoted(Lit(DecLit(1.0))))),Let(n@35,Ref(caseScrut@34),Else(Quoted(App(Ref(builtin:*),Tup(List(Fld(‹›,Unquoted(Ref(x@32)),None), Fld(‹›,Unquoted(App(App(Sel(Ref(globalThis:block#0),Ident(power)),Tup(List(Fld(‹›,Ref(x@32),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n@35),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),None)))))))) (of class hkmc2.semantics.Split$Cons)
 
 
 fun id: [A] -> A -> A
@@ -16,7 +16,9 @@ fun id(x) = x
 
 :fixme // FIXME[CY]
 run(x `=> id(x) `* x)
-//│ ═══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(*))
+//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(*))
+//│ ║  l.18: 	run(x `=> id(x) `* x)
+//│ ╙──      	                 ^
 //│ Type: ⊤
 
 :fixme
@@ -38,7 +40,9 @@ show
 fun inc(dbg) =
   x `=> let c = x `+ `1 in let t = dbg(c) in c
 inc
-//│ ═══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ║  l.41: 	  x `=> let c = x `+ `1 in let t = dbg(c) in c
+//│ ╙──      	                   ^
 //│ Type: forall α34_2: (CodeBase[⊥, ?, ?] ->{α34_2} ⊤) ->{α34_2} CodeBase[out ⊤ -> ⊥, ⊥, ?]
 
 inc(c => log(show(c)))
@@ -53,7 +57,7 @@ fun body(x, y) = case
 fun gib_naive(n) =
   (x, y) `=> body(x, y)(n)
 let gn5 = run(gib_naive(5))
-//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@79),Lit(IntLit(0)),Else(Ref(x@77))),Cons(Branch(Ref(caseScrut@79),Lit(IntLit(1)),Else(Ref(y@78))),Let(n@80,Ref(caseScrut@79),Else(App(App(Sel(Ref(globalThis:block#7),Ident(body)),Tup(List(Fld(‹›,Ref(y@78),None), Fld(‹›,Quoted(App(Sel(Ref(globalThis:import#bbPredef),Ident(+)),Tup(List(Fld(‹›,Unquoted(Ref(x@77)),None), Fld(‹›,Unquoted(Ref(y@78)),None))))),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n@80),None), Fld(‹›,Lit(IntLit(1)),None)))),None)))))))) (of class hkmc2.semantics.Split$Cons)
+//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@82),Lit(IntLit(0)),Else(Ref(x@78))),Cons(Branch(Ref(caseScrut@82),Lit(IntLit(1)),Else(Ref(y@79))),Let(n@83,Ref(caseScrut@82),Else(App(App(Sel(Ref(globalThis:block#7),Ident(body)),Tup(List(Fld(‹›,Ref(y@79),None), Fld(‹›,Quoted(App(Sel(Ref(globalThis:import#bbPredef),Ident(+)),Tup(List(Fld(‹›,Unquoted(Ref(x@78)),None), Fld(‹›,Unquoted(Ref(y@79)),None))))),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n@83),None), Fld(‹›,Lit(IntLit(1)),None)))),None)))))))) (of class hkmc2.semantics.Split$Cons)
 
 fun bind(rhs, k) = `let x = rhs `in k(x)
 bind
@@ -66,7 +70,7 @@ fun body(x, y) = case
   0 then x
   1 then y
   n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out C, out Any]
-//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@107),Lit(IntLit(0)),Else(Ref(x@105))),Cons(Branch(Ref(caseScrut@107),Lit(IntLit(1)),Else(Ref(y@106))),Let(n@108,Ref(caseScrut@107),Else(App(Sel(Ref(globalThis:block#8),Ident(bind)),Tup(List(Fld(‹›,Quoted(App(Sel(Ref(globalThis:import#bbPredef),Ident(+)),Tup(List(Fld(‹›,Unquoted(Ref(x@105)),None), Fld(‹›,Unquoted(Ref(y@106)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z@111,None)),App(App(Sel(Ref(globalThis:block#9),Ident(body)),Tup(List(Fld(‹›,Ref(y@106),None), Fld(‹›,Ref(z@111),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n@108),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C@115,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Int)))), WildcardTy(None,Some(Ref(C@115))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))),TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Ref(C@115))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))))))))))) (of class hkmc2.semantics.Split$Cons)
+//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@109),Lit(IntLit(0)),Else(Ref(x@106))),Cons(Branch(Ref(caseScrut@109),Lit(IntLit(1)),Else(Ref(y@107))),Let(n@110,Ref(caseScrut@109),Else(App(Sel(Ref(globalThis:block#8),Ident(bind)),Tup(List(Fld(‹›,Quoted(App(Sel(Ref(globalThis:import#bbPredef),Ident(+)),Tup(List(Fld(‹›,Unquoted(Ref(x@106)),None), Fld(‹›,Unquoted(Ref(y@107)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z@113,None)),App(App(Sel(Ref(globalThis:block#9),Ident(body)),Tup(List(Fld(‹›,Ref(y@107),None), Fld(‹›,Ref(z@113),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n@110),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C@117,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Int)))), WildcardTy(None,Some(Ref(C@117))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))),TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Ref(C@117))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))))))))))) (of class hkmc2.semantics.Split$Cons)
 
 fun bind: [G] -> (CodeBase[out Int, out G, out Any], [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out Int, out C | G, out Any]) -> CodeBase[out Int, out G, out Any]
 fun bind(rhs, k) = `let x = rhs `in k(x)
@@ -81,7 +85,7 @@ fun body(x, y) = case
   1 then y
   n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out Int, out C, out Any]
 body
-//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@134),Lit(IntLit(0)),Else(Ref(x@132))),Cons(Branch(Ref(caseScrut@134),Lit(IntLit(1)),Else(Ref(y@133))),Let(n@135,Ref(caseScrut@134),Else(App(Sel(Ref(globalThis:block#10),Ident(bind)),Tup(List(Fld(‹›,Quoted(App(Sel(Ref(globalThis:import#bbPredef),Ident(+)),Tup(List(Fld(‹›,Unquoted(Ref(x@132)),None), Fld(‹›,Unquoted(Ref(y@133)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z@138,None)),App(App(Sel(Ref(globalThis:block#11),Ident(body)),Tup(List(Fld(‹›,Ref(y@133),None), Fld(‹›,Ref(z@138),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n@135),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C@142,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Int)))), WildcardTy(None,Some(Ref(C@142))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))),TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Int)))), WildcardTy(None,Some(Ref(C@142))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))))))))))) (of class hkmc2.semantics.Split$Cons)
+//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@136),Lit(IntLit(0)),Else(Ref(x@133))),Cons(Branch(Ref(caseScrut@136),Lit(IntLit(1)),Else(Ref(y@134))),Let(n@137,Ref(caseScrut@136),Else(App(Sel(Ref(globalThis:block#10),Ident(bind)),Tup(List(Fld(‹›,Quoted(App(Sel(Ref(globalThis:import#bbPredef),Ident(+)),Tup(List(Fld(‹›,Unquoted(Ref(x@133)),None), Fld(‹›,Unquoted(Ref(y@134)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z@140,None)),App(App(Sel(Ref(globalThis:block#11),Ident(body)),Tup(List(Fld(‹›,Ref(y@134),None), Fld(‹›,Ref(z@140),None)))),Tup(List(Fld(‹›,App(Sel(Ref(globalThis:import#bbPredef),Ident(-)),Tup(List(Fld(‹›,Ref(n@137),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C@144,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Int)))), WildcardTy(None,Some(Ref(C@144))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))),TyApp(Sel(Ref(globalThis:import#bbPredef),Ident(CodeBase)),List(WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Int)))), WildcardTy(None,Some(Ref(C@144))), WildcardTy(None,Some(Sel(Ref(globalThis:import#Prelude),Ident(Any)))))),None))))))))))) (of class hkmc2.semantics.Split$Cons)
 
 fun gib(n) = (x, y) `=> body(x, y)(n)
 let g5 = run(gib(5))
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls
index a05dbe1d96..e9043d2c26 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbQQ.mls
@@ -45,19 +45,27 @@ f `=> x `=> f`(x)
 
 :fixme // FIXME[CY]
 x `=> y `=> x `+ y
-//│ ═══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ║  l.47: 	x `=> y `=> x `+ y
+//│ ╙──      	               ^
 //│ Type: CodeBase[out ⊤ -> (⊤ -> ⊥), ⊥, ?]
 
 
 :fixme // FIXME[CY]
 (x, y) `=> x `+ y
-//│ ═══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ║  l.55: 	(x, y) `=> x `+ y
+//│ ╙──      	              ^
 //│ Type: CodeBase[out (⊤, ⊤) -> ⊥, ⊥, ?]
 
 :fixme // FIXME[CY]
 (x, y, z) `=> x `+ y `+ z
-//│ ═══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
-//│ ═══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ║  l.62: 	(x, y, z) `=> x `+ y `+ z
+//│ ╙──      	                      ^
+//│ ╔══[ERROR] Cannot quote Sel(Ref(globalThis:import#bbPredef),Ident(+))
+//│ ║  l.62: 	(x, y, z) `=> x `+ y `+ z
+//│ ╙──      	                 ^
 //│ Type: CodeBase[out (⊤, ⊤, ⊤) -> ⊥, ⊥, ?]
 
 f `=> x `=> y `=> f`(x, y)
@@ -69,7 +77,7 @@ f `=> x `=> y `=> f`(x, y)
 :e
 `let x = 42 `in x
 //│ ╔══[ERROR] Type error in unquoted term
-//│ ║  l.70: 	`let x = 42 `in x
+//│ ║  l.78: 	`let x = 42 `in x
 //│ ║        	         ^^
 //│ ╙── because: cannot constrain  Int  <:  CodeBase[out α122_2, out α123_2, ?]
 //│ Type: CodeBase[⊥, ⊥, ?]
@@ -77,7 +85,7 @@ f `=> x `=> y `=> f`(x, y)
 :e
 `let x = `0 `in 1
 //│ ╔══[ERROR] Type error in unquoted term
-//│ ║  l.78: 	`let x = `0 `in 1
+//│ ║  l.86: 	`let x = `0 `in 1
 //│ ║        	                ^
 //│ ╙── because: cannot constrain  Int  <:  CodeBase[out α131_3, out α132_3, ?]
 //│ Type: CodeBase[⊥, ⊥, ?]
@@ -103,7 +111,7 @@ run(1)
 :e
 x `=> run(x)
 //│ ╔══[ERROR] Type error in unquoted term
-//│ ║  l.104: 	x `=> run(x)
+//│ ║  l.112: 	x `=> run(x)
 //│ ║         	      ^^^^^^
 //│ ╙── because: cannot constrain  ⊤  <:  CodeBase[out α136_3, out α137_3, ?]
 //│ Type: CodeBase[out ⊤ -> ⊥, ⊥, ?]
@@ -111,7 +119,7 @@ x `=> run(x)
 :e
 `let x = `42 `in run(x)
 //│ ╔══[ERROR] Type error in unquoted term
-//│ ║  l.112: 	`let x = `42 `in run(x)
+//│ ║  l.120: 	`let x = `42 `in run(x)
 //│ ║         	                 ^^^^^^
 //│ ╙── because: cannot constrain  ⊤  <:  CodeBase[out α142_3, out α143_3, ?]
 //│ Type: CodeBase[⊥, ⊥, ?]
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls
index 14ff893ae8..88906f39a7 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls
@@ -4,7 +4,9 @@
 
 :fixme // parsing
 fun f x = f
-//│ ═══[ERROR] Function definition shape not yet supported for x
+//│ ╔══[ERROR] Function definition shape not yet supported for x
+//│ ║  l.6: 	fun f x = f
+//│ ╙──     	          ^
 //│ Type: ⊤
 
 fun f(x) = f
@@ -20,8 +22,8 @@ f
 :todo
 fun f(x) = f(x.a)
 //│ ╔══[ERROR] Term shape not yet supported by BbML: Sel(Ref(x@39),Ident(a))
-//│ ║  l.21: 	fun f(x) = f(x.a)
-//│ ╙──      	             ^
+//│ ║  l.23: 	fun f(x) = f(x.a)
+//│ ╙──      	             ^^^
 //│ Type: ⊤
 
 
@@ -31,7 +33,7 @@ class Foo[A](a: A)
 :todo proper error
 Foo(123)
 //│ ╔══[ERROR] Variable not found: Foo
-//│ ║  l.32: 	Foo(123)
+//│ ║  l.34: 	Foo(123)
 //│ ╙──      	^^^
 //│ Type: ⊥
 
@@ -42,7 +44,9 @@ new Foo(123)
 
 :todo proper error
 fun f(x) = f(Foo.a(x))
-//│ ═══[ERROR] Term shape not yet supported by BbML: Sel(Sel(Ref(globalThis:block#4),Ident(Foo)),Ident(a))
+//│ ╔══[ERROR] Term shape not yet supported by BbML: Sel(Sel(Ref(globalThis:block#4),Ident(Foo)),Ident(a))
+//│ ║  l.46: 	fun f(x) = f(Foo.a(x))
+//│ ╙──      	             ^^^^^
 //│ Type: ⊤
 
 fun f(x) = f(x.Foo#a)
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls
index 9a720ddac1..a065d4f15b 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls
@@ -174,5 +174,7 @@ bar
 
 :e
 region x in x.ref bar
-//│ ═══[ERROR] Expected a monomorphic type or an instantiable type here, but (forall α103_2: (α103_2) ->{⊥} α103_2) ->{⊥} Int found
+//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (forall α103_2: (α103_2) ->{⊥} α103_2) ->{⊥} Int found
+//│ ║  l.176: 	region x in x.ref bar
+//│ ╙──       	                  ^^^
 //│ Type: Ref[⊥, ?]
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbTODOs.mls b/hkmc2/shared/src/test/mlscript/bbml/bbTODOs.mls
index 8f0b8cf32b..7cf34ef825 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbTODOs.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbTODOs.mls
@@ -20,10 +20,10 @@ fun id[A](x: A) = x
 fun id: [A] -> A -> A => x = x
 //│ ╔══[ERROR] Name not found: x
 //│ ║  l.20: 	fun id: [A] -> A -> A => x = x
-//│ ╙──      	                             ^
+//│ ╙──      	                         ^
 //│ ╔══[ERROR] Name not found: x
 //│ ║  l.20: 	fun id: [A] -> A -> A => x = x
-//│ ╙──      	                         ^
-//│ /!!!\ Uncaught error: scala.MatchError: Lam(List(Param(‹›,A@37,None)),Error) (of class hkmc2.semantics.Term$Lam)
+//│ ╙──      	                             ^
+//│ /!!!\ Uncaught error: scala.MatchError: Lam(List(Param(‹›,A@36,None)),Error) (of class hkmc2.semantics.Term$Lam)
 
 
diff --git a/hkmc2/shared/src/test/mlscript/codegen/ClassMatching.mls b/hkmc2/shared/src/test/mlscript/codegen/ClassMatching.mls
index 4ef12e2bdd..0f30637f56 100644
--- a/hkmc2/shared/src/test/mlscript/codegen/ClassMatching.mls
+++ b/hkmc2/shared/src/test/mlscript/codegen/ClassMatching.mls
@@ -6,7 +6,7 @@
 
 class Some[out A](value: A)
 
-module None
+object None
 
 
 :sjs
diff --git a/hkmc2/shared/src/test/mlscript/codegen/ModuleMatching.mls b/hkmc2/shared/src/test/mlscript/codegen/ModuleMatching.mls
index 4a19508ed2..8178706682 100644
--- a/hkmc2/shared/src/test/mlscript/codegen/ModuleMatching.mls
+++ b/hkmc2/shared/src/test/mlscript/codegen/ModuleMatching.mls
@@ -1,7 +1,7 @@
 :js
 
 
-module Foo
+object Foo
 
 fun test(x) = x is Foo
 
@@ -10,7 +10,7 @@ test(Foo)
 
 
 fun foo() =
-  module Foo
+  object Foo
   Foo is Foo
 
 foo()
diff --git a/hkmc2/shared/src/test/mlscript/codegen/ModuleMethods.mls b/hkmc2/shared/src/test/mlscript/codegen/ModuleMethods.mls
index 37be9037cc..f20cbc62fd 100644
--- a/hkmc2/shared/src/test/mlscript/codegen/ModuleMethods.mls
+++ b/hkmc2/shared/src/test/mlscript/codegen/ModuleMethods.mls
@@ -3,7 +3,7 @@
 
 // TODO could use `globalThis.Example` instead of `this` in the generated code
 :sjs
-module Example with
+object Example with
   val a = 456
   fun f(x) = [x, a]
 //│ JS:
diff --git a/hkmc2/shared/src/test/mlscript/codegen/Modules.mls b/hkmc2/shared/src/test/mlscript/codegen/Modules.mls
index 0ece367e89..0576fbee3f 100644
--- a/hkmc2/shared/src/test/mlscript/codegen/Modules.mls
+++ b/hkmc2/shared/src/test/mlscript/codegen/Modules.mls
@@ -94,7 +94,7 @@ M.oops
 
 :sjs
 module M with
-  val m = M
+  val m: module M = M
 //│ JS:
 //│ const M$class = class M {
 //│   constructor() {
diff --git a/hkmc2/shared/src/test/mlscript/codegen/OptMatch.mls b/hkmc2/shared/src/test/mlscript/codegen/OptMatch.mls
index 94ab607595..8feea48b63 100644
--- a/hkmc2/shared/src/test/mlscript/codegen/OptMatch.mls
+++ b/hkmc2/shared/src/test/mlscript/codegen/OptMatch.mls
@@ -2,7 +2,7 @@
 
 
 class Some(value)
-module None
+object None
 
 
 :sjs
diff --git a/hkmc2/shared/src/test/mlscript/codegen/ThisCallVariations.mls b/hkmc2/shared/src/test/mlscript/codegen/ThisCallVariations.mls
index 52b0064294..a63a6552de 100644
--- a/hkmc2/shared/src/test/mlscript/codegen/ThisCallVariations.mls
+++ b/hkmc2/shared/src/test/mlscript/codegen/ThisCallVariations.mls
@@ -4,7 +4,7 @@
 //│ Imported 2 member(s)
 
 
-module Example with
+object Example with
   val a = 1
   fun f(x) = [x, a]
 
diff --git a/hkmc2/shared/src/test/mlscript/ucs/examples/BinarySearchTree.mls b/hkmc2/shared/src/test/mlscript/ucs/examples/BinarySearchTree.mls
index 07dfe3dd4c..0ab633eaea 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/examples/BinarySearchTree.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/examples/BinarySearchTree.mls
@@ -14,7 +14,7 @@ fun abs(x) = if x < 0 then -x else x
 
 abstract class Option[T]: (Some[T] | None)
 class Some[T](val value: T) extends Option[T]
-module None extends Option[nothing]
+object None extends Option[nothing]
 
 fun (??) getOrElse(o, v) = if o is
   Some(v') then v'
@@ -24,7 +24,7 @@ let anyToString = toString
 
 abstract class List[out T]: (Cons[T] | Nil)
 class Cons[out T](val head: T, val tail: List[T]) extends List[T]
-module Nil extends List[nothing]
+object Nil extends List[nothing]
 
 fun (::) cons(head, tail) = Cons(head, tail)
 
@@ -32,7 +32,7 @@ fun (::) cons(head, tail) = Cons(head, tail)
 
 abstract class Tree[out A]: (Empty | Node[A])
 class Node[out A](value: A, left: Tree[A], right: Tree[A]) extends Tree[A]
-module Empty extends Tree
+object Empty extends Tree
 
 fun single(v) = Node(v, Empty, Empty)
 
diff --git a/hkmc2/shared/src/test/mlscript/ucs/examples/LeftistTree.mls b/hkmc2/shared/src/test/mlscript/ucs/examples/LeftistTree.mls
index 80e23ee3ae..a9db2adc64 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/examples/LeftistTree.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/examples/LeftistTree.mls
@@ -12,7 +12,7 @@ fun abs(x) = if x < 0 then -x else x
 
 abstract class Option[out T]: (Some[T] | None)
 class Some[out T](val value: T) extends Option[T]
-module None extends Option[nothing]
+object None extends Option[nothing]
 
 fun (??) getOrElse(o, v) = if o is
   Some(v') then v'
@@ -20,13 +20,13 @@ fun (??) getOrElse(o, v) = if o is
 
 abstract class List[out T]: (Cons[T] | Nil)
 class Cons[out T](val head: T, val tail: List[T]) extends List[T]
-module Nil extends List[nothing]
+object Nil extends List[nothing]
 
 fun (::) cons(head, tail) = Cons(head, tail)
 
 abstract class Tree[out A]: (Empty | Node[A])
 class Node[out A](value: A, left: Tree[A], right: Tree[A], rank: Int) extends Tree[A]
-module Empty extends Tree[nothing]
+object Empty extends Tree[nothing]
 
 fun show(t: Tree[Any]): Str = if t is
   Node(v, l, r, _) then
diff --git a/hkmc2/shared/src/test/mlscript/ucs/examples/SimpleTree.mls b/hkmc2/shared/src/test/mlscript/ucs/examples/SimpleTree.mls
index df37bb9b5a..28a589e6b7 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/examples/SimpleTree.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/examples/SimpleTree.mls
@@ -2,10 +2,10 @@
 
 type Option[out A] = Some[A] | None
 class Some[out A](value: A)
-module None
+object None
 
 type Tree[out A] = Node[A] | Empty
-module Empty
+object Empty
 class Node[out A](value: A, left: Tree[A], right: Tree[A])
 
 fun find(t, v) = if t is
diff --git a/hkmc2/shared/src/test/mlscript/ucs/general/DualOptions.mls b/hkmc2/shared/src/test/mlscript/ucs/general/DualOptions.mls
index fbf7364982..11f96faac4 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/general/DualOptions.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/general/DualOptions.mls
@@ -7,7 +7,7 @@
 
 abstract class Option[T]
 class Some[T](value: T) extends Option[T]
-module None extends Option[nothing]
+object None extends Option[nothing]
 class Pair[A, B](x: A, y: B)
 
 // All `add_n` functions should be inferred to have the same type.
diff --git a/hkmc2/shared/src/test/mlscript/ucs/hygiene/HygienicBindings.mls b/hkmc2/shared/src/test/mlscript/ucs/hygiene/HygienicBindings.mls
index c8f35f5d97..00cbab3d0f 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/hygiene/HygienicBindings.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/hygiene/HygienicBindings.mls
@@ -5,7 +5,7 @@ fun error = ()
 fun (~~>) expect(a, b) = if a == b then () else error
 
 type Option[out T] = None | Some[T]
-module None
+object None
 class Some[out T](val value: T)
 
 type Either[A, B] = Left[A] | Right[B]
@@ -13,7 +13,7 @@ class Left[A](val leftValue: A)
 class Right[B](val rightValue: B)
 
 type List[out A] = Nil | Cons[A]
-module Nil
+object Nil
 class Cons[out A](head: A, tail: List[A])
 
 fun justTrue(_) = true
diff --git a/hkmc2/shared/src/test/mlscript/ucs/papers/OperatorSplit.mls b/hkmc2/shared/src/test/mlscript/ucs/papers/OperatorSplit.mls
index fd0b7c2776..6e8d0d82af 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/papers/OperatorSplit.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/papers/OperatorSplit.mls
@@ -185,6 +185,7 @@ fun example(args) =
 //│             continuation = Else of Lit of StrLit of "small"
 //│           tail = Else of Lit of StrLit of "medium"
 //│       resSym = ‹result of member:example›@35
+//│       flags = ()
 //│   res = Lit of UnitLit of true
 
 
diff --git a/hkmc2/shared/src/test/mlscript/ucs/syntax/NestedOpSplits.mls b/hkmc2/shared/src/test/mlscript/ucs/syntax/NestedOpSplits.mls
index 6a39d86fac..018ad064c2 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/syntax/NestedOpSplits.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/syntax/NestedOpSplits.mls
@@ -58,6 +58,7 @@ fun f(x) =
 //│             continuation = Else of Lit of IntLit of 0
 //│           tail = Else of Lit of IntLit of 1
 //│       resSym = ‹result of member:f›@16
+//│       flags = ()
 //│   res = Lit of UnitLit of true
 
 
diff --git a/hkmc2/shared/src/test/mlscript/ucs/syntax/SimpleUCS.mls b/hkmc2/shared/src/test/mlscript/ucs/syntax/SimpleUCS.mls
index 9e69771efb..2ebe9d6d8f 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/syntax/SimpleUCS.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/syntax/SimpleUCS.mls
@@ -2,7 +2,7 @@
 
 abstract class Option[A]: Some[A] | None
 class Some[A](value: A) extends Option[A]
-module None extends Option
+object None extends Option
 
 abstract class Either[out A, out B]: Left[A] | Right[B]
 class Left[A](leftValue: A) extends Either[A, nothing]