[type checking] Solve meta right before failing subsumption check

Author: tgeng

.idea/modules/archon.archon-build.iml

@@ -21,6 +21,7 @@ lazy val root = (project in file("."))
       "com.lihaoyi" %% "pprint" % "0.9.0",
       "com.lihaoyi" %% "fastparse" % "3.1.0",
       "com.lihaoyi" %% "os-lib" % "0.10.2",
+      "org.scala-lang.modules" %% "scala-collection-contrib" % "0.3.0"
     ),
     Compile / unmanagedJars += {
       baseDirectory.value / "unmanaged" / "scalaz3_3-4.8.14-macos-aarch64.jar"

.idea/modules/archon.iml

@@ -12,6 +12,7 @@ import com.github.tgeng.archon.core.ir.Pattern.*
 import com.github.tgeng.archon.core.ir.VTerm.*
 import com.github.tgeng.archon.core.ir.Variance.*
 
+import scala.collection.decorators.*
 import scala.collection.mutable
 import scala.collection.mutable.ArrayBuffer
 
@@ -219,6 +220,27 @@ object PrettyPrinter extends Visitor[PPrintContext, Block]:
     : Block =
     Block(usageLiteral.usage.toString)
 
+  override def visitUsageProd
+    (usageProd: VTerm.UsageProd)
+    (using ctx: PPrintContext)
+    (using Σ: Signature)
+    : Block =
+    Block(usageProd.operands.toSeq.map(visitVTerm).intersperse("*"), Whitespace, Aligned, Wrap)
+
+  override def visitUsageSum
+    (usageSum: VTerm.UsageSum)
+    (using ctx: PPrintContext)
+    (using Σ: Signature)
+    : Block =
+    Block(usageSum.operands.multiToSeq.map(visitVTerm).intersperse("+"), Whitespace, Aligned, Wrap)
+
+  override def visitUsageJoin
+    (usageJoin: VTerm.UsageJoin)
+    (using ctx: PPrintContext)
+    (using Σ: Signature)
+    : Block =
+    Block(usageJoin.operands.toSeq.map(visitVTerm).intersperse("|"), Whitespace, Aligned, Wrap)
+
   override def visitTContext
     (tTelescope: List[(Binding[VTerm], Variance)])
     (using PPrintContext)
@@ -434,7 +456,7 @@ object PrettyPrinter extends Visitor[PPrintContext, Block]:
     (using
       Σ: Signature,
     )
-    : Block = app(".return", r.v)
+    : Block = app(".return", "[", r.usage, "]", r.v)
 
   override def visitLet
     (let: Let)

build.sbt

@@ -544,7 +544,7 @@ extension (v: VTerm)
 
         def sumToTerm(sum: USum[VTerm]): VTerm = UsageSum(sum.map(prodToTerm)*)
 
-        def prodToTerm(prod: UProd[VTerm]): VTerm = UsageProd(prod.map(varOrUsageToTerm).toSeq*)
+        def prodToTerm(prod: UProd[VTerm]): VTerm = UsageProd(prod.map(varOrUsageToTerm)*)
 
         def varOrUsageToTerm(t: VTerm | Usage): VTerm = t match
           case v: VTerm => v

src/main/scala/com/github/tgeng/archon/core/ir/pprint.scala

@@ -368,7 +368,11 @@ private def checkHandlerTypeSubsumption
       Set(Constraint.HandlerTypeSubsumption(Γ, handlerType1, handlerType2))
     case (_: ResolvedMetaVariable, _: ResolvedMetaVariable) =>
       Set(Constraint.HandlerTypeSubsumption(Γ, handlerType1, handlerType2))
-    case _ => throw NotHandlerTypeSubsumption(handlerType1, handlerType2)
+    case (sub: VTerm, sup: VTerm) =>
+      val solvedSub = ctx.solveTerm(sub)
+      val solvedSup = ctx.solveTerm(sup)
+      if solvedSub == sub && solvedSup == sup then throw NotHandlerTypeSubsumption(sub, sup)
+      else checkHandlerTypeSubsumption(solvedSub, solvedSup)
 
 @throws(classOf[IrError])
 private def checkEqDecidabilitySubsumption
@@ -390,7 +394,11 @@ private def checkEqDecidabilitySubsumption
       Set(Constraint.EqDecidabilitySubsumption(Γ, eqD1, eqD2))
     case (_: ResolvedMetaVariable, _: ResolvedMetaVariable) =>
       Set(Constraint.EqDecidabilitySubsumption(Γ, eqD1, eqD2))
-    case _ => throw NotEqDecidabilitySubsumption(eqD1, eqD2)
+    case (sub: VTerm, sup: VTerm) =>
+      val solvedSub = ctx.solveTerm(sub)
+      val solvedSup = ctx.solveTerm(sup)
+      if solvedSub == sub && solvedSup == sup then throw NotEqDecidabilitySubsumption(sub, sup)
+      else checkEqDecidabilitySubsumption(solvedSub, solvedSup)  
 
 /** @param invert
   *   useful when checking patterns where the consumed usages are actually provided usages because
@@ -442,7 +450,11 @@ def checkUsageSubsumption
       // hence we can't decide subsumption yet.
       else if spuriousOperands.forall(isMeta) || operands1.exists(isMeta) then
         Set(Constraint.UsageSubsumption(Γ, sub, sup))
-      else throw NotUsageSubsumption(sub, sup)
+      else
+        val solvedSub = ctx.solveTerm(sub)
+        val solvedSup = ctx.solveTerm(sup)
+        if solvedSub == sub && solvedSup == sup then throw NotUsageSubsumption(sub, sup)
+        else checkUsageSubsumption(solvedSub, solvedSup)
     // Handle the special case that the right hand side simply contains the left hand side as an operand.
     case (UsageJoin(operands), RUnsolved(_, _, _, tm, _)) if operands.contains(Collapse(tm)) =>
       Set.empty
@@ -512,11 +524,15 @@ def checkUsageSubsumption
       Set(Constraint.UsageSubsumption(Γ, rawSub, sup))
     case (_: ResolvedMetaVariable, _: ResolvedMetaVariable) =>
       Set(Constraint.UsageSubsumption(Γ, rawSub, rawSup))
-    case _ =>
+    case (sub: VTerm, sup: VTerm) =>
       if isMeta(rawSub) || isMeta(rawSup) then
         // We can't decide if the terms are unsolved.
         Set(Constraint.UsageSubsumption(Γ, rawSub, rawSup))
-      else throw NotUsageSubsumption(rawSub, rawSup)
+      else
+        val solvedSub = ctx.solveTerm(sub)
+        val solvedSup = ctx.solveTerm(sup)
+        if solvedSub == sub && solvedSup == sup then throw NotUsageSubsumption(sub, sup)
+        else checkUsageSubsumption(solvedSub, solvedSup)
 
 @throws(classOf[IrError])
 private def checkEffSubsumption
@@ -600,15 +616,23 @@ private def checkEffSubsumption
                 ).normalized
             ctx.updateConstraint(u, UmcEffSubsumption(newLowerBound))
             Set.empty
-          case _ => throw NotEffectSubsumption(sub, sup)
+          case _ =>
+            val solvedSub = ctx.solveTerm(sub)
+            val solvedSup = ctx.solveTerm(sup)
+            if solvedSub == sub && solvedSup == sup then throw NotEffectSubsumption(sub, sup)
+            else checkEffSubsumption(solvedSub, solvedSup)
       // If spurious operands are all stuck computation, it's possible for sub to be if all of these stuck computation
       // ends up being assigned values that are part of sup
       // Also, if sup contains stuck computation, it's possible for sup to end up including arbitrary effects and hence
       // we can't decide subsumption yet.
       else if spuriousOperands.keys.forall(isMeta) || unionOperands2.keys.exists(isMeta) then
         Set(Constraint.EffSubsumption(Γ, sub, sup))
       else throw NotEffectSubsumption(sub, sup)
-    case _ => throw NotEffectSubsumption(rawSub, rawSup)
+    case (sub: VTerm, sup: VTerm) =>
+      val solvedSub = ctx.solveTerm(sub)
+      val solvedSup = ctx.solveTerm(sup)
+      if solvedSub == sub && solvedSup == sup then throw NotEffectSubsumption(sub, sup)
+      else checkEffSubsumption(solvedSub, solvedSup)
 
 /** Checks if l1 is smaller than l2.
   */
@@ -647,7 +671,11 @@ private def checkLevelSubsumption
         // if sup contains unsolved meta variables, it's possible for sup to end up including
         // arbitrary large level and hence we can't decide subsumption yet.
         Set(Constraint.LevelSubsumption(Γ, sub, sup))
-      else throw NotLevelSubsumption(sub, sup)
+      else
+        val solvedSub = ctx.solveTerm(sub)
+        val solvedSup = ctx.solveTerm(sup)
+        if solvedSub == sub && solvedSup == sup then throw NotLevelSubsumption(sub, sup)
+        else checkLevelSubsumption(solvedSub, solvedSup)
     // Handle the special case that the right hand side simply contains the left hand side as an operand.
     case (RUnsolved(_, _, _, tm, _), Level(_, operands)) if operands.contains(Collapse(tm)) =>
       Set.empty
@@ -676,8 +704,11 @@ private def checkLevelSubsumption
       Set(Constraint.LevelSubsumption(Γ, rawSub, sup))
     case (_: ResolvedMetaVariable, _: ResolvedMetaVariable) =>
       Set(Constraint.LevelSubsumption(Γ, rawSub, rawSup))
-    case (sub, sup) =>
-      throw NotLevelSubsumption(rawSub, rawSup)
+    case (sub: VTerm, sup: VTerm) =>
+      val solvedSub = ctx.solveTerm(sub)
+      val solvedSup = ctx.solveTerm(sup)
+      if solvedSub == sub && solvedSup == sup then throw NotLevelSubsumption(sub, sup)
+      else checkLevelSubsumption(solvedSub, solvedSup)
 
 private def getSpurious[T, E: PartialOrdering](sub: SeqMap[T, E], sup: SeqMap[T, E]): SeqMap[T, E] =
   sub.filter { case (operand1, e1) =>

src/main/scala/com/github/tgeng/archon/core/ir/reduction.scala

@@ -36,7 +36,13 @@ def collectUsages
   (using Σ: Signature)
   (using ctx: TypingContext)
   : Usages =
-  ctx.trace("collectUsages", PrettyPrinter.pprint(tm)):
+  ctx.trace[Usages](
+    "collectUsages",
+    ty match
+      case Some(ty) => Block(PrettyPrinter.pprint(tm), ":", PrettyPrinter.pprint(ty))
+      case None     => PrettyPrinter.pprint(tm),
+    successMsg = PrettyPrinter.pprint,
+  ):
     tm match
       case Type(upperBound) => collectUsages(upperBound, None)
       case Top(level, eqDecidability) =>
@@ -98,7 +104,13 @@ def collectUsages
   (using Σ: Signature)
   (using ctx: TypingContext)
   : Usages =
-  ctx.trace("collectUsages", PrettyPrinter.pprint(tm)):
+  ctx.trace[Usages](
+    "collectUsages",
+    ty match
+      case Some(ty) => Block(PrettyPrinter.pprint(tm), ":", PrettyPrinter.pprint(ty))
+      case None     => PrettyPrinter.pprint(tm),
+    successMsg = PrettyPrinter.pprint,
+  ):
     tm match
       case Hole => throw IllegalStateException("Hole should not appear here.")
       case CapturedContinuationTip(_) =>
@@ -127,17 +139,22 @@ def collectUsages
             case F(ty, _, _) => ty
             case ty          => throw IllegalStateException(s"bad type, expect F but got $ty")
           },
-        ) * usage
+        ) * usage.normalized
       case Let(t, tBinding, eff, body) =>
         val tUsages = collectUsages(t, Some(F(tBinding.ty, eff, tBinding.usage)))
