object Foundation {

  trait Induction {}

  trait Template {

    type _I <: Induction
    type _V

    type _Node = Foundation.Node[_I, _V]
    type _Setter = Foundation.Setter[_I, _V]

    trait Node_ extends Node.Prime[this.type] {
      override val T: Template.this.type = Template.this
    }

    trait Setter_ extends Node.Prime[this.type] {
      override val T: Template.this.type = Template.this
    }
  }

  type T[I, V] = Template { type _I = I; type _V = V }

  implicit def newTemplate[I <: Induction, V]: Template {
    type _I = I
    type _V = V
  } = ???

  trait XProto {
    val T: Template
  }

  trait Def {

    type Prime <: XProto

    type Lt[+I <: Induction, +V] = Prime { val x: Template { type _I <: I; type _V <: V } }

    type Aux[I <: Induction, V] = Prime { val x: Template { type _I = I; type _V = V } }
  }

  object Node extends Def {

    trait Prime[X <: Template] extends XProto {

      def value: T._V

      def induction: Seq[(T._I, T._V)]
    }
  }
  type Node[+I <: Induction, +V] = Node.Lt[I, V]

  object Setter extends Def {

    trait Prime[X <: Template] extends XProto {

      def link(node: T._Node)(
          to: Seq[(T._I, T._V)]
      ): T._Node
    }
  }
  type Setter[I <: Induction, V] = Setter.Aux[I, V]
}


trait Topology { // constructor of axioms

  type _I <: Topology.AnyGraph._I

  class _Template[V] extends Foundation.Template {
    final type _I = Topology.this._I
    final type _V = V
  }

  type Node[V] = Foundation.Node[_I, V]
  type Setter[V] = Foundation.Setter[_I, V]
}

object Topology {

  object AnyGraph extends Topology {

    trait _I extends Foundation.Induction {}

  }

  object Tree extends Topology {

    trait _I extends AnyGraph._I

  }

  { // sanity

    object t1 extends Tree._Template[Int]

    def node2Setter[I <: Topology.AnyGraph._I, V](v: Foundation.Node[I, V])(
        implicit
        ev: Foundation.T[I, V]
    ): ev._Setter = {

      ???
    }

    val n1: t1._Node = ???
    val setter: t1._Setter = {
      node2Setter[Tree._I, Int](n1) // TODO: error
//      node2Setter(n1) // TODO: same error
      ???
    }
  }
}

Found:    (n1 : t1._Node)
Required: ai.acyclic.six.error1.Foundation.Node.Lt[
  ai.acyclic.six.error1.Topology.Tree._I, Int]

Explanation
===========

Tree: n1
I tried to show that
  (n1 : t1._Node)
conforms to
  ai.acyclic.six.error1.Foundation.Node.Lt[
  ai.acyclic.six.error1.Topology.Tree._I, Int]
but none of the attempts shown below succeeded:

  ==> (n1 : t1._Node)  <:  ai.acyclic.six.error1.Foundation.Node.Lt[   ai.acyclic.six.error1.Topology.Tree._I, Int] CachedTermRef CachedAppliedType
    ==> (n1 : t1._Node)  <:  ai.acyclic.six.error1.Foundation.Node.Prime{   val x:     ai.acyclic.six.error1.Foundation.Template{       type _I <: ai.acyclic.six.error1.Topology.Tree._I; type _V <: Int} } CachedTermRef CachedRefinedType
      ==> (n1 : t1._Node)  <:  ai.acyclic.six.error1.Foundation.Node.Prime CachedTermRef CachedTypeRef
        ==> t1._Node  <:  ai.acyclic.six.error1.Foundation.Node.Prime CachedTypeRef CachedTypeRef
          ==> ai.acyclic.six.error1.Foundation.Node.Lt[t1._I, t1._V]  <:  ai.acyclic.six.error1.Foundation.Node.Prime CachedAppliedType CachedTypeRef
            ==> ai.acyclic.six.error1.Foundation.Node.Prime{   val x:     ai.acyclic.six.error1.Foundation.Template{type _I <: t1._I; type _V <: t1._V       } }  <:  ai.acyclic.six.error1.Foundation.Node.Prime CachedRefinedType CachedTypeRef  = false
      ==> t1._Node  <:  ai.acyclic.six.error1.Foundation.Node.Prime{   val x:     ai.acyclic.six.error1.Foundation.Template{       type _I <: ai.acyclic.six.error1.Topology.Tree._I; type _V <: Int} } CachedTypeRef CachedRefinedType
        ==> ai.acyclic.six.error1.Foundation.Node.Lt[t1._I, t1._V]  <:  ai.acyclic.six.error1.Foundation.Node.Prime{   val x:     ai.acyclic.six.error1.Foundation.Template{       type _I <: ai.acyclic.six.error1.Topology.Tree._I; type _V <: Int} } CachedAppliedType CachedRefinedType
          ==> ai.acyclic.six.error1.Foundation.Node.Lt[t1._I, t1._V]  <:  ai.acyclic.six.error1.Foundation.Node.Prime CachedAppliedType CachedTypeRef
            ==> ai.acyclic.six.error1.Foundation.Node.Prime{   val x:     ai.acyclic.six.error1.Foundation.Template{type _I <: t1._I; type _V <: t1._V       } }  <:  ai.acyclic.six.error1.Foundation.Node.Prime CachedRefinedType CachedTypeRef  = false
          ==> ai.acyclic.six.error1.Foundation.Node.Prime{   val x:     ai.acyclic.six.error1.Foundation.Template{type _I <: t1._I; type _V <: t1._V       } }  <:  ai.acyclic.six.error1.Foundation.Node.Prime{   val x:     ai.acyclic.six.error1.Foundation.Template{       type _I <: ai.acyclic.six.error1.Topology.Tree._I; type _V <: Int} } CachedRefinedType CachedRefinedType
            ==> ai.acyclic.six.error1.Foundation.Node.Prime{   val x:     ai.acyclic.six.error1.Foundation.Template{type _I <: t1._I; type _V <: t1._V       } }  <:  ai.acyclic.six.error1.Foundation.Node.Prime CachedRefinedType CachedTypeRef  = false

The tests were made under the empty constraint

      node2Setter[Tree._I, Int](n1) // TODO: error