diff --git a/syntax/jvm/src/main/scala/chester/syntax/core/truffle.scala b/syntax/jvm/src/main/scala/chester/syntax/core/truffle.scala
index 1bbc5f93..70e22e04 100644
--- a/syntax/jvm/src/main/scala/chester/syntax/core/truffle.scala
+++ b/syntax/jvm/src/main/scala/chester/syntax/core/truffle.scala
@@ -17,7 +17,7 @@ import scala.collection.immutable.{ArraySeq, HashMap}
 object truffle {
   type ExecuteGeneric = (VirtualFrame, Term) => Object
   val globalExecuteGeneric: Parameter[ExecuteGeneric] = new Parameter[ExecuteGeneric]
-  given rw: ReadWriter[Term] = implicitly[ReadWriter[simple.Term]].bimap(convertToTruffle, convertToSimple)
+  given rw: ReadWriter[Term] = implicitly[ReadWriter[simple.Term]].bimap(convertToSimple, convertToTruffle)
   given rw1: ReadWriter[ReferenceCall] = rw.asInstanceOf[ReadWriter[ReferenceCall]]
   given rw2: ReadWriter[Effects] = rw.asInstanceOf[ReadWriter[Effects]]
   given rw3: ReadWriter[BlockTerm] = rw.asInstanceOf[ReadWriter[BlockTerm]]
@@ -58,7 +58,7 @@ object truffle {
   ) extends WHNF
       with FCallTermC[Term] {
     override type ThisTree = FCallTerm
-    override def cons: FCallTermF[Term, ThisTree] = this.copy
+    override def cons: FCallTermF[Term, ThisTree] = FCallTerm(_, _, _)
   }
   sealed abstract class Pat extends SpecialTerm with PatT[Term]  {
     override type ThisTree <: Pat
@@ -70,7 +70,7 @@ object truffle {
   ) extends Pat
       with BindC[Term] {
     override type ThisTree = Bind
-    override def cons: BindF[Term, ThisTree] = this.copy
+    override def cons: BindF[Term, ThisTree] = Bind(_,_,_)
   }
   sealed trait WHNF extends Term with WHNFT[Term]  {
     override type ThisTree <: WHNF
@@ -216,7 +216,7 @@ object truffle {
   ) extends TypeTerm
       with LiteralTypeC[Term] {
     override type ThisTree = LiteralType
-    override def cons: LiteralTypeF[Term, ThisTree] = this.copy
+    override def cons: LiteralTypeF[Term, ThisTree] = LiteralType(_,_)
   }
   case class ArgTerm(
       @child var bind: LocalV,
@@ -236,7 +236,7 @@ object truffle {
   ) extends WHNF
       with TelescopeTermC[Term] {
     override type ThisTree = TelescopeTerm
-    override def cons: TelescopeTermF[Term, ThisTree] = this.copy
+    override def cons: TelescopeTermF[Term, ThisTree] = TelescopeTerm(_,_,_)
   }
   case class Function(
       @child var ty: FunctionType,
@@ -245,7 +245,7 @@ object truffle {
   ) extends WHNF
       with FunctionC[Term] {
     override type ThisTree = Function
-    override def cons: FunctionF[Term, ThisTree] = this.copy
+    override def cons: FunctionF[Term, ThisTree] = Function(_,_,_)
   }
   case class FunctionType(
       @const telescope: Vector[TelescopeTerm],
@@ -272,7 +272,7 @@ object truffle {
   ) extends WHNF
       with ObjectTermC[Term] {
     override type ThisTree = ObjectTerm
-    override def cons: ObjectTermF[Term, ThisTree] = this.copy
+    override def cons: ObjectTermF[Term, ThisTree] = ObjectTerm(_,_)
   }
   case class ObjectType(
       @const fieldTypes: Vector[ObjectClauseValueTerm],
@@ -395,7 +395,7 @@ object truffle {
   ) extends Uneval
       with BlockTermC[Term]  {
     override type ThisTree = BlockTerm
-    override def cons: BlockTermF[Term, ThisTree] = this.copy
+    override def cons: BlockTermF[Term, ThisTree] = BlockTerm(_,_,_)
   }
   case class Annotation(
       @child var term: Term,
diff --git a/syntax/shared/src/main/scala/chester/syntax/Tree.scala b/syntax/shared/src/main/scala/chester/syntax/Tree.scala
index 671efb84..70d645ad 100644
--- a/syntax/shared/src/main/scala/chester/syntax/Tree.scala
+++ b/syntax/shared/src/main/scala/chester/syntax/Tree.scala
@@ -68,7 +68,4 @@ trait TreeMap[Tre <: Tree[Tre]] {
   final def apply[T <: Tre](x: T): T = use(x).asInstanceOf[T]
 }
 
-implicit def convertSpecialMap2[A <: Tree[A], T <: A](f: TreeMap[A]): Tree[A] => T = x => f.use(x.asInstanceOf[T]).asInstanceOf[T]
-implicit def conversion1[A <: Tree[A], T <: Tree[A], U <: T](x: Vector[T]): Vector[U] = x.asInstanceOf[Vector[U]]
-implicit def conversion11[A <: Tree[A], T <: Tree[A], U <: T](x: T): U = x.asInstanceOf[U]
-//implicit  def conversion2[A <: Tree[A], T <: Tree[A]](x:T): A&T = x.asInstanceOf[A&T]
+implicit def convertSpecialMap2[A <: Tree[A], T <: A](f: TreeMap[A]): Tree[A] => T = x => f.use(x.asInstanceOf[T]).asInstanceOf[T]
\ No newline at end of file
diff --git a/syntax/shared/src/main/scala/chester/syntax/core/simple.scala b/syntax/shared/src/main/scala/chester/syntax/core/simple.scala
index 41f09ae7..76bbef96 100644
--- a/syntax/shared/src/main/scala/chester/syntax/core/simple.scala
+++ b/syntax/shared/src/main/scala/chester/syntax/core/simple.scala
@@ -240,7 +240,7 @@ object simple {
   ) extends WHNF
       with FunctionTypeC[Term] {
     override type ThisTree = FunctionType
-    override def cons: FunctionTypeF[Term, ThisTree] = this.copy
+    override def cons: FunctionTypeF[Term, ThisTree] = FunctionType(_,_,_,_)
   }
   case class ObjectClauseValueTerm(
       key: Term,
diff --git a/syntax/shared/src/main/scala/chester/syntax/core/spec/Term.scala b/syntax/shared/src/main/scala/chester/syntax/core/spec/Term.scala
index 04ba30d9..0a0995ed 100644
--- a/syntax/shared/src/main/scala/chester/syntax/core/spec/Term.scala
+++ b/syntax/shared/src/main/scala/chester/syntax/core/spec/Term.scala
@@ -47,6 +47,9 @@ object spec {
   trait CallingArgTermF[Term <: TermT[Term], ThisTree <: CallingArgTermC[Term]] {
     def newCallingArgTerm(value: Term, ty: Term, name: Option[Name], vararg: Boolean, meta: OptionTermMeta): ThisTree
   }
+  
+  implicit def convertArg[Term <: TermT[Term],CallingArgTerm <: CallingArgTermC[Term] ](x: CallingArgTermC[Term] ): CallingArgTerm = x.asInstanceOf[CallingArgTerm]
+  implicit def convertArg[Term <: TermT[Term],CallingArgTerm <: CallingArgTermC[Term] ](x: Seq[CallingArgTermC[Term]] ): Seq[CallingArgTerm] = x.asInstanceOf[Seq[CallingArgTerm] ]
 
   trait CallingArgTermC[Term <: TermT[Term]] extends WHNFT[Term] {
     override type ThisTree <: CallingArgTermC[Term]
@@ -86,7 +89,7 @@ object spec {
     def newCalling(args: Seq[CallingArgTermC[Term]], implicitly: Boolean, meta: OptionTermMeta): ThisTree
   }
   
-  implicit inline def convertaaa[Term <: TermT[Term], ThisTree <: CallingC[Term]](x: Seq[CallingArgTermC[Term]]): Seq[ThisTree] = x.asInstanceOf[Seq[ThisTree]]
+  implicit inline def convertbbb[Term <: TermT[Term], ThisTree <: CallingC[Term]](x: Vector[CallingC[Term]]): Vector[ThisTree] = x.asInstanceOf[Vector[ThisTree]]
 
   trait CallingC[Term <: TermT[Term]] extends WHNFT[Term] {
     override type ThisTree <: CallingC[Term]
@@ -167,6 +170,8 @@ object spec {
     override def descent(f: Term => Term, g: TreeMap[Term]): Term = thisOr(cpy(bind = g(bind), ty = f(ty)))
   }
 
+  implicit def convert [Term <: TermT[Term]](x: TermT[Term]): Term = x.asInstanceOf[Term]
+
   /** more abstract Term. sealed trait *T corresponds to sealed trait in Term; trait *C corresponds to case class in Term */
   trait TermT[Term <: TermT[Term]] extends Any with ToDoc with WithPos with ContainsUniqid with Tree[Term] {
     override type ThisTree <: TermT[Term]
@@ -278,6 +283,8 @@ object spec {
     override type ThisTree <: EffectsMT[Term]
   }
 
+  implicit def convertEffectsM[Term <: TermT[Term], EffectsM <: EffectsMT[Term]](x: EffectsMT[Term]): EffectsM = x.asInstanceOf[EffectsM]
+
   trait MetaTermC[Term <: TermT[Term]] extends TermT[Term] with EffectsMT[Term] with SpecialTermT[Term] {
     override type ThisTree <: MetaTermC[Term]
 
@@ -448,6 +455,8 @@ object spec {
     override type ThisTree <: LiteralTermT[Term]
   }
 
+  implicit def conveL[Term <: TermT[Term], LiteralTerm <: LiteralTermT[Term]](x: LiteralTermT[Term]): LiteralTerm = x.asInstanceOf[LiteralTerm]
+
   trait AbstractIntTermT[Term <: TermT[Term]] extends LiteralTermT[Term] {
     override type ThisTree <: AbstractIntTermT[Term]
   }
@@ -778,6 +787,10 @@ object spec {
     def newArgTerm(bind: LocalVC[Term], ty: Term, default: Option[Term], vararg: Boolean, meta: OptionTermMeta): ThisTree
   }
 
+  implicit def convertA[Term <: TermT[Term], ArgTerm <: ArgTermC[Term]](x: ArgTermC[Term]): ArgTerm = x.asInstanceOf[ArgTerm]
+
+  implicit def convertA[Term <: TermT[Term], ArgTerm <: ArgTermC[Term]](x: Vector[ArgTermC[Term]]): Vector[ArgTerm] = x.asInstanceOf[Vector[ArgTerm]]
+
   trait ArgTermC[Term <: TermT[Term]] extends WHNFT[Term] {
     override type ThisTree <: ArgTermC[Term]
 
@@ -813,6 +826,9 @@ object spec {
     def name = bind.name
   }
 
+  implicit def convertTelescopeTerm[Term <: TermT[Term], TelescopeTerm <: TelescopeTermC[Term]](x: TelescopeTermC[Term]): TelescopeTerm = x.asInstanceOf[TelescopeTerm]
+  implicit def convertTelescopeTermVec[Term <: TermT[Term], TelescopeTerm <: TelescopeTermC[Term]](x: Vector[TelescopeTermC[Term]]): Vector[TelescopeTerm] = x.asInstanceOf[Vector[TelescopeTerm]]
+
   trait TelescopeTermC[Term <: TermT[Term]] extends WHNFT[Term] {
     override type ThisTree <: TelescopeTermC[Term]
 
@@ -884,6 +900,8 @@ object spec {
     ): ThisTree
   }
 
+  implicit def convertFunctionTypeC[Term <: TermT[Term], FunctionType <: FunctionTypeC[Term]](x: FunctionTypeC[Term]): FunctionType = x.asInstanceOf[FunctionType]
+
   trait FunctionTypeC[Term <: TermT[Term]] extends WHNFT[Term] {
     override type ThisTree <: FunctionTypeC[Term]
 
@@ -927,6 +945,9 @@ object spec {
     def newObjectClauseValueTerm(key: Term, value: Term, meta: OptionTermMeta): ThisTree
   }
 
+  implicit def convertObjectClauseValueTermC[Term <: TermT[Term], ObjectClauseValueTerm <: ObjectClauseValueTermC[Term]](x: ObjectClauseValueTermC[Term]): ObjectClauseValueTerm = x.asInstanceOf[ObjectClauseValueTerm]
+  implicit def convertObjectClauseValueTermCB[Term <: TermT[Term], ObjectClauseValueTerm <: ObjectClauseValueTermC[Term]](x: Vector[ObjectClauseValueTermC[Term]]): Vector[ObjectClauseValueTerm] = x.asInstanceOf[Vector[ObjectClauseValueTerm]]
+
   trait ObjectClauseValueTermC[Term <: TermT[Term]] extends WHNFT[Term] {
     override type ThisTree <: ObjectClauseValueTermC[Term]
 
@@ -1174,6 +1195,8 @@ object spec {
   implicit def conversionTop[Term <: TermT[Term], ToplevelV <: ToplevelVC[Term]](x: UniqidOf[ToplevelVC[Term]]): UniqidOf[ToplevelV] =
     x.asInstanceOf[UniqidOf[ToplevelV]]
 
+  implicit def converLocalV[Term <: TermT[Term], LocalV <: LocalVC[Term]](x: LocalVC[Term]): LocalV =
+    x.asInstanceOf[LocalV]
   trait LocalVC[Term <: TermT[Term]] extends ReferenceCallC[Term] {
     override type ThisTree <: LocalVC[Term]
 
@@ -1239,6 +1262,9 @@ object spec {
     override type ThisTree <: StmtTermT[Term]
   }
 
+  implicit def convertStmtTermT[Term <: TermT[Term], StmtTerm <: StmtTermT[Term]](x: StmtTermT[Term]): StmtTerm = x.asInstanceOf[StmtTerm]
+  implicit def convertStmtTermT2[Term <: TermT[Term], StmtTerm <: StmtTermT[Term]](x: Vector[StmtTermT[Term]]): Vector[StmtTerm] = x.asInstanceOf[Vector[StmtTerm]]
+
   @FunctionalInterface
   trait LetStmtTermF[Term <: TermT[Term], ThisTree <: LetStmtTermC[Term]] {
     def newLetStmt(localv: LocalVC[Term], value: Term, ty: Term, meta: OptionTermMeta): ThisTree
@@ -1464,6 +1490,10 @@ object spec {
     )
   }
 
+
+  implicit def convertFieldTerm[Term <: TermT[Term], FieldTerm <: FieldTermC[Term]](x: FieldTermC[Term]): FieldTerm = x.asInstanceOf[FieldTerm]
+  implicit def convertFieldTermVec[Term <: TermT[Term], FieldTerm <: FieldTermC[Term]](x: Vector[FieldTermC[Term]]): Vector[FieldTerm] = x.asInstanceOf[Vector[FieldTerm]]
+
   trait FieldTermC[Term <: TermT[Term]] extends WHNFT[Term] {
     override type ThisTree <: FieldTermC[Term]
 
diff --git a/tyck-base/src/main/scala/chester/tyck/ElaboraterCommon.scala b/tyck-base/src/main/scala/chester/tyck/ElaboraterCommon.scala
index 5806051d..e97ac230 100644
--- a/tyck-base/src/main/scala/chester/tyck/ElaboraterCommon.scala
+++ b/tyck-base/src/main/scala/chester/tyck/ElaboraterCommon.scala
@@ -42,7 +42,7 @@ trait ElaboraterCommon extends ProvideCtx with ElaboraterBase with CommonPropaga
       with NoFill[Effects] {
     override def add(key: LocalV, value: Term): DynamicEffectsCell = {
       require(!effects.contains(key))
-      copy(effects = effects + (key -> value))
+      copy(effects = effects.updated(key, value))
     }
 
     override def readUnstable: Option[Effects] = Some(Effects(effects, None))