fix test

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

@@ -113,6 +113,7 @@ object Builtins:
   val EffectsRetainSimpleLinearQn: QualifiedName = BuiltinEffects / "retainSimpleLinear"
   val TotalQn: QualifiedName = BuiltinEffects / "total"
   val DivQn: QualifiedName = BuiltinEffects / "div"
+  val NdetQn: QualifiedName = BuiltinEffects / "ndet"
   val MaybeDivQn: QualifiedName = BuiltinEffects / "mdiv"
 
   val BuiltinLevel: QualifiedName = Builtin / "level"
@@ -134,9 +135,8 @@ object Builtins:
       throw new IllegalArgumentException(s"Conflicting definitions: $conflictingDefs")
     elaborateAll(builtins)(using Context.empty)(using SimpleSignature())
 
-  import CTerm.*
-  import PreDeclaration.*
-  import Usage.*
+import CTerm.*
+import PreDeclaration.* import Usage.*
   import VTerm.*
 
   private def binding(name: Name, ty: VTerm, usage: VTerm = uAny): Binding[CTerm] =

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

@@ -284,7 +284,7 @@ def checkIsConvertible
               op2 @ OperationCall(effInstance2, name2, args2),
             ) if name1 == name2 =>
             val effConstraint = checkIsConvertible(effInstance1, effInstance2, Some(EffectsType()))
-            val (qn, tArgs) = inferType(effInstance1)._1 match
+            val (qn, tArgs) = inferType(effInstance1)._2 match
               case EffectInstanceType(eff, _) => eff
               case _                          => throw ComplexOperationCall(op2)
             val operation = Σ.getOperation(qn, name1)

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

@@ -49,7 +49,6 @@ enum IrError(val Γ: Context, e: Throwable | Null = null) extends Exception(e):
   case MissingDefinition(qn: QualifiedName) extends IrError(Context.empty)
   case MissingField(name: Name, qn: QualifiedName) extends IrError(Context.empty)
   case MissingFieldsInCoPattern(clause: PreClause)(using Γ: Context) extends IrError(Γ)
-  case MissingOperation(name: Name, qn: QualifiedName) extends IrError(Context.empty)
   case MissingUserCoPattern(clause: PreClause)(using Γ: Context) extends IrError(Γ)
   case NonEmptyType(ty: VTerm, source: PreClause)(using Γ: Context) extends IrError(Γ)
   case NotCConvertible(sub: CTerm, sup: CTerm, ty: Option[CTerm])(using Γ: Context)
@@ -60,12 +59,6 @@ enum IrError(val Γ: Context, e: Throwable | Null = null) extends Exception(e):
   case NotDataTypeType(tm: CTerm)(using Γ: Context) extends IrError(Γ)
   case NotLevelType(tm: VTerm)(using Γ: Context) extends IrError(Γ)
   case NotEffectSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ)
-  case NotEqDecidabilitySubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ)
-  case NotHandlerTypeSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ)
-  case NotEqDecidableDueToConstructor
-    (qn: QualifiedName, conName: Name, badComponentIndex: Nat)
-    (using Γ: Context) extends IrError(Γ)
-  case NotEqDecidableType(ty: VTerm)(using Γ: Context) extends IrError(Γ)
   case NotLevelSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ)
   case NotTypeError(tm: VTerm)(using Γ: Context) extends IrError(Γ)
   case NotUsageSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ)
@@ -94,13 +87,11 @@ enum IrError(val Γ: Context, e: Throwable | Null = null) extends Exception(e):
     (using Γ: Context) extends IrError(Γ, cause)
   case DataLevelCannotDependOnIndexArgument(preData: PreDeclaration.PreData)(using Γ: Context)
     extends IrError(Γ)
-  case DataEqDecidabilityCannotDependOnIndexArgument
-    (preData: PreDeclaration.PreData)
-    (using Γ: Context) extends IrError(Γ)
   case DuplicatedDeclaration(qn: QualifiedName) extends IrError(Context.empty)
   case UnableToFindUsageMeetDuringUnification(lowerBounds: Set[VTerm])(using Γ: Context)
     extends IrError(Γ)
   case InternalIrError(message: String)(using Γ: Context) extends IrError(Γ)
   case ComplexOperationCall(call: CTerm.OperationCall)(using Γ: Context) extends IrError(Γ)
   case ExpectEffectInstance(badEffInstance: VTerm)(using Γ: Context) extends IrError(Γ)
+  case ExpectEffectInstanceTypeSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ)
   override def getMessage: String = verbosePPrinter.apply(this).plainText

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

