diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala
index d809625227..5af62281bb 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala
@@ -265,6 +265,12 @@ class InstSymbol(val origin: Symbol)(using State) extends LocalSymbol:
   override def toLoc: Option[Loc] = origin.toLoc
   def subst(using sub: SymbolSubst): InstSymbol = sub.mapInstSym(this)
 
+class InfVarSymbol(val origin: Symbol | Term, val hint: Str = "")(using State) extends LocalSymbol:
+  override def nme: Str = origin match
+    case x: Symbol => x.nme ++ hint
+    case x: Term => hint
+  override def toLoc: Option[Loc] = origin.toLoc
+  def subst(using sub: SymbolSubst): InfVarSymbol = ???
 
 class VarSymbol(val id: Ident)(using State)
     extends LocalVarSymbol(id.name)
diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala
new file mode 100644
index 0000000000..a6b1578a0b
--- /dev/null
+++ b/hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala
@@ -0,0 +1,151 @@
+package hkmc2
+package typing
+package logicsub
+
+import scala.collection.mutable
+import syntax.*
+import semantics.*
+import Message.MessageContext
+import hkmc2.utils.*, shorthands.*
+import utils.*
+import utils.Scope
+
+type Cache = mutable.HashSet[(Type, Type)]
+type ExtrudeCache = mutable.HashMap[(InfVarSymbol, Bool), InfVar]
+
+case class CCtx(cache: Cache, parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType])(using Scope):
+  def err(using ctx: KCtx)(using TL, Raise) = 
+    given CCtx = this
+    ctx.err(parents, origin, exp)
+  def nest(sub: (Type, Type)): CCtx =
+    copy(cache = cache += sub, parents = parents match
+      case `sub` :: _ => parents
+      case _ =>  sub :: parents
+    )
+object CCtx:
+  inline def init(origin: Term, exp: Opt[InfType])(using Scope) =
+    CCtx(mutable.HashSet.empty, Nil, origin, exp)
+
+object ConstraintSolver:
+  private def log(msg: => Any, noIndent: Bool = false)(using tl: TL) = tl.log(msg, noIndent)
+
+  private def constrainConj(conj: Conj)(using ctx: KCtx, cctx:CCtx)(using TL, Raise): Unit =
+  tl.trace(s"Constraining ${conj.showDbg}"):
+    conj match
+      case Conj(i, u, S(v), S(w), xs, ys) if w.lvl > v.lvl =>
+        val rest = Conj(i, u, S(v), N, xs, ys)
+        val nc = rest.toDnf // always cache the normal form to avoid unexpected cache misses
+        log(s"New bound: ${v.showDbg} >: ${nc.showDbg}")
+        cctx.nest(nc -> w.toDnf) givenIn:
+          ctx.addlb(nc, w)
+      case Conj(i, u, S(v), w, xs, ys) =>
+        val rest = Conj(i, u, N, w, xs, ys)
+        val nc = (~rest).toDnf // always cache the normal form to avoid unexpected cache misses
+        log(s"New bound: ${v.showDbg} <: ${nc.showDbg}")
+        cctx.nest(v.toDnf -> nc) givenIn:
+          ctx.addub(v, nc)
+      case Conj(i, u, N, S(v), xs,ys) =>
+        val rest = Conj(i, u, N,N,xs,ys)
+        val c = rest.toDnf // always cache the normal form to avoid unexpected cache misses
+        log(s"New bound: ${v.showDbg} :> ${c.showDbg}")
+        cctx.nest(c -> v.toDnf) givenIn:
+          ctx.addlb(c, v)
+      case Conj(NF.Inter(x :: Nil), NF.Union(Nil), N,N,_,_) =>
+        val da = x.args.iterator.zip(x.congr).collect:
+          case (t, true) => t.posPart
+        val d = (x.refinement.values ++ da).toList
+        if d.isEmpty then cctx.err
+        else ctx.constrain(d.tail.foldLeft(ctx.sub(d.head, Bot))((k, t) => ctx.or(k, ctx.sub(t, Bot))))
+      case Conj(NF.Inter(x :: Nil), NF.Union(y :: Nil), N,N,_,_) =>
+        val da = x.args.iterator.zip(x.congr).collect:
+          case (t, true) => t.posPart
+        val d = (x.refinement.values ++ da).toList
+        val xrm = x.refinement.toMap
+        val yrm = y.refinement.toMap
+        val sp = ctx.asSubcls(x,y.sym)
+        if sp.isEmpty || !yrm.keySet.subsetOf(xrm.keySet) then
+          if d.isEmpty then cctx.err
+          else ctx.constrain(d.map(ctx.sub(_, Bot)).reduce(ctx.or))
+        else
+          val x = sp.get
+          val u = x.args.zip(y.args).flatMap(ctx.subArg)
+          val w = y.refinement.map:
+            case (a,b) => ctx.sub(xrm(a), b)
+          val ds = x.refinement.filterNot(f => yrm.contains(f._1)).map:
+            case (_,t) => ctx.sub(t,Bot)
+          (u++w).foreach: k =>
+            ctx.constrain((ds ++ Ls(k)).reduce(ctx.or))
+      case Conj(NF.Inter(xs @ (x :: _)), NF.Union(y :: Nil), N,N,_,_) =>
+        if x.sym === y.sym then
+          val k = x.ov.get
+          val u = xs.map(_.args(k).negPart.discriminator)
+          val w = u.reduce[Type](_|_)
+          val in = y.args(k)
+          ctx.constrain(ctx.sub(in.negPart, w))
+          u.lazyZip(xs).foreach: (p, c) =>
+            val d = ctx.sub(in.negPart, ~p)
+            val r = y.copy(args = y.args.updated(k, Wildcard(p & in.negPart, in.posPart)))
+            val s = ctx.sub(c, r)
+            ctx.constrain(ctx.or(d, s))
+        else cctx.err
+      case Conj(k @ NF.Inter(x :: _), NF.Union(ys @ (_ :: _)), N,N,ws,zs) =>
+        def h(y: ClassLikeType) =
+          def f(u: Ls[TypeArg], w: Ls[TypeArg], s: Ls[TypeArg], p:Ls[Bool])
+              : Ls[ClassLikeType] = (w,p) match
+            case (Nil, _) => Nil
+            case (t::ws, true::ps) =>
+              val a = u ++ (Wildcard.out(~t.posPart)::s)
+              y.copy(args = a) :: f(s.head::u, ws, s.tail, ps)
+            case (t::ws, false::ps) => f(s.head::u, ws, s.tail, ps)
+            case _ => ???
+          def g(u: Ls[(Tree.Ident, Type)]) =
+            val w = y.args.map(_ => Wildcard.empty)
+            y.refinement.map((a,t) => y.copy(args = w, refinement = (a,~t)::Nil))
+          f(Nil, y.args, y.args.map(_ => Wildcard.empty), y.congr) ++ g(y.refinement)
+        val (ps,t) = ys.partition(_.partialpattern)
+        val xrs = x.refinement.keys.toSet
+        val qs = ps.filter: p =>
+          ctx.asSubcls(x,p.sym).isDefined && p.refinement.keys.forall(xrs.contains)
+        val ks = qs.foldLeft(Ls(k)): (ks, y) =>
+          ks.flatMap(k => h(y).map(c => k.merge(NF.Inter(Ls(c))).get))
+        ks.foreach(k => constrainConj(Conj(k, NF.Union(t),N,N,ws,zs)))
+      case _ =>
+        raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} <: ⊥" -> N :: Nil))
+        cctx.err
+
+  // private class SkolemBoundsInliner(using ctx: KCtx) extends TypeMap:
+  //   val cache: mutable.HashSet[InfVarSymbol] = mutable.HashSet.empty
+  //   override def apply(pol: Bool)(t: Type) = t.toBasic match
+  //     case v @ InfVar(_, s, true) if !cache(s) =>
+  //       cache += s
+  //       apply(pol)(if pol
+  //         then ctx.ubs(s).foldLeft[Type](v)(_ & _)
+  //         else ctx.lbs(s).foldLeft[Type](v)(_ | _))
+  //     case _: ClassLikeType | _: InfVar => t
+  //     case t => super.apply(pol)(t)
+  private def inlineSkolemBounds(ty: Type)(using KCtx): Type = ty // TODO
+  //   (new SkolemBoundsInliner)(true)(ty)
+
+  def constrainImpl(lhs: Type, rhs: Type)
+      (using ctx: KCtx, cctx:CCtx)(using TL, Raise)
+      : Unit =
+    val p = lhs.toDnf -> rhs.toDnf
+    if cctx.cache(p) then log(s"Cached!")
+    else tl.trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"):
+      cctx.nest(p) givenIn:
+        val disj = inlineSkolemBounds(lhs & ~rhs).toDnf
+        disj.cs.foreach(constrainConj(_))
+
+  def constrain(lhs: Type, rhs: Type)(using ctx: KCtx, cctx:CCtx)(using TL, Raise): Unit =
+    val (ps, ts) = rhs.disjuncts.toList.partition(_.partialpattern)
+    if ts.length > 1 then
+      val p = lhs.toDnf -> rhs
+      if cctx.cache(p) then log(s"Cached!")
+      else tl.trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"):
+        cctx.nest(p) givenIn:
+          val u = ps.foldLeft(lhs)((x, y) => x & ~y)
+          val qs = ts.map(_.discriminator)
+          constrainImpl(u, qs.reduce(_ | _))
+          qs.zip(ts).foreach((q, y) => constrainImpl(q & u, y))
+    else
+      constrainImpl(lhs, rhs)
diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala
new file mode 100644
index 0000000000..0cdcb58683
--- /dev/null
+++ b/hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala
@@ -0,0 +1,100 @@
+package hkmc2
+package typing
+package logicsub
+
+import scala.annotation.tailrec
+
+import syntax.*
+import semantics.*
+import Message.MessageContext
+import hkmc2.utils.*, shorthands.*
+import utils.*
+import utils.Scope
+
+sealed abstract class NormalForm extends TypeExt
+
+object NF:
+  final case class Inter(v: Ls[ClassLikeType]) extends NormalForm:
+    lazy val toBasic = v.foldLeft[Type](Top)(_ & _).toBasic
+    def merge(other: Inter): Opt[Inter] =
+      other.v.foldLeft(Opt(v))((r, w) => r.flatMap(w.merge(_))).map(Inter(_))
+
+  final case class Union(v: Ls[ClassLikeType]) extends NormalForm:
+    lazy val toBasic = v.foldLeft[Type](Bot)(_ | _).toBasic
+    def merge(other: Union) = Union(v ++ other.v)
+
+  object Inter:
+    val empty = Inter(Nil)
+  object Union:
+    val empty = Union(Nil)
+
+final case class Disj(cs: Ls[Conj]) extends NormalForm:
+  lazy val toBasic = cs.foldLeft[Type](Bot)(_ | _).toBasic
+  def isBot = cs.isEmpty
+
+final case class Conj(
+  i: NF.Inter, u: NF.Union,
+  v1: Opt[InfVar], v2: Opt[InfVar],
+  ps: Ls[InfVar], ns: Ls[InfVar]
+) extends NormalForm:
+  lazy val toBasic = (i.toBasic & ~u.toBasic & v1.getOrElse(Top) & v2.fold(Top)(~_)).toBasic
+  def merge(that: Conj)(using TL): Opt[Conj] =
+  tl.traceNot[Opt[Conj]](s"merge ${this.showDbg} and ${that.showDbg}", r => s"= ${r.map(_.showDbg)}"):
+    val Conj(i1, u1, v1, w1, x1, y1) = this
+    val Conj(i2, u2, v2, w2, x2, y2) = that
+    val xs = (x1 ++ x2).distinct
+    val ys = (y1 ++ y2).distinct
+    if xs.intersect(ys).nonEmpty then N
+    else i1.merge(i2).flatMap: i =>
+      val u = u1.merge(u2)
+      (v1.orElse(v2), w1.orElse(w2)) match
+        case (S(v), S(w)) if v.sym === w.sym => N
+        case (v,w) => S(Conj(i, u, v, w, xs, ys))
+
+object Conj:
+  val empty: Conj = Conj(NF.Inter.empty, NF.Union.empty, N, N, Nil, Nil)
+  def mkVar(v: InfVar, pol: Bool) =
+    if pol then
+      Conj(NF.Inter.empty, NF.Union.empty, S(v), N, Nil, Nil)
+    else Conj(NF.Inter.empty, NF.Union.empty, N, S(v), Nil, Nil)
+  def mkInter(inter: ClassLikeType) =
+    Conj(NF.Inter(Ls(inter)), NF.Union.empty, N, N, Nil, Nil)
+  def mkUnion(union: ClassLikeType) =
+    Conj(NF.Inter.empty, NF.Union(Ls(union)), N, N, Nil, Nil)
+object Disj:
+  val bot = Disj(Nil)
+  val top = Disj(Ls(Conj.empty))
+ 
+object NormalForm:
+  def inter(lhs: Disj, rhs: Disj)(using TL): Disj =
+  tl.traceNot[Disj](s"inter ${lhs.showDbg} and ${rhs.showDbg}", r => s"= ${r.showDbg}"):
+    if lhs.isBot || rhs.isBot then Disj.bot
+    else Disj(lhs.cs.flatMap(lhs => rhs.cs.flatMap(rhs => lhs.merge(rhs) match {
+      case S(conj) => conj :: Nil
+      case N => Nil
+    })))
+
+  def union(lhs: Disj, rhs: Disj): Disj = Disj(lhs.cs ++ rhs.cs)
+
+  def neg(ty: Type)(using TL): Disj =
+  tl.traceNot[Disj](s"~Disj ${ty.showDbg} ${ty.getClass} ${ty.toBasic.showDbg}", r => s"= ${r.showDbg}"):
+    ty match
+    case u: NF.Union => Disj(Ls(Conj(NF.Inter(Nil), u, N, N, Nil, Nil)))
+    case v: InfVar => Disj(Ls(Conj.mkVar(v, false)))
+    case ct: ClassLikeType => Disj(Ls(Conj.mkUnion(ct)))
+    case _ => (~ty.toBasic).toDnf
+
+  def dnf(ty: Type)(using TL): Disj =
+  tl.traceNot[Disj](s"Disj ${ty.showDbg} ${ty.getClass}", r => s"= ${r.showDbg}"):
+    ty match
+    case d: Disj => d
+    case c: Conj => Disj(Ls(c))
+    case i: NF.Inter => Disj(Ls(Conj(i, NF.Union.empty, N, N, Nil, Nil)))
+    case _ => ty.toBasic match
+    case Top => Disj.top
+    case Bot => Disj.bot
+    case v: InfVar => Disj(Ls(Conj.mkVar(v, true)))
+    case ct: ClassLikeType => Disj(Conj.mkInter(ct) :: Nil)
+    case Inter(lhs, rhs) => inter(lhs.toDnf, rhs.toDnf)
+    case Union(lhs, rhs) => union(lhs.toDnf, rhs.toDnf)
+    case Neg(ty) => neg(ty)
diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala
new file mode 100644
index 0000000000..8c566e53e8
--- /dev/null
+++ b/hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala
@@ -0,0 +1,36 @@
+package hkmc2
+package typing
+package logicsub
+
+import hkmc2.utils.*, shorthands.*
+
+// class TypeTraverser:
+//   def apply(pol: Bool)(ty: Type): Unit = ty.toBasic match
+//     case Union(x, y) => 
+//       apply(pol)(x)
+//       apply(pol)(y)
+//     case Inter(x, y) =>
+//       apply(pol)(x)
+//       apply(pol)(y)
+//     case Neg(ty) => apply(!pol)(ty)
+//     case ClassLikeType(name, targs, refine) =>
+//       targs.foreach:
+//         case Wildcard(in, out) =>
+//           apply(!pol)(in)
+//           apply(pol)(out)
+//         case ty: Type =>
+//           apply(pol)(ty)
+//           apply(!pol)(ty)
+//       refine.values.foreach(apply(pol))
+//     case _ =>
+
+class TypeMap:
+  def applyArg(pol: Bool)(t: TypeArg): TypeArg =
+    Wildcard(apply(!pol)(t.negPart), apply(pol)(t.posPart))
+  def apply(pol: Bool)(t: Type): Type = t.toBasic match
+    case Bot | Top | _: InfVar => t
+    case Union(x, y) => Union(apply(pol)(x), apply(pol)(y))
+    case Inter(x, y) => Inter(apply(pol)(x), apply(pol)(y))
+    case Neg(x) => Neg(apply(!pol)(x))
+    case ClassLikeType(n, args, refine, i,o) =>
+      ClassLikeType(n, args.map(applyArg(pol)), refine.mapValues(t => apply(pol)(t)), i,o)
diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala
new file mode 100644
index 0000000000..512e579149
--- /dev/null
+++ b/hkmc2/shared/src/main/scala/hkmc2/typing/infctx.scala
@@ -0,0 +1,156 @@
+package hkmc2
+package typing
+package logicsub
+
+import scala.collection.mutable.{HashSet, HashMap, ListBuffer}
+import scala.annotation.tailrec
+
+import hkmc2.utils.*, shorthands.*
+import utils.*
+
+import Message.MessageContext
+import semantics.*, Term.*, ucs.FlatPattern
+import Elaborator.Ctx
+import syntax.*
+import Tree.*
+import utils.Scope
+
+final case class K(x: Type, y: Type, cs: Opt[Ls[K]]):
+  def lvl: Int = x.lvl max y.lvl max cs.fold(0)(_.map(_.lvl).max)
+
+class InfVarState:
+  var lowerBounds: Ls[Type] = Nil
+  var upperBounds: Ls[Type -> Opt[Ls[K]]] = Nil
+
+trait KCtx(using val prim: PrimCtx):
+  def sub(x: Type, y: Type): K = K(x,y,N)
+  def subArg(x: TypeArg, y: TypeArg): Ls[K] =
+    sub(x.posPart,y.posPart) :: sub(y.negPart,x.negPart) :: Nil
+  def or(x: K, y: K): K = (x,y) match
+    case (K(a, b, N), y) => K(a, b, S(Ls(y)))
+    case (K(a, b, S(cs)), y) => K(a, b, S(cs.map(or(_,y))))
+  def constrain(c: K)(using CCtx, TL, Raise): Unit = c match
+    case K(x,y,N) => ConstraintSolver.constrain(x,y)(using this)
+    case K(x,y,S(Nil)) =>
+    case K(x,y,S(cs)) => ConstraintSolver.constrain(x,y)(using SuffixCtx(cs, this))
+  def asSubcls(x: ClassLikeType, y: ClsTag) =
+    if x.sym === y then S(x)
+    else x.sym match
+      case LitSymbol(_: IntLit) if prim.intSym === y => S(ClassLikeType(y, Nil, Nil, Nil, N))
+      case LitSymbol(_: StrLit) if prim.strSym === y => S(ClassLikeType(y, Nil, Nil, Nil, N))
+      case LitSymbol(_: BoolLit) if prim.boolSym === y => S(ClassLikeType(y, Nil, Nil, Nil, N))
+      case _ => N
+
+  def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise): Unit
+  def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise): Unit
+  def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType])
+    (using CCtx, TL, Raise, Scope): Unit
+
+final case class InfCtx(
+  lvl: Int,
+  parent: Option[InfCtx],
+  env: HashMap[Symbol, InfType],
+  outRegAcc: Type,
+  prefix: Opt[Ls[K]] = N
+)(using
+    val varSt: HashMap[InfVarSymbol, InfVarState],
+    val xbds: ListBuffer[K],
+    prim: PrimCtx,
+    val ctx: Ctx,
+    val cfg: Config
+) extends KCtx:
+  def +=(p: Symbol -> InfType) = env += p
+  def get(sym: Symbol): Option[InfType] = env.get(sym) `orElse` parent.dlof(_.get(sym))(None)
+  def nest: InfCtx = copy(parent = Some(this), env = HashMap.empty)
+  def nestWithOuter(outer: InfVar): InfCtx = copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty, outRegAcc = outRegAcc | outer)
+  def nextLevel: InfCtx= copy(parent = Some(this), lvl = lvl + 1, env = HashMap.empty)
+
+  def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise) =
+    val k = K(s, ub, cs)
+    if s.lvl < k.lvl then xbds += k
+    else
+      val v = varSt.getOrElseUpdate(s.sym, new InfVarState)
+      v.upperBounds = ub -> cs :: v.upperBounds
+      v.lowerBounds.foreach(lb => constrain(sub(lb, ub)))
+  def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise) =
+   val k = K(lb, s, N)
+   if s.lvl < k.lvl then xbds += k
+   else
+     val v = varSt.getOrElseUpdate(s.sym, new InfVarState)
+     v.lowerBounds = lb :: v.lowerBounds
+     v.upperBounds.foreach(p => constrain(K(lb, p._1, p._2)))
+  def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType])
+     (using CCtx, TL, Raise, Scope) = 
+   given InfCtx = this
+   raise(ErrorReport(
+       msg"Type error in ${origin.describe}${exp match
+           case S(ty) => msg" with expected type ${ty.show}"
+           case N => msg""
+         }" -> origin.toLoc
+       :: parents.reverse.map(p =>
+         msg"because: cannot constrain  ${p._1.show}  <:  ${p._2.show}" -> N
+       )
+     ))
+  // TODO
+  def ubs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).upperBounds.map(_._1)
+  def lbs(s: InfVarSymbol): Ls[Type] = varSt.getOrElseUpdate(s, new InfVarState).lowerBounds
+  // def withPrefix(x: Type, y: Type) = ???
+  override def constrain(c: K)(using CCtx, TL, Raise) = prefix match
+    case N => super.constrain(c)
+    case S(Nil) =>
+    case S(cs) => cs.foreach(k => super.constrain(or(k,c)))
+
+class PrimCtx(using st: Elaborator.State, ctx: Elaborator.Ctx, cfg: Config):
+  val objSym = ctx.get("Object").get.symbol.get.asTpe.get
+  val intSym = ctx.get("Int").get.symbol.get.asTpe.get
+  val strSym = ctx.get("Str").get.symbol.get.asTpe.get
+  val boolSym = ctx.get("Bool").get.symbol.get.asTpe.get
+  val errSym = ctx.get("Error").get.symbol.get.asTpe.get
+  val fnSym = ctx.get("Function").get.symbol.get.asTpe.get
+  val arrSym = ctx.get("Array").get.symbol.get.asTpe.get
+  def litSym(x: syntax.Literal) = LitSymbol(x)
+
+object InfCtx:
+  def init(using st: Elaborator.State, ctx: Elaborator.Ctx, tl: TL, cfg: Config): InfCtx =
+    given PrimCtx = new PrimCtx
+    InfCtx(1, N, HashMap.empty, Bot)(using HashMap.empty, ListBuffer.empty)
+  def mkTag(s: ClsTag) = ClassLikeType(s, Nil, Nil, Nil, N)
+  def litTy(lit: Literal)(using ctx: InfCtx) = mkTag(ctx.prim.litSym(lit))
+  def objTy(using ctx: InfCtx) = mkTag(ctx.prim.objSym)
+  def funTy(args: Ls[Type], ret: Type, eff: Type)(using ctx: InfCtx) =
+    val u = tupTy(args)
+    val w = Ls(Wildcard.in(u), Wildcard.out(ret), Wildcard.out(eff))
+    val i = Ls(true, false, false)
+    ClassLikeType(ctx.prim.fnSym, w, Nil, i, S(0))
+  // def arrayTy(elem: Type)(using ctx: InfCtx) = ClassLikeType(ctx.prim.arrSym, Ls(elem), Nil, Nil)
+  def tupTy(e: Ls[Type])(using ctx: InfCtx) =
+    // val refine = (Tree.Ident("size"): Tree.Ident, litTy(IntLit(e.length))) :: e.zipWithIndex.map:
+    //   case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy)
+    // ClassLikeType(ctx.prim.arrSym, Ls(e.foldLeft[Type](Bot)(_ | _)), refine, Ls(true), N)
+    val refine = e.zipWithIndex.map:
+      case (elemTy, idx) => (Tree.Ident(idx.toString): Tree.Ident, elemTy)
+    ClassLikeType(ctx.prim.arrSym, Nil, refine, Nil, N)
+  def refinedObj(r: Ls[Tree.Ident -> Type])(using ctx: InfCtx) =
+    ClassLikeType(ctx.prim.objSym, Nil, r, Nil, N)
+
+class SuffixCtx(val suffix: Ls[K], val cont: KCtx)(using PrimCtx) extends KCtx:
+  def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise) = cs match
+    case N => cont.addub(s, ub, S(suffix))
+    case S(Nil) =>
+    case S(cs) => cont.addub(s, ub, S(cs.flatMap(k => suffix.map(or(k,_)))))
+  def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise) = ???
+  def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType])
+      (using CCtx, TL, Raise, Scope) =
+    suffix.foreach(cont.constrain)
+
+class MkPrefix(using PrimCtx) extends KCtx:
+  var r = Opt(ListBuffer.empty[K])
+  def addub(s: InfVar, ub: Type, cs: Opt[Ls[K]] = N)(using CCtx, TL, Raise) =
+    r.foreach(_ += K(s, ub, cs))
+  def addlb(lb: Type, s: InfVar)(using CCtx, TL, Raise) = ???
+  def err(parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType])
+      (using CCtx, TL, Raise, Scope) =
+    r = N
+  def apply(x: Type, y: Type)(using CCtx, TL, Raise): Opt[Ls[K]] =
+    constrain(sub(x,y))
+    r.map(_.toList)
diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala
new file mode 100644
index 0000000000..782c433612
--- /dev/null
+++ b/hkmc2/shared/src/main/scala/hkmc2/typing/inftype.scala
@@ -0,0 +1,223 @@
+package hkmc2
+package typing
+package logicsub
+
+import hkmc2.utils.*, shorthands.*
+import syntax.*
+import semantics.*, semantics.Term.*
+import utils.*
+import scala.collection.mutable.{Set => MutSet}
+import utils.Scope, Scope.scope
+import Elaborator.State
+
+
+sealed abstract class InfType:
+  def lvl: Int
+  def show(using Scope, InfCtx, Raise): Str
+  def showDbg: Str
+
+sealed trait TypeArg:
+  def lvl: Int
+  def show(using Scope, InfCtx, Raise): Str
+  def showDbg: Str
+  def & (that: TypeArg): TypeArg = (this, that) match
+    case (Wildcard(in1, out1), Wildcard(in2, out2)) => Wildcard(in1 | in2, out1 & out2)
+    case (ty: Type, Wildcard(in2, out2)) => Wildcard(ty | in2, ty & out2)
+    case (Wildcard(in1, out1), ty: Type) => Wildcard(in1 | ty, out1 & ty)
+    case (ty1: Type, ty2: Type) => ty1 & ty2
+  def | (that: TypeArg): TypeArg = (this, that) match
+    case (Wildcard(in1, out1), Wildcard(in2, out2)) => Wildcard(in1 & in2, out1 | out2)
+    case (ty: Type, Wildcard(in2, out2)) => Wildcard(ty & in2, ty | out2)
+    case (Wildcard(in1, out1), ty: Type) => Wildcard(in1 & ty, out1 | ty)
+    case (ty1: Type, ty2: Type) => ty1 | ty2
+  def posPart: Type = this match
+    case Wildcard(_, out) => out
+    case ty: Type => ty
+  def negPart: Type = this match
+    case Wildcard(in, _) => in
+    case ty: Type => ty
+
+case class Wildcard(in: Type, out: Type) extends TypeArg:
+  lazy val lvl = in.lvl.max(out.lvl)
+  def show(using Scope, InfCtx, Raise): Str = in match
+    case `out` => in.show
+    case Bot =>
+      out match
+        case Top => "?"
+        case _ => s"out ${out.show}"
+    case _ =>
+      out match
+        case Top => s"in ${in.show}"
+        case _ => s"in ${in.show} out ${out.show}"
+  def showDbg: Str = s"in ${in.showDbg} out ${out.showDbg}"
+
+object Wildcard:
+  def in(ty: Type) = Wildcard(ty, Top)
+  def out(ty: Type) = Wildcard(Bot, ty)
+  def empty = Wildcard(Bot, Top)
+
+case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], xbds: Ls[K], body: InfType) extends InfType:
+  lazy val lvl = (body :: tvs).map(_.lvl).max
+  def show(using Scope, InfCtx, Raise) = showDbg //TODO
+  def showDbg = ???
+
+case class PolyFunType(args: Ls[InfType], ret: InfType, eff: Type) extends InfType:
+  lazy val lvl = (ret :: eff :: args).iterator.map(_.lvl).max
+  def show(using Scope, InfCtx, Raise) =
+    s"(${args.map(_.show).mkString(", ")}) ->{${eff.show}} ${ret.show}"
+  def showDbg = s"(${args.map(_.showDbg).mkString(", ")}) ->{${eff.showDbg}} ${ret.showDbg}"
+
+sealed abstract class Type extends InfType with TypeArg:
+  lazy val lvl = toBasic match
+    case ClassLikeType(name, targs, refinement, _,_) =>
+      val args = targs.iterator
+      val refine = refinement.iterator.map(_._2)
+      (args ++ refine).map(_.lvl).maxOption.getOrElse(0)
+    case InfVar(lvl, _, _) => lvl
+    case Top | Bot => 0
+    case Union(lhs, rhs) => lhs.lvl.max(rhs.lvl)
+    case Inter(lhs, rhs) => lhs.lvl.max(rhs.lvl)
+    case Neg(ty) => ty.lvl
+  def show(using Scope, InfCtx, Raise) = toBasic match
+    case ClassLikeType(f, args, _,_,_) if f === summon[InfCtx].prim.fnSym =>
+      val fargs :: ret :: eff :: Nil = args.runtimeChecked
+      val ClassLikeType(_,_,r,_,_) = fargs.negPart.runtimeChecked
+      val a = s"[${r.values.map(_.show).mkString(", ")}]"
+      if eff === Bot then
+        s"$a -> ${ret.show}"
+      else
+        s"$a ->{${eff.show}} ${ret.show}"
+    case ClassLikeType(name, targs, refinement, _,_) =>
+      val cls = if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.show).mkString(", ")}]"
+      val r = refinement.map { case (l,t) => s"${l.name}: ${t.showDbg}" }.mkString(", ")
+      cls ++ (if refinement.isEmpty then "" else s" & {$r}")
+    case v @ InfVar(lvl, sym, isSkolem) =>
+      val name = scope.lookup(v.sym).getOrElse(scope.allocateName(v.sym, v.sym.hint))
+      if isSkolem then name else s"'${name}"
+    case Union(lhs, rhs) => s"${lhs.paren} ∨ ${rhs.paren}"
+    case Inter(lhs, rhs) => s"${lhs.paren} ∧ ${rhs.paren}"
+    case Neg(ty) => s"¬${ty.paren}"
+    case _ => showDbg
+  def showDbg: Str = toBasic match
+    case ClassLikeType(name, targs, refinement, _,_) =>
+      val cls = if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.showDbg).mkString(", ")}]"
+      val r = refinement.map { case (l,t) => s"${l.name}: ${t.showDbg}" }.mkString(", ")
+      cls ++ (if refinement.isEmpty then "" else s" & {$r}")
+    case v @ InfVar(lvl, sym, isSkolem) =>
+      val name = if sym.hint.isEmpty then s"${sym.nme}" else s"${sym.nme}(${sym.hint})"
+      if isSkolem then s"${name}${sym.uid}_${lvl}" else s"'${name}${sym.uid}_${lvl}"
+    case Union(lhs, rhs) => s"${lhs.parenDbg} ∨ ${rhs.parenDbg}"
+    case Inter(lhs, rhs) => s"${lhs.parenDbg} ∧ ${rhs.parenDbg}"
+    case Neg(ty) => s"¬${ty.parenDbg}"
+    case Top => "⊤"
+    case Bot => "⊥"
+
+  protected[logicsub] def paren(using Scope, InfCtx, Raise): Str = toBasic match
+    case _: InfVar | _: ClassLikeType | _: Neg | Top | Bot => show
+    case _ => s"($show)"
+
+  protected[logicsub] def parenDbg: Str = toBasic match
+    case _: InfVar | _: ClassLikeType | _: Neg | Top | Bot => showDbg
+    case _ => s"($showDbg)"
+
+  lazy val toBasic: BasicType
+  lazy val discriminator = Discriminator(true)(this).simp
+  lazy val partialpattern: Bool = simp match
+    case _: InfVar => false
+    case Top | Bot => true
+    case ClassLikeType(s, args, refine,congr,_) =>
+      val p = args.iterator.zip(congr).forall:
+        case (t, true) => t.negPart === Bot && t.posPart.partialpattern
+        case (t, false) => t is Wildcard.empty
+      p && refine.values.forall(_.partialpattern)
+    case Union(x,y) => x.partialpattern && y.partialpattern
+    case Inter(x,y) => x.partialpattern && y.partialpattern
+    case Neg(x) => x.partialpattern
+
+  lazy val simp: BasicType = (toBasic match
+    case Union(x,y) => x.simp | y.simp
+    case Inter(x,y) => x.simp & y.simp
+    case Neg(Union(x,y)) => Neg(x).simp & Neg(y).simp
+    case Neg(Inter(x,y)) => Neg(x).simp | Neg(y).simp
+    case Neg(Neg(x)) => x.simp
+    case Neg(x) => ~x
+    case x => x).toBasic
+
+  def disjuncts: Ite[Type] = simp match
+    case Union(x,y) => x.disjuncts ++ y.disjuncts
+    case x => Ite(x)
+  def conjuncts: Ite[Type] = simp match
+    case Inter(x,y) => x.conjuncts ++ y.conjuncts
+    case x => Ite(x)
+
+  var _dnf: Disj = null
+  def toDnf(using TL) = 
+    if _dnf eq null then _dnf = NormalForm.dnf(this)
+    _dnf
+
+  def |(that: Type): Type = this match
+    case Top => Top
+    case Bot => that
+    case _ => that match
+      case Top => Top
+      case Bot => this
+      case Union(l, r) => this | l | r
+      case _ => if this === that then this else Union(this, that)
+  def &(that: Type): Type = this match
+    case Top => that
+    case Bot => Bot
+    case _ => that match
+      case Top => this
+      case Bot => Bot
+      case Inter(l, h) => this & l & h
+      case _ => if this === that then this else Inter(this, that)
+  def unary_~ : Type = toBasic match
+    case Top => Bot
+    case Bot => Top
+    case Inter(x,y) => ~x | ~y
+    case Union(x,y) => ~x & ~y
+    case Neg(x) => x
+    case _ => Neg(this)
+
+abstract class TypeExt extends Type
+
+sealed abstract class BasicType extends Type:
+  lazy val toBasic = this
+final case class InfVar(vlvl: Int, sym: InfVarSymbol, isSkolem: Bool) extends BasicType
+object Bot extends BasicType
+object Top extends BasicType
+case class Union(lhs: Type, rhs: Type) extends BasicType
+case class Inter(lhs: Type, rhs: Type) extends BasicType
+case class Neg(t: Type) extends BasicType
+case class ClassLikeType(
+  sym: ClsTag, args: Ls[TypeArg],
+  refinement: Ls[(Tree.Ident, Type)],
+  congr: Ls[Bool], ov: Opt[Int]
+) extends BasicType:
+  private def merge(u: Ls[TypeArg], r: Ls[Tree.Ident -> Type]) =
+    val targs = args.lazyZip(u).map(_ & _)
+    val rmap = mergeMap(refinement, r)(_ & _)
+    val lbl = (refinement.iterator ++ r.iterator).map(_._1).distinct.toList
+    val refine = lbl.zip(lbl.map(rmap)).toList
+    ClassLikeType(sym, targs, refine, congr, ov)
+  def merge(cs: Ls[ClassLikeType]): Opt[Ls[ClassLikeType]] = cs match
+    case Nil => S(Ls(this))
+    case x :: xs if x.sym === sym && x.ov.isDefined =>
+      S(this :: x :: xs)
+    case x :: _ if x.sym is sym =>
+      S(Ls(cs.foldLeft(this)((x, y) => x.merge(y.args, y.refinement))))
+    case _ => N
+type ClsTag = LitSymbol | TypeSymbol | ModuleOrObjectSymbol
+
+object Discriminator extends TypeMap:
+  override def apply(pol: Bool)(t: Type) = t.simp match
+    case _: InfVar => Top
+    case c @ ClassLikeType(_: LitSymbol, _,_,_,_) => c
+    case c @ ClassLikeType(s: (TypeSymbol | ModuleOrObjectSymbol), args, refine,congr,ov) =>
+      // TODO flags in `s.defn.get.tparams`
+      val a = args.iterator.zip(congr).map:
+        case (t, true) => Wildcard.out(apply(pol)(t.posPart)) // TODO
+        case _ => Wildcard.empty
+      ClassLikeType(s, a.toList, refine.mapValues(apply(pol)), congr,ov)
+    case t @ Neg(ClassLikeType(_, _, refine, _,_)) => if refine.isEmpty then t else Top
+    case t => super.apply(pol)(t)
diff --git a/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala
new file mode 100644
index 0000000000..194360d695
--- /dev/null
+++ b/hkmc2/shared/src/main/scala/hkmc2/typing/logicsub.scala
@@ -0,0 +1,471 @@
+package hkmc2
+package typing
+package logicsub
+
+
+import scala.collection.mutable.{HashSet, HashMap, ListBuffer}
+import scala.annotation.tailrec
+
+import hkmc2.utils.*, shorthands.*
+import utils.*
+
+import Message.MessageContext
+import semantics.*, Term.*, ucs.FlatPattern
+import Elaborator.Ctx
+import syntax.*
+import Tree.*
+import utils.Scope
+import hkmc2.codegen.ErasedType.eraseSign
+
+
+class Typer(using elState: Elaborator.State, tl: TL, raise: Raise):
+  import tl.{trace, log}
+  private val builtinOps = Elaborator.binaryOps ++ Elaborator.unaryOps ++ Elaborator.aliasOps.keySet
+
+  private def error(msg: Ls[Message -> Opt[Loc]], extraInfo: => Opt[Any] = N) =
+    raise(ErrorReport(msg, extraInfo = extraInfo))
+    Bot // TODO: error type?
+
+  private def freshVar(origin: Symbol | Term, hint: Str = "")(using ctx: InfCtx) =
+    InfVar(ctx.lvl, InfVarSymbol(origin, hint), false)
+  private def freshWildcard(s: Symbol)(using InfCtx) = Wildcard(freshVar(s),freshVar(s))
+  private def freshOuter(sym: Symbol)(using ctx: InfCtx): InfVar =
+    InfVar(ctx.lvl + 1, InfVarSymbol(sym), true)
+  private def freshEnv(sym: Symbol)(using ctx: InfCtx): InfVar =
+    val s = InfVarSymbol(sym)
+    val state = new InfVarState
+    ctx.varSt += s -> state
+    state.upperBounds = ctx.outRegAcc -> N :: Nil
+    state.lowerBounds = ctx.outRegAcc :: Nil
+    InfVar(ctx.lvl, s, false)
+
+  private def mono(ty: InfType)(using InfCtx): Opt[Type] = ty match
+    case x: Type => S(x)
+    case PolyFunType(args, ret, eff) =>
+      val a = args.map(mono)
+      val r = mono(ret)
+      if (r::a).exists(_.isEmpty) then N
+      else S(InfCtx.funTy(a.flatten, r.get, eff))
+    case _ => N
+
+  private def monoOrErr(ty: InfType, sc: Located)(using InfCtx): Type =
+    mono(ty).getOrElse(error(msg"General type is not allowed here." -> sc.toLoc :: Nil))
+
+  private def tryMkMono(ty: InfType, sc: Located)(using InfCtx, CCtx, Scope): Type = ty match
+    case pt: PolyType => tryMkMono(instantiate(pt), sc)
+    case ft: PolyFunType =>
+      mono(ft).getOrElse:
+        error(msg"Expected a monomorphic type or an instantiable type here, but ${ty.show} found" -> sc.toLoc :: Nil)
+    case ty: Type => ty
+
+  private def typeAndSubstType(ty: Term, pol: Bool)
+      (using map: Map[LocalSymbol, TypeArg], ctx: InfCtx, cctx: CCtx)
+    : InfType =
+    def mono(ty: Term, pol: Bool): Type = monoOrErr(typeAndSubstType(ty, pol), ty)
+    trace[InfType](s"${ctx.lvl}. Typing type ${ty.showDbg}", r => s"~> ${r.showDbg}"):
+      ty match
+        case Ref(sym: LocalSymbol) =>
+          log(s"Type lookup: ${sym.nme} ${sym.uid} ${map.keySet}")
+          map.get(sym) match
+            case S(Wildcard(in, out)) => if pol then out else in
+            case S(ty: Type) => ty
+            case N => ctx.get(sym) match
+              case S(ty) => ty
+              case _ => error(msg"Variable not found: ${sym.nme}" -> ty.toLoc :: Nil)
+        case Term.TyApp(cls, targs) =>
+          // log(s"Type application: ${cls.nme} with ${targs}")
+          cls.symbol.flatMap(_.asTpe) match
+            case S(tpeSym) =>
+              if tpeSym.nme === "Any" then Top // FIXME hygiene
+              else if tpeSym.nme === "Nothing" then Bot // FIXME hygiene
+              else
+                val defn = tpeSym.defn.get
+                if targs.length != defn.tparams.length then
+                  error(msg"Type arguments do not match class definition" -> ty.toLoc :: Nil)
+                val ts = defn.tparams.lazyZip(targs).map: (tp, t) =>
+                  t match
+                  case Term.WildcardTy(in, out) => Wildcard(
+                      in.fold(Bot)(t => mono(t, !pol)),
+                      out.fold(Top)(t => mono(t, pol))
+                    )
+                  case _ =>
+                    val ta = mono(t, pol)
+                    tp.vce match
+                      case S(false) => Wildcard.in(ta)
+                      case S(true) => Wildcard.out(ta)
+                      case N => ta
+                val fs = ts.map(_ => false) // TODO
+                ClassLikeType(tpeSym, ts, Nil, fs, N)
+            case N => error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil)
+        case FunTy(Term.Tup(params), ret, eff) =>
+          val p = params.map {
+            case Fld(_, p, _) => typeAndSubstType(p, !pol)
+            case spd: Spd => lastWords(s"unexpected spread in function type parameters: $spd")
+          }
+          val e = eff.fold(Bot): e =>
+            typeAndSubstType(e, pol) match
+              case t: Type => t
+              case _ => error(msg"Effect cannot be polymorphic." -> ty.toLoc :: Nil)
+          PolyFunType(p, typeAndSubstType(ret, pol), e)
+        case f @ Forall(tvs, outer, body) =>
+          val outsym = outer.getOrElse(TempSymbol(S(f), erasedType = N, "outer"))
+          val outVar = freshOuter(outsym)(using ctx)
+          val nestCtx = ctx.nestWithOuter(outVar)
+          outer.foreach(sym => nestCtx += sym -> outVar)
+          given InfCtx = nestCtx
+          genPolyType(tvs, outVar, typeAndSubstType(body, pol))
+        case Neg(t) => ~mono(t, !pol)
+        case CompType(lhs, rhs, pol) =>
+          if pol then mono(lhs, pol) | mono(rhs, pol) else mono(lhs, pol) & mono(rhs, pol)
+        case UnitVal() => InfCtx.objTy
+        case Lit(x) => InfCtx.litTy(x)
+        case _ => ty.symbol.flatMap(_.asTpe) match
+          case S(cls: (ClassSymbol | TypeAliasSymbol)) => typeAndSubstType(Term.TyApp(ty, Nil)(N), pol)
+          case _ => error(msg"Invalid type" -> ty.toLoc :: Nil, S(ty)) // TODO
+
+  private def genPolyType(tvs: Ls[QuantVar], outer: InfVar, body: => InfType)
+      (using ctx: InfCtx, cctx: CCtx) =
+    val bds = tvs.map:
+      case qv @ QuantVar(sym, ub, lb) =>
+        val tv = freshVar(sym)
+        ctx += sym -> tv // TODO: a type var symbol may be better...
+        tv -> qv
+    bds.foreach:
+      case (tv, QuantVar(_, ub, lb)) =>
+        val v = ctx.varSt.getOrElseUpdate(tv.sym, new InfVarState)
+        ub.foreach(ub => v.upperBounds = typeMonoType(ub) -> N :: v.upperBounds)
+        lb.foreach(lb => v.lowerBounds = typeMonoType(lb) :: v.lowerBounds)
+        val lbty = ctx.lbs(tv.sym).foldLeft[Type](Bot)(_ | _)
+        val ubty = ctx.ubs(tv.sym).foldLeft[Type](Top)(_ & _)
+        constrain(lbty, ubty)
+    PolyType(bds.map(_._1), S(outer), Nil, body)
+
+  private def typeType(ty: Term)(using ctx: InfCtx, cctx: CCtx): InfType =
+    typeAndSubstType(ty, true)(using Map.empty)
+  private def typeMonoType(ty: Term)(using InfCtx, CCtx) = monoOrErr(typeType(ty), ty)
+
+  def typePurely(t: Term)(using InfCtx, Scope) =
+    val (ty, eff) = typeCheck(t)
+    given CCtx = CCtx.init(t, N)
+    constrain(eff, Bot)
+    ty
+
+  private def constrain(x: Type, y: Type)(using ctx: InfCtx, cctx: CCtx): Unit =
+    ctx.constrain(K(x,y,N)) // TODO
+
+  private def fundef(sym: Symbol, lam: Term, sig: Opt[Term])
+      (using ctx: InfCtx, cctx: CCtx, scope: Scope) = lam match
+    case Term.Lam(params, body) => sig match
+      case S(sig) =>
+        val sigTy = typeType(sig)
+        ctx += sym -> sigTy
+        ascribe(lam, sigTy)
+        ()
+      case N =>
+        val outer = freshOuter(new TempSymbol(S(lam), erasedType = N, "outer"))(using ctx)
+        given InfCtx = ctx.nestWithOuter(outer)
+        val funTyV = freshVar(sym)
+        ctx += sym -> funTyV // for recursive functions
+        val (res, _) = typeCheck(lam)
+        val funTy = tryMkMono(res, lam)
+        {
+          given CCtx = CCtx.init(lam, N)
+          constrain(funTy, funTyV)
+          ctx += sym -> generalize(funTy, S(outer), ctx.lvl + 1)
+        }
+    case _ =>
+      error(msg"Function definition shape not yet supported for ${sym.nme}" -> lam.toLoc :: Nil)
+
+
+  private class Subst(map: Map[InfVarSymbol, InfVar]) extends TypeMap:
+    override def apply(pol: Bool)(t: Type) = t.toBasic match
+      case v @ InfVar(_, s, _) => map.get(s).getOrElse(v)
+      case t => super.apply(pol)(t)
+
+  private def substMono(map: Map[InfVarSymbol, InfVar])(x: Type): Type =
+    Subst(map)(true)(x)
+
+  private def substMono(map: Map[InfVarSymbol, InfVar])(x: K): K = x match
+    case K(x, y, cs) => K(substMono(map)(x), substMono(map)(y), cs.map(_.map(substMono(map))))
+
+  private def subst(map: Map[InfVarSymbol, InfVar])(x: InfType): InfType =
+    x match
+      case _: PolyType => ???
+      case PolyFunType(args, ret, eff) =>
+        PolyFunType(args.map(subst(map)), subst(map)(ret), substMono(map)(eff))
+      case x: Type => substMono(map)(x)
+
+  private def instantiate(x: PolyType)(using ctx: InfCtx, cctx: CCtx) =
+    val PolyType(tvs, outer, xbds, body) = x
+    val env = freshEnv(new TempSymbol(N, erasedType = N, "env"))
+    val map = (outer.map(_.sym -> env).toList ++ tvs.map(v =>
+      val nv = InfVar(ctx.lvl, InfVarSymbol(InstSymbol(v.sym), v.sym.hint), false)
+      tl.log(s"instantiate ${v.showDbg} ~> ${nv.showDbg}")
+      v.sym -> nv
+    )).toMap
+    tvs.foreach: v =>
+      ctx.varSt.get(v.sym).foreach: st =>
+        val ns = new InfVarState
+        ctx.varSt += map(v.sym).sym -> ns
+        ns.upperBounds = st.upperBounds.map: d =>
+          substMono(map)(d._1) -> d._2.map(_.map(substMono(map)))
+        ns.lowerBounds = st.lowerBounds.map(substMono(map))
+    // TODO bound scheme
+    xbds.foreach(k => ctx.constrain(substMono(map)(k)))
+    subst(map)(body)
+
+  private def skolemize(x: PolyType)(using ctx: InfCtx, cctx: CCtx) =
+    val PolyType(tvs, outer, xbds, body) = x
+    // * Note that by this point, the state is supposed to be frozen/treated as immutable
+    // * `outer` is already skolemized when it is declared
+    val map = tvs.map(v =>
+      val sk = InfVar(ctx.lvl, InfVarSymbol(InstSymbol(v.sym), v.sym.hint), true)
+      tl.log(s"skolemize ${v.showDbg} ~> ${sk.showDbg}")
+      v.sym -> sk
+    ).toMap
+    tvs.foreach: v =>
+      ctx.varSt.get(v.sym).foreach: st =>
+        val ns = new InfVarState
+        ctx.varSt += map(v.sym).sym -> ns
+        ns.upperBounds = st.upperBounds.map: d =>
+          substMono(map)(d._1) -> d._2.map(_.map(substMono(map)))
+        ns.lowerBounds = st.lowerBounds.map(substMono(map))
+    // xbds.foreach(k => ctx.constrain(substMono(map)(k)))
+    subst(map)(body)
+
+  private def generalize(ty: InfType, outer: Opt[InfVar], lvl: Int): PolyType = ???
+
+  private def app(lhs: InfType, lhsEff: Type, rhs: Ls[Elem], t: Term)
+      (using ctx: InfCtx, cctx: CCtx, scope: Scope)
+    : (InfType, Type) = lhs match
+    case PolyFunType(params, ret, eff) =>
+    // * if the function type is known, we can directly use it
+      if params.length != rhs.length
+      then (error(msg"Incorrect number of arguments" -> t.toLoc :: Nil), Bot)
+      else
+        var resEff: Type = lhsEff | eff
+        rhs.lazyZip(params).foreach:
+          case (f: Fld, t) =>
+            val (ty, ef) = ascribe(f.term, t)
+            resEff |= ef
+          case (spd: Spd, _) => TODO(s"spread arguments: $spd")
+        (ret, resEff)
+    case ClassLikeType(s, (params: ClassLikeType) :: ret :: eff :: Nil, _,_,_)
+        if s === ctx.prim.fnSym => // && params.sym === ctx.prim.objSym =>
+      app(PolyFunType(params.refinement.values.toList, ret.posPart, eff.posPart), lhsEff, rhs, t)
+    case ty: PolyType => app(instantiate(ty), lhsEff, rhs, t)
+    case funTy =>
+      val (argTy, argEff) = rhs.flatMap:
+          case f: Fld =>
+            val (ty, eff) = typeCheck(f.term)
+            Left(ty) :: Right(eff) :: Nil
+          case spd: Spd => TODO(s"spread arguments: $spd")
+        .partitionMap(x => x)
+      val effVar = freshVar(TempSymbol(S(t), erasedType = N, "eff"))
+      val retVar = freshVar(TempSymbol(S(t), erasedType = N, "app"))
+      constrain(tryMkMono(funTy, t), InfCtx.funTy(argTy.map(tryMkMono(_, t)), retVar, effVar))
+      (retVar, argEff.foldLeft[Type](effVar | lhsEff)((res, e) => res | e))
+
+
+  private def selproj(t: Term, cls: Term, field: Tree.Ident)(using InfCtx, CCtx, Scope)
+    : (InfType, Type) =
+    val (ty, eff) = typeCheck(t)
+    cls.symbol.flatMap(_.asCls.flatMap(sym => sym.defn.map(sym -> _))) match
+      case S(clsSym -> clsDfn) =>
+        val map = HashMap[LocalSymbol, TypeArg]()
+        val targs = clsDfn.tparams.map {
+          case TyParam(_, _, targ) =>
+            val ty = freshWildcard(targ)
+            map += targ -> ty
+            ty
+        }
+        val fs = targs.map(_ => false) // TODO
+        constrain(tryMkMono(ty, t), ClassLikeType(clsSym, targs, Nil, fs, N))
+        require(clsDfn.paramsOpt.forall(_.restParam.isEmpty))
+        (clsDfn.paramsOpt.fold(Nil)(_.params).map {
+          case Param(_, sym, sign, _) =>
+            if sym.nme === field.name then sign else N
+        }.filter(_.isDefined)) match
+          case S(res) :: Nil => (typeAndSubstType(res, pol = true)(using map.toMap), eff)
+          case _ => (error(msg"${field.name} is not a valid member in class ${clsSym.nme}" -> t.toLoc :: Nil), Bot)
+      case N => 
+        (error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil), Bot)
+
+  private def newobj(cls: Term, args: Ls[Term])(using InfCtx, CCtx, Scope) =
+    cls.symbol.flatMap(_.asCls.flatMap(_.defn)) match
+    case S(clsDfn: ClassDef.Parameterized) =>
+      require(clsDfn.paramsOpt.forall(_.restParam.isEmpty))
+      val argsList = args match
+        case Nil => Nil
+        case Term.Tup(elems) :: Nil => elems.map:
+          case PlainFld(term) => term
+          case _ => ???
+        case _ => ???
+      if argsList.length != clsDfn.params.params.length then
+        (error(msg"The number of parameters is incorrect" -> cls.toLoc :: Nil), Bot)
+      else
+        val map = HashMap[LocalSymbol, TypeArg]()
+        val targs = clsDfn.tparams.map {
+          case TyParam(_, S(_), targ) =>
+            val ty = freshVar(targ)
+            map += targ -> ty
+            ty
+          case TyParam(_, N, targ) =>
+            // val ty = freshWildcard // FIXME probably not correct
+            val ty = freshVar(targ)
+            map += targ -> ty
+            ty
+        }
+        val effBuff = ListBuffer.empty[Type]
+        require(clsDfn.paramsOpt.forall(_.restParam.isEmpty))
+        argsList.iterator.zip(clsDfn.params.params).foreach {
+          case (arg, Param(sign = S(sign))) =>
+            val (ty, eff) = ascribe(arg, typeAndSubstType(sign, pol = true)(using map.toMap))
+            effBuff += eff
+          case _ => ???
+        }
+        val fs = targs.map(_ => false) // TOOD
+        (ClassLikeType(clsDfn.sym, targs, Nil, fs, N), effBuff.foldLeft[Type](Bot)((res, e) => res | e))
+    case S(clsDfn: ClassDef.Plain) => ??? // TODO
+    case N => 
+      (error(msg"Not a valid class: ${cls.describe}" -> cls.toLoc :: Nil), Bot)
+
+  def ascribe(lhs: Term, rhs: InfType)(using ctx: InfCtx, scope: Scope): (InfType, Type) = // TODO
+  trace[(InfType, Type)](s"${ctx.lvl}. Ascribing ${lhs.showDbg} : ${rhs.showDbg}", res => s"! ${res._2.showDbg}"):
+    given CCtx = CCtx.init(lhs, S(rhs))
+    (lhs, rhs) match
+    case (Term.Lam(PlainParamList(params), body), ft @ PolyFunType(args, ret, eff)) => // * annoted functions
+      if params.length != args.length then
+        (error(msg"Cannot type this ${lhs.describe} as ${rhs.show}" -> lhs.toLoc :: Nil), Bot)
+      else
+        val nestCtx = ctx.nest
+        val argsTy = params.zip(args).map:
+          case (Param(sym = sym), ty) =>
+            nestCtx += sym -> ty
+            ty
+        given InfCtx = nestCtx
+        val (_, effTy) = ascribe(body, ret)
+        constrain(effTy, eff)
+        (ft, Bot)
+    case (Term.Lam(params, body), ft @ ClassLikeType(fn, (args: ClassLikeType)::ret::eff::Nil, _,_,_))
+        if fn === ctx.prim.fnSym =>
+      ascribe(lhs, PolyFunType(args.refinement.values.toList, ret.posPart, eff.posPart))
+    case (term, pt @ PolyType(_, outer, _, _)) => // * generalize
+      val nextCtx = outer match
+        case S(outer) => ctx.nestWithOuter(outer)
+        case N => ctx.nextLevel
+      given InfCtx = nextCtx
+      constrain(ascribe(term, skolemize(pt))._2, Bot) // * never generalize terms with effects
+      (pt, Bot)
+    // case (Term.IfLike(_, IfLikeForm.ReturningIf, split), ty) => // * propagate
+    //   typeAllSplits(split.getExpandedSplit, S(ty))
+    case (Term.Asc(term, ty), rhs) =>
+      ascribe(term, typeType(ty))
+      ascribe(term, rhs)
+    case (lhs, rhs: Type) => rhs.conjuncts.toList match
+      case rhs :: Nil =>
+        val (lhsTy, eff) = typeCheck(lhs)
+        constrain(tryMkMono(lhsTy, lhs), monoOrErr(rhs, lhs))
+        (rhs, eff)
+      case cs =>
+        val e = cs.map(c => ascribe(lhs, c)._2).reduce(_|_)
+        (rhs, e)
+    case _ =>
+      val (lhsTy, eff) = typeCheck(lhs)
+      rhs match
+        case pf: PolyFunType if mono(pf).isEmpty =>
+          (error(msg"Cannot type non-function term ${lhs.toString} as ${rhs.show}" -> lhs.toLoc :: Nil), Bot)
+        case _ =>
+          constrain(tryMkMono(lhsTy, lhs), monoOrErr(rhs, lhs))
+          (rhs, eff)
+
+  def typeCheck(t: Term)(using ctx: InfCtx, scope: Scope): (InfType, Type) =
+  trace[(InfType, Type)](s"${ctx.lvl}. Typing ${t.showDbg}", r => s": (${r._1.showDbg}, ${r._2.showDbg})"):
+    given CCtx = CCtx.init(t, N)
+    t match
+      case Term.Error() => (Bot, Bot) // TODO: error type?
+      case UnitVal() => (InfCtx.objTy, Bot)
+      case Lit(lit) => (InfCtx.litTy(lit), Bot)
+      case Ref(sym) =>
+        ctx.get(sym) match
+          case Some(ty) => (ty, Bot)
+          case _ => (error(msg"Variable not found: ${sym.nme}" -> t.toLoc :: Nil), Bot)
+      case t @ Term.App(lhs, Term.Tup(rhs)) =>
+        val (funTy, lhsEff) = typeCheck(lhs)
+        app(funTy, lhsEff, rhs, t)
+      case trm @ Term.Sel(t, l) =>
+        val (ty, eff) = typeCheck(t)
+        val r = freshVar(trm, "")
+        constrain(tryMkMono(ty, t) , InfCtx.refinedObj(Ls(l -> r)))
+        (r, eff)
+      case sel @ Term.SynthSel(Ref(_: TopLevelSymbol), nme) if sel.symbol.isDefined =>
+        typeCheck(Ref(sel.symbol.get)(sel.nme, N))
+      case Term.SelProj(term, cls, field) => selproj(term, cls, field)
+      case Term.Tup(fields) => // TODO tup type
+        var eff: Type = Bot
+        val fs = fields.zipWithIndex.map:
+          case (f: Fld, i) =>
+            val (ty, ef) = typeCheck(f.term)
+            eff |= ef
+            (Tree.Ident(i.toString): Tree.Ident, tryMkMono(ty, f))
+          case (spd: Spd, _) => TODO(s"spread arguments: $spd")
+        (InfCtx.refinedObj(fs), eff)
+      // case Term.IfLike(_, IfLikeForm.ReturningIf, split) => typeAllSplits(split.getExpandedSplit, N)
+      case Lam(PlainParamList(params), body) =>
+        val nestCtx = ctx.nest
+        given InfCtx = nestCtx
+        val tvs = params.map:
+          case Param(_, sym, sign, _) =>
+            val ty = sign.map(s => typeType(s)(using nestCtx)).getOrElse(freshVar(sym))
+            nestCtx += sym -> ty
+            ty
+        val (bodyTy, eff) = typeCheck(body)
+        (PolyFunType(tvs, bodyTy, eff), Bot)     
+      case Blk(stats, res) =>
+        val effBuff = ListBuffer.empty[Type]
+        def goStats(stats: Ls[Statement]): Unit = stats match
+          case Nil => ()
+          case (term: Term) :: stats =>
+            effBuff += typeCheck(term)._2
+            goStats(stats)
+          case LetDecl(sym, _) :: DefineVar(sym2, rhs) :: stats =>
+            require(sym2 is sym)
+            val (rhsTy, eff) = typeCheck(rhs)
+            effBuff += eff
+            ctx += sym -> rhsTy
+            goStats(stats)
+          case (td @ TermDefinition(k = Fun, params = ps :: Nil, sign = sig, body = S(body))) :: stats =>
+            fundef(td.sym, Term.Lam(ps, body), sig)
+            goStats(stats)
+          case (td @ TermDefinition(k = Fun, params = Nil, sign = sig, body = S(body))) :: stats =>
+            fundef(td.sym, body, sig)  // * may be a case expressions
+            goStats(stats)
+          case (td1 @ TermDefinition(k = Fun, sign = S(sig), body = None)) :: (td2 @ TermDefinition(k = Fun, body = S(body))) :: stats
+           if td1.sym === td2.sym => goStats(td2 :: stats) // * avoid type check signatures twice
+          case (td @ TermDefinition(k = Fun, sign = S(sig), body = None)) :: stats =>
+            ctx += td.sym -> typeType(sig)
+            goStats(stats)
+          case (clsDef: ClassDef) :: stats =>
+            // typeNames.add(clsDef.sym.nme)
+            // clsDef.ext match
+            //   case S(Term.New(ty, _, N)) => createADTCtor(clsDef, ty)
+            //   case _ => ()
+            goStats(stats)
+          case (modDef: ModuleOrObjectDef) :: stats =>
+            // typeNames.add(modDef.sym.nme)
+            goStats(stats)
+          case Import(sym, str, pth) :: stats =>
+            goStats(stats) // TODO:
+          case (_: SetConfig) :: _ =>
+          case stat :: _ =>
+            TODO(stat)
+        goStats(stats)
+        val (ty, eff) = typeCheck(res)
+        (ty, effBuff.foldLeft(eff)((res, e) => res | e))
+      case Term.New(cls, args, N) => newobj(cls, args)
+      case Term.Asc(term, ty) =>
+        val res = typeType(ty)(using ctx)
+        ascribe(term, res)
+      case Term.Annotated(Annot.Untyped, _) => (Bot, Bot)
+      case _ =>
+        (error(msg"Term shape not yet supported: ${t.toString}" -> t.toLoc :: Nil), Bot)
diff --git a/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls b/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls
index c8dbcfe0d3..89e8cd5faf 100644
--- a/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls
+++ b/hkmc2/shared/src/test/mlscript/codegen/ConfigDirective.mls
@@ -217,6 +217,7 @@ applyTwice(fst, Pair(1, 2))
   allowUnresolvedAccesses: true,
   useNewResolution: false,
   typeCheck: Some(TypeChecking()))