-        val bodyUsages = collectUsages(body, ty.map(_.weakened))(using Γ :+ tBinding)
-        val actualTUsage = bodyUsages.last
-        ctx.checkSolved(
-          checkUsageSubsumption(actualTUsage, tBinding.usage),
-          NotUsageSubsumption(actualTUsage, tBinding.usage),
-        )
+        val bodyUsages = {
+          given Context = Γ :+ tBinding
+
+          val bodyUsages = collectUsages(body, ty.map(_.weakened))
+          val actualTUsage = bodyUsages.last
+          ctx.checkSolved(
+            checkUsageSubsumption(actualTUsage, tBinding.usage),
+            NotUsageSubsumption(actualTUsage, tBinding.usage),
+          )
+          bodyUsages.dropRight(1)
+        }
         val continuationUsage = getEffectsContinuationUsage(eff)
-        tUsages + bodyUsages.dropRight(1).map { t =>
+        tUsages + bodyUsages.map { t =>
           // A variable's usage may reference the variable bound to the value returned from `t`. In
           // this case, strength would fail and the referenced usage can take any value. Hence, we
           // just approximate it with `uAny`.

src/main/scala/com/github/tgeng/archon/core/ir/subtyping.scala

@@ -128,26 +128,40 @@ class BasicTypeCheckSpec extends AnyFreeSpec:
     "with nat" in:
       decls"""
         data Nat: Type 0L
-        Zero: Nat
-        Succ: Nat -> Nat
-        
+        Z: Nat
+        S: Nat -> Nat
+
         def prec: Nat -> <> Nat
-        Zero = Zero
-        (Succ m) = m
+        Z = Z
+        (S m) = m
+
+        def plus: Nat -> Nat -> <> Nat
+        Z n = n
+        (S m) n = S (plus m n)
 
         data Vec (l: Level) +(t: Type l): Nat -> Type l
-        Nil: Vec l t Zero
-        Succ: n: Nat -> t -> Vec l t n -> Vec l t (Succ n)
+        Nil: Vec l t Z
+        Suc: n: Nat -> t -> Vec l t n -> Vec l t (S n)
+
         """.inUse:
         assertVType(vt"Nat", Type(Top(LevelLiteral(0))))
-        assertVType(vt"Zero", vt"Nat")
+        assertVType(vt"Z", vt"Nat")
+        assertCType(
+          ct"prec (S Z)",
+          ct"<> Nat",
+        )
+        assertCConvertible(
+          ct"prec (S Z)",
+          ct"Z",
+          Some(ct"<> Nat"),
+        )
         assertCType(
-          ct"prec (Succ Zero)",
+          ct"plus (S Z) (S (S Z))",
           ct"<> Nat",
         )
         assertCConvertible(
-          ct"prec (Succ Zero)",
-          ct"Zero",
+          ct"plus (S Z) (S (S Z))",
+          ct"S (S Z)",
           Some(ct"<> Nat"),
         )
   }