@@ -557,9 +557,9 @@ extension (v: VTerm)
                 operands.map((k, v) => dfs(k.normalized, retainSimpleLinearOnly || v)).toSeq
               val newLiterals = (literalsAndOperands.flatMap { case (l, _) => l } ++ literal)
                 .filter(effInstance =>
-                  val (qn, args) = inferType(effInstance)._1 match
+                  val (qn, args) = inferType(effInstance)._2 match
                     case EffectInstanceType(eff, _) => eff
-                    case _                          => throw IllegalStateException("bad type")
+                    case t                          => throw IllegalStateException(s"Expect EffectInstanceType but got $t")
                   if retainSimpleLinearOnly then {
                     val effect = Σ.getEffect(qn)
                     effect.continuationUsage
@@ -634,9 +634,9 @@ given Reducible[CTerm] with
     (using signature: Signature)
     (using TypingContext)
     : CTerm =
-    // TODO[P0]: if the reduced term contains `Continuation` or `HandlerKey`, then throw away the
-    //  reduced term and simply return t as it is. This is needed because `Continuation` is too hard
-    //  to be lowered.
+    // TODO[P1]: if the reduced term contains `Continuation` or `EffectInstance`, then throw away
+    //  the reduced term and simply return t as it is. This is needed because `Continuation` is too
+    //  hard to be lowered.
     StackMachine(mutable.ArrayBuffer()).run(t).withSourceInfo(t.sourceInfo)
 
 object Reducible:

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

@@ -6,7 +6,6 @@ import com.github.tgeng.archon.common.WrapPolicy.*
 import com.github.tgeng.archon.core.common.*
 import com.github.tgeng.archon.core.ir.CTerm.*
 import com.github.tgeng.archon.core.ir.Declaration.*
-import com.github.tgeng.archon.core.ir.HandlerType.{Complex, Simple}
 import com.github.tgeng.archon.core.ir.IrError.*
 import com.github.tgeng.archon.core.ir.PrettyPrinter.pprint
 import com.github.tgeng.archon.core.ir.ResolvedMetaVariable.*
@@ -28,7 +27,6 @@ def checkIsSubtype
   (using ctx: TypingContext)
   : Set[Constraint] = debugSubsumption("checkIsSubtype", sub, sup):
   check2(sub, sup):
-    // TODO[P0]: add logic for EffectInstanceType
     case (sub, sup) if sub == sup => Set.empty
     case (sub: VTerm, u @ RUnsolved(_, _, constraint, _, _)) =>
       ctx.adaptForMetaVariable(u, sub):
@@ -96,6 +94,13 @@ def checkIsSubtype
         case _                => throw NotVSubtype(sub, sup)
     case (LevelType(ub1), LevelType(ub2)) =>
       if ub1 <= ub2 then Set.empty else throw NotVSubtype(sub, sup)
+    case (
+        EffectInstanceType((qn1, args1), handlerConstraint1),
+        EffectInstanceType((qn2, args2), handlerConstraint2),
+      ) =>
+      if handlerConstraint1 > handlerConstraint2 || qn1 != qn2 then
+        throw ExpectEffectInstanceTypeSubsumption(sub, sup)
+      else checkAreConvertible(args1, args2, Σ.getEffect(qn1).context.toList)
     case _ => checkIsConvertible(sub, sup, None)
 
 /** Preconditions: sub and sup are both types

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

@@ -327,14 +327,12 @@ enum VTerm(val sourceInfo: SourceInfo) extends SourceInfoOwner[VTerm]:
     (literal: LevelOrder, maxOperands: SeqMap[VTerm, /* level offset */ Nat])
     (using sourceInfo: SourceInfo) extends VTerm(sourceInfo)
 
-  // TODO[P0]: rename to EffectInstanceType
   case EffectInstanceType
-    (effect: Eff, handlerConstraint: HandlerConstraint)
+    (eff: Eff, handlerConstraint: HandlerConstraint)
     (using sourceInfo: SourceInfo) extends VTerm(sourceInfo)
 
-  // TODO[P0]: rename to EffectInstance
   case EffectInstance