+//│ Type: undefined
 
 #config(language: Language(
   allowUnresolvedAccesses: false,
diff --git a/hkmc2/shared/src/test/mlscript/logicsub/test.mls b/hkmc2/shared/src/test/mlscript/logicsub/test.mls
new file mode 100644
index 0000000000..45ece01d1a
--- /dev/null
+++ b/hkmc2/shared/src/test/mlscript/logicsub/test.mls
@@ -0,0 +1,29 @@
+#config(language: Language(typeCheck: TypeChecking()))
+//│ Type: undefined
+
+fun f: (1 -> 1) & (("a"|"B") -> ("a"|"B"|"c"))
+fun f(x) = x
+//│ Type: undefined
+
+f(1)
+//│ Type: 'app
+//│   >: 1
+
+f("a")
+//│ Type: 'app
+//│   >: ("c" ∨ "B") ∨ "a"
+
+fun g: (Int -> Int) & (Str -> Str)
+//│ Type: undefined
+
+// TODO
+g(1)
+//│ Type: 'app
+//│   >: ⊥
+
+fun g: (1 -> 1) & (2 -> 2)
+//│ Type: undefined
+
+g(1)
+//│ Type: 'app
+//│   >: 1
diff --git a/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala b/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala
new file mode 100644
index 0000000000..f62aecfdc6
--- /dev/null
+++ b/hkmc2DiffTests/src/test/scala/hkmc2/LogicSubDiffMaker.scala
@@ -0,0 +1,34 @@
+package hkmc2
+
+import hkmc2.utils.*, shorthands.*
+
+import hkmc2.semantics.*
+import hkmc2.typing.*
+import utils.Scope
+
+
+abstract class LogicSubDiffMaker extends WasmDiffMaker:
+
+  lazy val infctx =
+    given Elaborator.Ctx = curCtx
+    given Config = mkConfig
+    logicsub.InfCtx.init
+
+  var typer: Opt[logicsub.Typer] = None
+
+  override def processTerm(trm: semantics.Term.Blk, inImport: Bool)(using Config, Raise): Unit =
+    super.processTerm(trm, inImport)
+    Config.extractConfigFromStats(trm).givenIn:
+      if summon[Config].language.typeCheck.isDefined then
+        given Scope = Scope.empty(Scope.Cfg.default)
+        if typer.isEmpty then
+          given Elaborator.Ctx = curCtx
+          typer = S(logicsub.Typer())
+        given logicsub.InfCtx = infctx
+        val ty = typer.get.typePurely(trm)
+        output(s"Type: ${ty.show}")
+        ty match
+          case x: logicsub.InfVar =>
+            output(s"  >: ${infctx.lbs(x.sym).foldLeft(logicsub.Bot:logicsub.Type)(_|_).toBasic.show}")
+          case _ =>
+
diff --git a/hkmc2DiffTests/src/test/scala/hkmc2/MainDiffMaker.scala b/hkmc2DiffTests/src/test/scala/hkmc2/MainDiffMaker.scala
index 573bf03e78..89c30aff81 100644
--- a/hkmc2DiffTests/src/test/scala/hkmc2/MainDiffMaker.scala
+++ b/hkmc2DiffTests/src/test/scala/hkmc2/MainDiffMaker.scala
@@ -9,7 +9,7 @@ import hkmc2.utils.*, shorthands.*
 
 abstract class MainDiffMaker
     (val rootPath: Str, val file: io.Path, val preludeFile: io.Path, val predefFile: io.Path, val relativeName: Str)
-  extends WasmDiffMaker:
+  extends LogicSubDiffMaker:
     
     // println(s"Running diff test for $relativeName") // * useful to debug nonterminating tests