diff --git a/README.md b/README.md
index d59ddfa..28813ce 100644
--- a/README.md
+++ b/README.md
@@ -4,7 +4,7 @@ A ***D**efinitional* ***C**ompiler* for generating Scala code.
  - Generates code for Scala 3
 
 ```scala
-"com.julianpeeters" %% "dc10-scala" % "0.5.0"
+"com.julianpeeters" %% "dc10-scala" % "0.6.0"
 ```
 
 ### `dc10-scala`
@@ -21,7 +21,7 @@ val snippet =
     s <- VAL("str", STRING, "hello, world")
     _ <- VAL("msg", STRING, s)
   yield ()
-// snippet: IndexedStateT[ErrorF, List[Statement], List[Statement], Unit] = cats.data.IndexedStateT@71417d5f
+// snippet: IndexedStateT[ErrorF, List[Statement], List[Statement], Unit] = cats.data.IndexedStateT@6f7d85d7
 ```
 
 Use the `compiler` impl to check and render code `toString` or `toVirtualFile`:
diff --git a/src/main/scala/dc10/scala/Statement.scala b/src/main/scala/dc10/scala/Statement.scala
index c433151..17decbe 100644
--- a/src/main/scala/dc10/scala/Statement.scala
+++ b/src/main/scala/dc10/scala/Statement.scala
@@ -135,19 +135,19 @@ object Statement:
       def indent: Int = i
       def sp: SourcePos = s
       def tpe: Term.TypeLevel.App.App1[T, A, X, Y, Z]
-      def rhs: NonEmptyList[Term.TypeLevel.App.App2[?, ?, ?, Nothing, ?]]
+      def rhs: NonEmptyList[Term.TypeLevel.App.Infix[?, ?, ?, ?, ?, ?, ?]]
 
     object Match:
       def apply[T[_], A, B, X, Y, Z](
         i: Int,
         t: Term.TypeLevel.App.App1[T, A, X, Y, Z],
-        f: NonEmptyList[Term.TypeLevel.App.App2[?, ?, ?, Nothing, ?]]
+        f: NonEmptyList[Term.TypeLevel.App.Infix[?, ?, ?, ?, ?, ?, ?]]
       )(
         using sp: SourcePos
       ): TypeDef =
         new Match[T, A, B, X, Y, Z](i, sp):
           def tpe: Term.TypeLevel.App.App1[T, A, X, Y, Z] = t
-          def rhs: NonEmptyList[Term.TypeLevel.App.App2[?, ?, ?, Nothing, ?]] = f
+          def rhs: NonEmptyList[Term.TypeLevel.App.Infix[?, ?, ?, ?, ?, ?, ?]] = f
 
   sealed trait ValueDef extends Statement:
     type Tpe
diff --git a/src/main/scala/dc10/scala/Symbol.scala b/src/main/scala/dc10/scala/Symbol.scala
index 085174b..d03be69 100644
--- a/src/main/scala/dc10/scala/Symbol.scala
+++ b/src/main/scala/dc10/scala/Symbol.scala
@@ -88,6 +88,7 @@ object Symbol:
             case Symbol.Term.TypeLevel.App.App1(qnt, tfun, targ, dep) => dep 
             case Symbol.Term.TypeLevel.App.App2(qnt, tfun, ta, tb, dep) => dep
             case Symbol.Term.TypeLevel.App.App3(qnt, tfun, ta1, ta2, tb, dep) => dep
+            case Symbol.Term.TypeLevel.App.Infix(qnt, tfun, ta, tb, dep) => dep
             case Symbol.Term.TypeLevel.Lam.Function1Type(qnt, dep) => dep
             case Symbol.Term.TypeLevel.Lam.Function2Type(qnt, dep) => dep
             case Symbol.Term.TypeLevel.Var.BooleanType(qnt, dep) => dep
@@ -101,8 +102,9 @@ object Symbol:
       sealed trait App[T, Z] extends TypeLevel[T, Z]
       object App:
         case class App1[T[_], A, X, Y, Z](qnt: Option[Long], tfun: TypeLevel[T[A], X], targ: TypeLevel[A, Y], dep: Z) extends App[T[A], Z]
-        case class App2[T[_,_], A, B, X, Z](qnt: Option[Long], tfun: TypeLevel[T[A, B], Z], ta: TypeLevel[A, Z], tb: TypeLevel[B, Z], dep: Z) extends App[T[A, B], Z]
+        case class App2[T[_,_], A, B, W, X, Y, Z](qnt: Option[Long], tfun: TypeLevel[T[A, B], W], ta: TypeLevel[A, X], tb: TypeLevel[B, Y], dep: Z) extends App[T[A, B], Z]
         case class App3[T[_,_,_], A, B, C, X, Z](qnt: Option[Long], tfun: TypeLevel[T[A,B,C], Z], ta1: TypeLevel[A, Z], ta2: TypeLevel[B, Z], tb: TypeLevel[C, Z], dep: Z) extends App[T[A, B, C], Z]
+        case class Infix[T[_,_], A, B, W, X, Y, Z](qnt: Option[Long], tfun: TypeLevel[T[A, B], W], ta: TypeLevel[A, X], tb: TypeLevel[B, Y], dep: Z) extends App[T[A, B], Z]
       sealed trait Lam[T, Z] extends TypeLevel[T, Z]
       object Lam:
         case class Function1Type[A, B, Z](qnt: Option[Long], dep: Z) extends Lam[A => B, Z]
@@ -151,7 +153,7 @@ object Symbol:
         case class Dotless[A, B, C, D, Z](qnt: Option[Long], fun: ValueLevel[D, Z], arg1: ValueLevel[A, Z], arg2: ValueLevel[B, Z], tpe: TypeLevel[C, Z]) extends Term.ValueLevel.App[C, Z]
       sealed abstract class Lam[T, Z] extends Term.ValueLevel[T, Z]
       object Lam:
-        case class Lam1[A, B, Z](qnt: Option[Long], a: ValueLevel[A, Z], b: ValueLevel[B, Z], tpe: TypeLevel[A => B, Z]) extends Term.ValueLevel.Lam[A => B, Z]
+        case class Lam1[A, B, X, Y, Z](qnt: Option[Long], a: ValueLevel[A, X], b: ValueLevel[B, Y], tpe: TypeLevel[A => B, Z]) extends Term.ValueLevel.Lam[A => B, Z]
         case class Lam2[A, B, C, Z](qnt: Option[Long], a1: ValueLevel[A, Z], a2: ValueLevel[B, Z], c: ValueLevel[C, Z], tpe: TypeLevel[(A, B) => C, Z]) extends Term.ValueLevel.Lam[(A, B) => C, Z]
       sealed abstract class Var[T, Z] extends Term.ValueLevel[T, Z]
       object Var:
@@ -162,4 +164,80 @@ object Symbol:
         case class OptionCtor[A, Z](qnt: Option[Long], tpe: TypeLevel[A, Z]) extends Var[A, Z]
         case class SomeCtor[A, Z](qnt: Option[Long], tpe: TypeLevel[A, Z]) extends Var[A, Z]
         case class UserDefinedValue[T, Z](qnt: Option[Long], nme: String, tpe: TypeLevel[T, Z], impl: Option[ValueLevel[T, Z]]) extends Var[T, Z]
-              
\ No newline at end of file
+
+    
+    extension [T, Z] (t: Term.TypeLevel[T, Z])
+      def manageDep[ZZ](f: Z => ZZ): Term.TypeLevel[T, ZZ] =
+        t match
+          case Term.TypeLevel.App.App1(qnt, tfun, targ, dep) =>  Term.TypeLevel.App.App1(qnt, tfun, targ, f(dep)) 
+          case Term.TypeLevel.App.App2(qnt, tfun, ta, tb, dep) => Term.TypeLevel.App.App2(qnt, tfun, ta, tb, f(dep))
+          case Term.TypeLevel.App.App3(qnt, tfun, ta1, ta2, tb, dep) => Term.TypeLevel.App.App3(qnt, tfun.manageDep(f), ta1.manageDep(f), ta2.manageDep(f), tb.manageDep(f), f(dep))
+          case Term.TypeLevel.App.Infix(qnt, tfun, ta, tb, dep) => Term.TypeLevel.App.App2(qnt, tfun, ta, tb, f(dep))
+          case Term.TypeLevel.Lam.Function1Type(qnt, dep) => Term.TypeLevel.Lam.Function1Type(qnt, f(dep)).asInstanceOf[Term.TypeLevel[T, ZZ]]
+          case Term.TypeLevel.Lam.Function2Type(qnt, dep) => Term.TypeLevel.Lam.Function2Type(qnt, f(dep)).asInstanceOf[Term.TypeLevel[T, ZZ]]
+          case Term.TypeLevel.Var.BooleanType(qnt, dep) => Term.TypeLevel.Var.BooleanType(qnt, f(dep))
+          case Term.TypeLevel.Var.IntType(qnt, dep) => Term.TypeLevel.Var.IntType(qnt, f(dep))
+          case Term.TypeLevel.Var.StringType(qnt, dep) => Term.TypeLevel.Var.StringType(qnt, f(dep))
+          case Term.TypeLevel.Var.ListType(qnt, dep) => Term.TypeLevel.Var.ListType(qnt, f(dep))
+          case Term.TypeLevel.Var.OptionType(qnt, dep) => Term.TypeLevel.Var.OptionType(qnt, f(dep))
+          case Term.TypeLevel.Var.SomeType(qnt, dep) => Term.TypeLevel.Var.SomeType(qnt, f(dep))
+          case Term.TypeLevel.Var.UserDefinedType(qnt, nme, impl, dep) => Term.TypeLevel.Var.UserDefinedType(qnt, nme, impl.map(i => i.manageDep(f)), f(dep))
+
+    extension [T, Z] (v: Term.ValueLevel[T, Z])
+      def manageDep[ZZ](f: Z => ZZ): Term.ValueLevel[T, ZZ] =
+        v match
+          case Term.ValueLevel.App.App1(qnt, fun, arg, tpe) => Term.ValueLevel.App.App1(qnt, fun.manageDep(f), arg.manageDep(f), tpe.manageDep(f))
+          case Term.ValueLevel.App.AppCtor1(qnt, tpe, arg) => Term.ValueLevel.App.AppCtor1(qnt, tpe.manageDep(f), arg.manageDep(f))
+          case Term.ValueLevel.App.AppCtor2(qnt, tpe, arg1, arg2) => Term.ValueLevel.App.AppCtor2(qnt, tpe.manageDep(f), arg1.manageDep(f), arg2.manageDep(f))
+          case Term.ValueLevel.App.AppPure(qnt, fun, arg, tpe) => Term.ValueLevel.App.AppPure(qnt, fun, arg, tpe.manageDep(f))
+          case Term.ValueLevel.App.AppVargs(qnt, fun, tpe, vargs*) => ???
+          case Term.ValueLevel.App.Dot1(qnt, fun, arg1, arg2, tpe) => Term.ValueLevel.App.Dot1(qnt, fun.manageDep(f), arg1.manageDep(f), arg2.manageDep(f), tpe.manageDep(f))
+          case Term.ValueLevel.App.Dotless(qnt, fun, arg1, arg2, tpe) => Term.ValueLevel.App.Dotless(qnt, fun.manageDep(f), arg1.manageDep(f), arg2.manageDep(f), tpe.manageDep(f))
+          case Term.ValueLevel.Lam.Lam1(qnt, a, b, tpe) => Term.ValueLevel.Lam.Lam1(qnt, a, b, tpe.manageDep(f))
+          case Term.ValueLevel.Lam.Lam2(qnt, a1, a2, b, tpe) => ???
+          case Term.ValueLevel.Var.BooleanLiteral(qnt, tpe, b) => Term.ValueLevel.Var.BooleanLiteral(qnt, tpe.manageDep(f), b)
+          case Term.ValueLevel.Var.IntLiteral(qnt, tpe, i) => Term.ValueLevel.Var.IntLiteral(qnt, tpe.manageDep(f), i)
+          case Term.ValueLevel.Var.StringLiteral(qnt, tpe, s) => Term.ValueLevel.Var.StringLiteral(qnt, tpe.manageDep(f), s)
+          case Term.ValueLevel.Var.ListCtor(qnt, tpe) => Term.ValueLevel.Var.ListCtor(qnt, tpe.manageDep(f))
+          case Term.ValueLevel.Var.OptionCtor(qnt, tpe) => Term.ValueLevel.Var.OptionCtor(qnt, tpe.manageDep(f))
+          case Term.ValueLevel.Var.SomeCtor(qnt, tpe) => Term.ValueLevel.Var.SomeCtor(qnt, tpe.manageDep(f))
+          case Term.ValueLevel.Var.UserDefinedValue(qnt, nme, tpe, impl) => Term.ValueLevel.Var.UserDefinedValue(qnt, nme, tpe.manageDep(f), impl.map(i => i.manageDep(f)))
+
+      def findImpl: Option[Term.ValueLevel[T, Z]] =
+        v match
+          case Term.ValueLevel.App.App1(qnt, fun, arg, tpe) => Some(v)
+          case Term.ValueLevel.App.AppCtor1(qnt, tpe, arg) => Some(v)
+          case Term.ValueLevel.App.AppCtor2(qnt, tpe, arg1, arg2) => Some(v)
+          case Term.ValueLevel.App.AppPure(qnt, fun, arg, tpe) => Some(v)
+          case Term.ValueLevel.App.AppVargs(qnt, fun, tpe, vargs*) => Some(v)
+          case Term.ValueLevel.App.Dot1(qnt, fun, arg1, arg2, tpe) => Some(v)
+          case Term.ValueLevel.App.Dotless(qnt, fun, arg1, arg2, tpe) => Some(v)
+          case Term.ValueLevel.Lam.Lam1(qnt, a, b, t) => Some(v)
+          case Term.ValueLevel.Lam.Lam2(qnt, a1, a2, b, t) => Some(v)
+          case Term.ValueLevel.Var.BooleanLiteral(qnt, tpe, b) => Some(v)
+          case Term.ValueLevel.Var.IntLiteral(qnt, tpe, i) => Some(v)
+          case Term.ValueLevel.Var.StringLiteral(qnt, tpe, s) => Some(v)
+          case Term.ValueLevel.Var.ListCtor(qnt, tpe) => Some(v)
+          case Term.ValueLevel.Var.OptionCtor(qnt, tpe) => Some(v)
+          case Term.ValueLevel.Var.SomeCtor(qnt, tpe) => Some(v)
+          case u@Term.ValueLevel.Var.UserDefinedValue(qnt, nme, tpe, impl) => impl.fold(None)(i => i.findImpl)
+
+      def findVargs[U, A]: Option[Seq[Term.ValueLevel[U, A]]] =
+        v.findImpl.fold(None)(i => i match
+          case Term.ValueLevel.App.App1(qnt, fun, arg, tpe) => None
+          case Term.ValueLevel.App.AppCtor1(qnt, tpe, arg) => None
+          case Term.ValueLevel.App.AppCtor2(qnt, tpe, arg1, arg2) => None
+          case Term.ValueLevel.App.AppPure(qnt, fun, arg, tpe) => None
+          case Term.ValueLevel.App.AppVargs(qnt, fun, tpe, vargs*) => Some(vargs.asInstanceOf[Seq[Term.ValueLevel[U, A]]])
+          case Term.ValueLevel.App.Dot1(qnt, fun, arg1, arg2, tpe) => None
+          case Term.ValueLevel.App.Dotless(qnt, fun, arg1, arg2, tpe) => None
+          case Term.ValueLevel.Lam.Lam1(qnt, a, b, t) => None
+          case Term.ValueLevel.Lam.Lam2(qnt, a1, a2, b, t) => None
+          case Term.ValueLevel.Var.BooleanLiteral(qnt, tpe, b) => None
+          case Term.ValueLevel.Var.IntLiteral(qnt, tpe, i) => None
+          case Term.ValueLevel.Var.StringLiteral(qnt, tpe, s) => None
+          case Term.ValueLevel.Var.ListCtor(qnt, tpe) => None
+          case Term.ValueLevel.Var.OptionCtor(qnt, tpe) => None
+          case Term.ValueLevel.Var.SomeCtor(qnt, tpe) => None
+          case Term.ValueLevel.Var.UserDefinedValue(qnt, nme, tpe, impl) => None
+        )
diff --git a/src/main/scala/dc10/scala/predef/Applications.scala b/src/main/scala/dc10/scala/predef/Applications.scala
index a8d3733..bafc6bf 100644
--- a/src/main/scala/dc10/scala/predef/Applications.scala
+++ b/src/main/scala/dc10/scala/predef/Applications.scala
@@ -16,13 +16,13 @@ trait Applications[F[_]]:
     @scala.annotation.targetName("app1T")
     def apply[Z](args: F[TypeExpr[A, Z]]): F[TypeExpr[T[A], (Y, Z)]]
 
-  extension [T[_,_], A, B] (tfunction: F[TypeExpr[T[A, B], Unit]])
+  extension [T[_,_], A, B, X, Y, Z] (tfunction: F[TypeExpr[T[A, B], X]])
     @scala.annotation.targetName("app2T")
-    def apply(fta: F[TypeExpr[A, Unit]])(ftb: F[TypeExpr[B, Unit]]): F[TypeExpr[T[A, B], Unit]]
+    def apply(fta: F[TypeExpr[A, Y]], ftb: F[TypeExpr[B, Z]]): F[TypeExpr[T[A, B], (X, (Y, Z))]]
 
-  extension [A, B] (function: F[ValueExpr[A => B, Unit]])
+  extension [A, B, Y, Z] (function: F[ValueExpr[A => B, Y]])
     @scala.annotation.targetName("app1V")
-    def apply(args: F[ValueExpr[A, Unit]])(using sp: SourcePos): F[ValueExpr[B, Unit]]
+    def apply(args: F[ValueExpr[A, Y]])(using sp: SourcePos): F[ValueExpr[B, Y]]
 
   extension [A, B] (arg1: F[ValueExpr[A, Unit]] | ValueExpr[A, Unit])
     @scala.annotation.targetName("dot1V_fa|a")
@@ -44,25 +44,26 @@ object Applications:
           a <- targs
         yield TypeExpr(Term.TypeLevel.App.App1(None, f.tpe, a.tpe, (f.tpe.dep, a.tpe.dep)))
 
-    extension [T[_,_], A, B] (tfunction: StateT[ErrorF, List[Statement], TypeExpr[T[A, B], Unit]])
+    extension [T[_,_], A, B, X, Y, Z] (tfunction: StateT[ErrorF, List[Statement], TypeExpr[T[A, B], X]])
       @scala.annotation.targetName("app2T")
-      def apply(fta: StateT[ErrorF, List[Statement], TypeExpr[A, Unit]])(ftb: StateT[ErrorF, List[Statement], TypeExpr[B, Unit]]): StateT[ErrorF, List[Statement], TypeExpr[T[A, B], Unit]] =
+      def apply(fta: StateT[ErrorF, List[Statement], TypeExpr[A, Y]], ftb: StateT[ErrorF, List[Statement], TypeExpr[B, Z]]): StateT[ErrorF, List[Statement], TypeExpr[T[A, B], (X, (Y, Z))]] =
         for
           f <- tfunction
           a <- fta
           b <- ftb
-        yield TypeExpr(Term.TypeLevel.App.App2(None, f.tpe, a.tpe, b.tpe, ()))
+        yield TypeExpr(Term.TypeLevel.App.App2(None, f.tpe, a.tpe, b.tpe, (f.tpe.dep, (a.tpe.dep, b.tpe.dep))))
 
-    extension [A, B] (function: StateT[ErrorF, List[Statement], ValueExpr[A => B, Unit]])
+    extension [A, B, Y, Z] (function: StateT[ErrorF, List[Statement], ValueExpr[A => B, Y]])
       @scala.annotation.targetName("app1V")
-      def apply(args: StateT[ErrorF, List[Statement], ValueExpr[A, Unit]])(using sp: SourcePos): StateT[ErrorF, List[Statement], ValueExpr[B, Unit]] =
+      def apply(args: StateT[ErrorF, List[Statement], ValueExpr[A, Y]])(using sp: SourcePos): StateT[ErrorF, List[Statement], ValueExpr[B, Y]] =
         for
           f <- function
           a <- args
-          t <- StateT.liftF[ErrorF, List[Statement], Term.TypeLevel[B, Unit]](f.value.tpe match
+          t <- StateT.liftF[ErrorF, List[Statement], Term.TypeLevel[B, Y]](f.value.tpe match
             case Term.TypeLevel.App.App1(qnt, tfun, targ, dep) => Left(List(Error(s"${sp.file}:${sp.line}\nApplication Error"))) 
-            case Term.TypeLevel.App.App2(qnt, tfun, ta, tb, dep) => Right(tb)
+            case Term.TypeLevel.App.App2(qnt, tfun, ta, tb, dep) => Right(tb.asInstanceOf[Term.TypeLevel[B, Y]])
             case Term.TypeLevel.App.App3(qnt, tfun, ta1, ta2, tb, dep) => Left(List(Error(s"${sp.file}:${sp.line}\nApplication Error"))) 
+            case Term.TypeLevel.App.Infix(qnt, tfun, ta, tb, dep) => Right(tb.asInstanceOf[Term.TypeLevel[B, Y]])
             case Term.TypeLevel.Lam.Function1Type(qnt, dep) => Left(List(Error(s"${sp.file}:${sp.line}\nApplication Error"))) 
             case Term.TypeLevel.Var.UserDefinedType(qnt, nme, impl, dep) => Left(List(Error(s"${sp.file}:${sp.line}\nApplication Error")))
             case Term.TypeLevel.Var.ListType(_, dep) => Left(List(Error(s"${sp.file}:${sp.line}\nApplication Error"))) 
diff --git a/src/main/scala/dc10/scala/predef/Functions.scala b/src/main/scala/dc10/scala/predef/Functions.scala
index 17ad53b..ebe5184 100644
--- a/src/main/scala/dc10/scala/predef/Functions.scala
+++ b/src/main/scala/dc10/scala/predef/Functions.scala
@@ -7,23 +7,23 @@ import dc10.scala.{Error, ErrorF, Statement}
 import dc10.scala.Statement.{ExtensionDef, TypeDef, TypeExpr, ValueExpr}
 import dc10.scala.Symbol.{Extension, Term}
 import dc10.scala.Symbol.Term.{TypeLevel, ValueLevel}
-import dc10.scala.Symbol.Term.TypeLevel.App.App2
+import dc10.scala.Symbol.Term.TypeLevel.App.Infix
 import org.tpolecat.sourcepos.SourcePos
 import dc10.scala.Statement.TypeDef.Match
 
 trait Functions[F[_]]:
 
-  extension [A, B] (domain: F[TypeExpr[A, Unit]])
+  extension [A, B, Y, Z] (domain: F[TypeExpr[A, Y]])
     @scala.annotation.targetName("fun1T")
-    def ==>(codomain: F[TypeExpr[B, Unit]]): F[TypeExpr[A => B, Unit]]
+    def ==>(codomain: F[TypeExpr[B, Z]]): F[TypeExpr[A => B, Unit]]
 
   extension [Z, A, B] (domain: F[(TypeExpr[A, Z], TypeExpr[A, Z])])
     @scala.annotation.targetName("fun2T")
     def ==>(codomain: F[TypeExpr[B, Z]]): F[TypeExpr[(A, A) => B, Z]]
 
-  extension [Z, A, B] (fa: F[ValueExpr[A, Z]])
+  extension [A, B, X, Y] (fa: F[ValueExpr[A, Y]])
     @scala.annotation.targetName("fun1V")
-    def ==>(f: ValueExpr[A, Z] => F[ValueExpr[B, Z]]): F[ValueExpr[A => B, Z]]
+    def ==>(f: ValueExpr[A, Y] => F[ValueExpr[B, X]]): F[ValueExpr[A => B, Unit]]
 
   extension [A, B] (fa: F[(ValueExpr[A, Unit], ValueExpr[A, Unit])])
     @scala.annotation.targetName("fun2V")
@@ -40,16 +40,16 @@ object Functions:
 
   trait Mixins extends Functions[[A] =>> StateT[ErrorF, List[Statement], A]]:
  
-    extension [A, B] (domain: StateT[ErrorF, List[Statement], TypeExpr[A, Unit]])
+    extension [A, B, Y, Z] (domain: StateT[ErrorF, List[Statement], TypeExpr[A, Y]])
       @scala.annotation.targetName("fun1T")
       def ==>(
-        codomain: StateT[ErrorF, List[Statement], TypeExpr[B, Unit]]
+        codomain: StateT[ErrorF, List[Statement], TypeExpr[B, Z]]
       ): StateT[ErrorF, List[Statement], TypeExpr[A => B, Unit]] =
         for
           a <- domain
           b <- codomain
           v <- StateT.pure[ErrorF, List[Statement], TypeLevel[A => B, Unit]](
-            Term.TypeLevel.App.App2(
+            Term.TypeLevel.App.Infix(
               None,
               Term.TypeLevel.Lam.Function1Type(None, ()),
               a.tpe,
@@ -81,16 +81,18 @@ object Functions:
     
         yield TypeExpr(v)
 
-    extension [Z, A, B] (fa: StateT[ErrorF, List[Statement], ValueExpr[A, Z]])
+    extension [A, B, X, Y] (fa: StateT[ErrorF, List[Statement], ValueExpr[A, Y]])
       @scala.annotation.targetName("fun1V")
       def ==>(
-        f: ValueExpr[A, Z] => StateT[ErrorF, List[Statement], ValueExpr[B, Z]]
-      ): StateT[ErrorF, List[Statement], ValueExpr[A => B, Z]] =
+        f: ValueExpr[A, Y] => StateT[ErrorF, List[Statement], ValueExpr[B, X]]
+      ): StateT[ErrorF, List[Statement], ValueExpr[A => B, Unit]] =
         for
-          a <- StateT.liftF[ErrorF, List[Statement], ValueExpr[A, Z]](fa.runEmptyA)
+          a <- StateT.liftF[ErrorF, List[Statement], ValueExpr[A, Y]](fa.runEmptyA)
           b <- f(a)
-          t <- StateT.pure[ErrorF, List[Statement], TypeLevel[A => B, Z]](Term.TypeLevel.App.App2(None, Term.TypeLevel.Lam.Function1Type(None, a.value.tpe.dep), a.value.tpe, b.value.tpe, a.value.tpe.dep))
-          v <- StateT.pure[ErrorF, List[Statement], ValueLevel[A => B, Z]](Term.ValueLevel.Lam.Lam1(None, a.value, b.value, t))
+          t <- StateT.pure[ErrorF, List[Statement], TypeLevel[A => B, Unit]](
+            Term.TypeLevel.App.App2(None, Term.TypeLevel.Lam.Function1Type(None, a.value.tpe.dep), a.value.tpe, b.value.tpe, ())
+          )
+          v <- StateT.pure[ErrorF, List[Statement], ValueLevel[A => B, Unit]](Term.ValueLevel.Lam.Lam1(None, a.value, b.value, t))
         yield ValueExpr(v)
 
     extension [A, B] (fa: StateT[ErrorF, List[Statement], (ValueExpr[A, Unit], ValueExpr[A, Unit])])
@@ -129,7 +131,7 @@ object Functions:
         l <- StateT.liftF(cases(a).runEmptyS)
         c <- StateT.liftF(l.map(s => s match
           case TypeExpr(tpe) => tpe match
-            case App2(qnt, tfun, ta, tb, dep) => Right(App2(qnt, tfun, ta, tb, dep))
+            case Infix(qnt, tfun, ta, tb, dep) => Right(Infix(qnt, tfun, ta, tb, dep))
             case _ => Left(List(Error(s"${sp.file}:${sp.line}\nMatch types error: expected function but found ${tpe}")))
           case _ => Left(List(Error(s"${sp.file}:${sp.line}\nMatch types error: expected cases but found ${a.tpe}")))
         ).sequence)
diff --git a/src/main/scala/dc10/scala/predef/datatype/ComplexTypes.scala b/src/main/scala/dc10/scala/predef/datatype/ComplexTypes.scala
index d78c438..ed85bc7 100644
--- a/src/main/scala/dc10/scala/predef/datatype/ComplexTypes.scala
+++ b/src/main/scala/dc10/scala/predef/datatype/ComplexTypes.scala
@@ -32,9 +32,7 @@ object ComplexTypes:
       StateT.pure(TypeExpr(Term.TypeLevel.Var.ListType(None, ())))
       
     def List[A]: StateT[ErrorF, List[Statement], ValueExpr[List[A], Unit]] =
-      for
-        v <- StateT.pure[ErrorF, List[Statement], ValueExpr[List[A], Unit]](ValueExpr(Term.ValueLevel.Var.ListCtor(None, Term.TypeLevel.Var.ListType(None, ()))))
-      yield v
+      StateT.pure[ErrorF, List[Statement], ValueExpr[List[A], Unit]](ValueExpr(Term.ValueLevel.Var.ListCtor(None, Term.TypeLevel.Var.ListType(None, ()))))
     
     extension [A] (list: StateT[ErrorF, List[Statement], ValueExpr[List[A], Unit]])
       @scala.annotation.targetName("appVL")
diff --git a/src/main/scala/dc10/scala/version/package.scala b/src/main/scala/dc10/scala/version/package.scala
index 33aa500..1b842e5 100644
--- a/src/main/scala/dc10/scala/version/package.scala
+++ b/src/main/scala/dc10/scala/version/package.scala
@@ -64,8 +64,9 @@ given `3.3.1`: Renderer["scala-3.3.1", Error, List[Statement]] =
       tpe match
         // application
         case Term.TypeLevel.App.App1(qnt, tfun, targ, z) => s"${renderType(tfun)}[${renderType(targ)}]"
-        case Term.TypeLevel.App.App2(qnt, tfun, ta, tb, z) => s"${renderType(ta)} ${renderType(tfun)} ${renderType(tb)}"
+        case Term.TypeLevel.App.App2(qnt, tfun, ta, tb, z) => s"${renderType(tfun)}[${renderType(ta)}, ${renderType(tb)}]"
         case Term.TypeLevel.App.App3(qnt, tfun, ta1, ta2, tb, z) => s"${renderType(ta1)} ${renderType(tfun)} ${renderType(tb)}"
+        case Term.TypeLevel.App.Infix(qnt, tfun, ta, tb, z) => s"${renderType(ta)} ${renderType(tfun)} ${renderType(tb)}"
         // primitive
         case Term.TypeLevel.Var.BooleanType(_, z) => "Boolean"
         case Term.TypeLevel.Var.IntType(_, z) => "Int"