-    (effect: Eff, handlerConstraint: HandlerConstraint, handlerKey: HandlerKey = HandlerKey())
+    (eff: Eff, handlerConstraint: HandlerConstraint, handlerKey: HandlerKey = HandlerKey())
     extends VTerm(SourceInfo.SiEmpty)
 
   /** Automatically derived term, aka, `_` in Agda-like languages. During type checking, this is
@@ -455,7 +453,9 @@ object VTerm:
   val uAny: VTerm = VTerm.UsageLiteral(Usage.UAny)
   val div: EffectInstance =
     EffectInstance((Builtins.DivQn, Nil), HandlerConstraint(Usage.U0, HandlerType.Simple))
-  val globalKeys: Set[EffectInstance] = Set(div)
+  val ndet: EffectInstance =
+    EffectInstance((Builtins.NdetQn, Nil), HandlerConstraint(Usage.U1, HandlerType.Simple))
+  val globalKeys: Set[EffectInstance] = Set(div, ndet)
 
   /** Marker of a computation that surely diverges. Computation with this effect will not be
     * executed by the type checker.

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

@@ -179,7 +179,9 @@ def inferType
     case EffectInstanceType(eff, handlerConstraint) =>
       val newTm = EffectInstanceType(checkEff(eff), handlerConstraint)
       (newTm, Type(newTm))
-    case EffectInstance(_, _, _) => ???
+    case t @ EffectInstance(eff, handlerConstraint, _) =>
+      // There is no need to check eff because EffectInstance is only created by reduction.
+      (t, EffectInstanceType(eff, handlerConstraint))
     case LevelType(strictUpperBound) =>
       (LevelType(strictUpperBound), Type(LevelType(strictUpperBound)))
     case Level(literal, maxOperands) =>
@@ -440,7 +442,7 @@ def inferType
             val args = checkTypes(uncheckedArgs, record.context.map(_._1).toList)
             (RecordType(qn, args, effects), CType(tm, Total()))
       case OperationCall(effInstance, name, uncheckedArgs) =>
-        val (qn, uncheckedTArgs) = inferType(effInstance)._1 match
+        val (qn, uncheckedTArgs) = inferType(effInstance)._2 match
           case EffectInstanceType(eff, _) => eff
           case _ =>
             throw IllegalStateException(
@@ -511,6 +513,7 @@ def checkType
   (using Σ: Signature)
   (using ctx: TypingContext)
   : CTerm = debugCheckType(tm, ty):
+  // TODO[P0]: using something of effect instance type but not as an effect instance should yield ndet effect.
   tm match
     case Force(v) =>
       val checkedV = checkType(v, U(ty))
@@ -943,7 +946,7 @@ private def getEffectsContinuationUsage
   val usage = ctx.withMetaResolved(effects.normalized):
     case Effects(effectInstances, operands) =>
       val literalUsages = effectInstances.map { effectInstance =>
-        inferType(effectInstance)._1 match
+        inferType(effectInstance)._2 match
           case EffectInstanceType(_, handlerConstraint) =>
             UsageLiteral(handlerConstraint.continuationUsage)
           case _ => throw IllegalStateException("type error")

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

@@ -194,7 +194,7 @@ def collectUsages
         collectArgsUsages(args, record.context.map(_._1).toList) +
           collectUsages(effects, Some(EffectsType()))
       case OperationCall(effectInstance, name, args) =>
-        val (qn, tArgs) = inferType(effectInstance)._1 match
+        val (qn, tArgs) = inferType(effectInstance)._2 match
           case EffectInstanceType(eff, _) => eff
           case _ =>
             throw IllegalStateException(

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

@@ -121,10 +121,10 @@ trait TermVisitor[C, R]:
     (using ctx: C)
     (using Σ: Signature)
     : R =
-    visitEff(instanceType.effect)
+    visitEff(instanceType.eff)
 
   def visitEffectInstance(instance: VTerm.EffectInstance)(using ctx: C)(using Σ: Signature): R =
-    visitEff(instance.effect)
+    visitEff(instance.eff)
 
   def visitAuto(auto: Auto)(using ctx: C)(using Σ: Signature): R = combine()
 
@@ -655,13 +655,13 @@ trait Transformer[C]:
     (using Σ: Signature)
     : VTerm =
     EffectInstanceType(
-      transformEff(instanceType.effect),
+      transformEff(instanceType.eff),
       instanceType.handlerConstraint,
     )
 
   def transformEffectInstance(instance: EffectInstance)(using ctx: C)(using Σ: Signature): VTerm =
     EffectInstance(
-      transformEff(instance.effect),
+      transformEff(instance.eff),
       instance.handlerConstraint,
       instance.handlerKey,
     )

src/test/resources/com/github/tgeng/archon/core/ir/testing/tterm/t_declaration_spec/record_stream/translation_output.scala

@@ -48,7 +48,7 @@ List(
             bodyTy = RecordType(
               qn = qn"test.CStream",
               args = List(),
-              effects = Effects(literal = Set(), unionOperands = SeqMap()) @ "ε"
+              effects = Effects(handlerKeys = Set(), unionOperands = SeqMap()) @ "ε"
             ) @ "CStream",
             effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total") @ "ε") @ "ε"
           ) @ "Eq Nat m (head self) -> CStream",