upgrade to scala 3.5.1 and fix compile issues

build.sbt

@@ -1,14 +1,14 @@
 Global / onChangedBuildSource := ReloadOnSourceChanges
 ThisBuild / version := "0.1.0-SNAPSHOT"
 
-ThisBuild / scalaVersion := "3.4.2"
+ThisBuild / scalaVersion := "3.5.1"
 
 lazy val root = (project in file("."))
   .settings(
     name := "archon",
     scalacOptions ++= Seq(
       "-Yexplicit-nulls",
-      "-Ykind-projector",
+      "-Xkind-projector",
       "-Xfatal-warnings",
       "-feature",
       "-deprecation",
@@ -17,10 +17,10 @@ lazy val root = (project in file("."))
       "-indent",
     ),
     libraryDependencies ++= Seq(
-      "org.scalatest" %% "scalatest" % "3.2.18" % "test",
+      "org.scalatest" %% "scalatest" % "3.2.19" % "test",
       "com.lihaoyi" %% "pprint" % "0.9.0",
-      "com.lihaoyi" %% "fastparse" % "3.1.0",
-      "com.lihaoyi" %% "os-lib" % "0.10.2",
+      "com.lihaoyi" %% "fastparse" % "3.1.1",
+      "com.lihaoyi" %% "os-lib" % "0.10.7",
       "org.scala-lang.modules" %% "scala-collection-contrib" % "0.3.0",
     ),
     Compile / unmanagedJars += {

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

@@ -2,7 +2,11 @@ package com.github.tgeng.archon.core.ir
 
 import com.github.tgeng.archon.core.common.*
 import com.github.tgeng.archon.core.common.QualifiedName.*
+import com.github.tgeng.archon.core.ir.CTerm.*
 import com.github.tgeng.archon.core.ir.Declaration.*
+import com.github.tgeng.archon.core.ir.PreDeclaration.*
+import com.github.tgeng.archon.core.ir.Usage.*
+import com.github.tgeng.archon.core.ir.VTerm.*
 
 import scala.collection.immutable.SeqMap
 
@@ -135,10 +139,6 @@ object Builtins:
       throw new IllegalArgumentException(s"Conflicting definitions: $conflictingDefs")
     elaborateAll(builtins)(using Context.empty)(using SimpleSignature())
 
-import CTerm.*
-import PreDeclaration.* import Usage.*
-  import VTerm.*
-
   private def binding(name: Name, ty: VTerm, usage: VTerm = uAny): Binding[CTerm] =
     Binding(Return(ty, uAny), Return(usage, uAny))(name)
 

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

@@ -131,23 +131,23 @@ def checkIsSubtype
     case ((_: ResolvedMetaVariable, Nil), _) | (_, (_: ResolvedMetaVariable, Nil)) =>
       Set(Constraint.CSubType(Γ, sub, sup))
     case (CType(upperBound1, eff1), CType(upperBound2, eff2)) =>
-      val effConstraint = checkEffSubsumption(eff1, eff2)
+      val effConstraint = checkEffectSubsumption(eff1, eff2)
       val upperBoundConstraint = checkIsSubtype(upperBound1, upperBound2)
       effConstraint ++ upperBoundConstraint
     case (ty: IType, CTop(level2, eff2)) =>
       val levelConstraint = checkLevelSubsumption(inferLevel(sub), level2)
-      val effConstraint = checkEffSubsumption(ty.effects, eff2)
+      val effConstraint = checkEffectSubsumption(ty.effects, eff2)
       levelConstraint ++ effConstraint
     case (F(vTy1, eff1, u1), F(vTy2, eff2, u2)) =>
-      val effConstraint = checkEffSubsumption(eff1, eff2)
+      val effConstraint = checkEffectSubsumption(eff1, eff2)
       val usageConstraint = checkUsageSubsumption(u1, u2)
       val tyConstraint = checkIsSubtype(vTy1, vTy2)
       effConstraint ++ usageConstraint ++ tyConstraint
     case (
         FunctionType(binding1, bodyTy1, eff1),
         FunctionType(binding2, bodyTy2, eff2),
       ) =>
-      val effConstraint = checkEffSubsumption(eff1, eff2)
+      val effConstraint = checkEffectSubsumption(eff1, eff2)
       val tyConstraint = ctx.solve(checkIsSubtype(binding2.ty, binding1.ty))
       val usageConstraint = ctx.solve(checkUsageSubsumption(binding2.usage, binding1.usage))
       val bodyConstraint =
@@ -177,7 +177,7 @@ def checkIsSubtype
         case None => throw MissingDeclaration(qn1)
         case Some(record) =>
           val args = ArrayBuffer[VTerm]()
-          val effConstraint = checkEffSubsumption(eff1, eff2)
+          val effConstraint = checkEffectSubsumption(eff1, eff2)
           val argConstraint = args1
             .zip(args2)
             .zip(record.context)
@@ -449,6 +449,8 @@ def checkUsageSubsumption
           )
           Set.empty
         case _ => Set(Constraint.UsageSubsumption(Γ, sub, rawSup))
+    case (_: VTerm, r: ResolvedMetaVariable) =>
+      throw IllegalStateException(s"Expected unsolved usage meta var but got $r")
     case (_: ResolvedMetaVariable, sup: VTerm) =>
       Set(Constraint.UsageSubsumption(Γ, rawSub, sup))
     case (_: ResolvedMetaVariable, _: ResolvedMetaVariable) =>
@@ -464,12 +466,12 @@ def checkUsageSubsumption
         else checkUsageSubsumption(solvedSub, solvedSup)
 
 @throws(classOf[IrError])
-private def checkEffSubsumption
+private def checkEffectSubsumption
   (rawSub: VTerm, rawSup: VTerm)
   (using Γ: Context)
   (using Σ: Signature)
   (using ctx: TypingContext)
-  : Set[Constraint] = debugSubsumption("checkEffSubsumption", rawSub, rawSup):
+  : Set[Constraint] = debugSubsumption("checkEffectSubsumption", rawSub, rawSup):
   check2(rawSub, rawSup):
     case (sub, sup) if sub == sup => Set.empty
     // Handle the special case that the right hand side simply contains the left hand side as an operand.
@@ -501,6 +503,8 @@ private def checkEffSubsumption
             case _ => throw IllegalStateException("type error")
           ctx.updateConstraint(u, UmcEffSubsumption(newLowerBound))
           Set.empty
+    case (_: VTerm, r: ResolvedMetaVariable) =>
+      throw IllegalStateException(s"Expected unsolved effect meta var but got $r")
     // If upper bound is total, the meta variable can only take total as the value.
     case (
         u @ RUnsolved(_, _, UmcEffSubsumption(_), _, _),
@@ -549,7 +553,7 @@ private def checkEffSubsumption
             val solvedSub = ctx.solveTerm(sub)
             val solvedSup = ctx.solveTerm(sup)
             if solvedSub == sub && solvedSup == sup then throw NotEffectSubsumption(sub, sup)
-            else checkEffSubsumption(solvedSub, solvedSup)
+            else checkEffectSubsumption(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
@@ -561,7 +565,7 @@ private def checkEffSubsumption
       val solvedSub = ctx.solveTerm(sub)
       val solvedSup = ctx.solveTerm(sup)
       if solvedSub == sub && solvedSup == sup then throw NotEffectSubsumption(sub, sup)
-      else checkEffSubsumption(solvedSub, solvedSup)
+      else checkEffectSubsumption(solvedSub, solvedSup)
 
 /** Checks if l1 is smaller than l2.
   */
@@ -605,6 +609,8 @@ private def checkLevelSubsumption
         val solvedSup = ctx.solveTerm(sup)
         if solvedSub == sub && solvedSup == sup then throw NotLevelSubsumption(sub, sup)
         else checkLevelSubsumption(solvedSub, solvedSup)
+    case (_: VTerm, r: ResolvedMetaVariable) =>
+      throw IllegalStateException(s"Expected unsolved level meta var but got $r")
     // 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

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

@@ -193,8 +193,6 @@ object LevelOrder:
   // 256 is arbitrary but it should be enough for any practical purpose
   val upperBound: LevelOrder = LevelOrder(256, 0)
 
-extension (o: LevelOrder) infix def suc(n: Nat): LevelOrder = LevelOrder(o.m, o.n + n)
-
 sealed trait UsageCompound(val distinctOperands: Set[VTerm])
 
 /** @param body

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

@@ -846,7 +846,7 @@ def checkHandler
           ExpectU1Effect(qn),
         )
         ctx.checkSolved(
-          checkEffSubsumption(
+          checkEffectSubsumption(
             bodyTy.asInstanceOf[F].effects,
             EffectsRetainSimpleLinear(implOutputEffects),
           ),

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

@@ -301,7 +301,7 @@ class TypingContext
       case UmcNothing               => Set.empty
       case UmcCSubtype(lowerBounds) => lowerBounds.map(checkIsSubtype(_, value)).flatten
       case UmcVSubtype(lowerBounds) => lowerBounds.map(checkIsSubtype(_, Collapse(value))).flatten
-      case UmcEffSubsumption(lowerBound)   => checkEffSubsumption(lowerBound, Collapse(value))
+      case UmcEffSubsumption(lowerBound)   => checkEffectSubsumption(lowerBound, Collapse(value))
       case UmcLevelSubsumption(lowerBound) => checkLevelSubsumption(lowerBound, Collapse(value))
       case UmcUsageSubsumption(lowerBounds, upperBound) =>
         lowerBounds.flatMap(lb => checkUsageSubsumption(Collapse(value), lb)) ++
@@ -567,7 +567,7 @@ class TypingContext
       case Constraint.CSubType(context, sub, sup) =>
         checkIsSubtype(sub, sup)(using context)
       case Constraint.EffSubsumption(context, sub, sup) =>
-        checkEffSubsumption(sub, sup)(using context)
+        checkEffectSubsumption(sub, sup)(using context)
       case Constraint.LevelSubsumption(context, sub, sup) =>
         checkLevelSubsumption(sub, sup)(using context)
       case Constraint.UsageSubsumption(context, sub, sup) =>

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

@@ -94,6 +94,8 @@ def collectUsages
       case LevelType(_) => Usages.zero
       case Level(_, maxOperands) =>
         maxOperands.keys.map(collectUsages(_, Some(LevelType()))).fold(Usages.zero)(_ + _)
+      case EffectInstanceType(eff, _) => collectEffUsages(eff)
+      case EffectInstance(eff, _, _)  => collectEffUsages(eff)
       case Auto() =>
         throw IllegalStateException("All auto should have been replaced by meta variables.")