Witness should provide the evidence of `value.type =:= T`

[Atry]

Suppose we are creating a XML processing library, we want to ensure all the methods in a XML document only applies to elements that belong to the document.

We can define the document type like this:

trait Element[Owner <: Document with Singleton]

trait Document {
    def createElement(): Element[this.type]
    def appendChild(element: Element[this.type]): Unit
}

However, this approach is problematic when we summon the document for an element:

import shapeless._

def appendToDocument[Owner <: Document with Singleton](
    element: Element[Owner])(
    implicit witnessOwner: Witness.Aux[Owner]) = {
  witnessOwner.value.appendChild(element)
}

cmd2.sc:11: type mismatch;
 found   : Helper.this.Element[Owner]
 required: Helper.this.Element[shapeless.Witness.<refinement>.type]
Note: Owner >: shapeless.Witness.<refinement>.type, but trait Element is invariant in type Owner.
You may wish to define Owner as -Owner instead. (SLS 4.5)
    witnessOwner.value.appendChild(element)
                                   ^

The problem is that Scala compiler does not know Element[witnessOwner.value.type] and Element[Owner] are the same type.

This problem can be resolved if we add a value.type =:= T evidence in Witness, along with the ability of substitution in Scala 2.13.

[Atry]

Or we can define Witness as following:

trait Witness {
    type T = value.type
    val value: Any
}
object Witness {
      type Lt[+T0] = Witness {
          val value: T0
      }
      type Aux[T0] = Witness.Lt[T0] {
          type T = T0
      }
}

Then the evidence can be created as following:

def ev(w: Witness): w.value.type =:= w.T = {
    implicitly
}

[milessabin]

@Atry have you tried that alternative definition of Witness?

[milessabin]

As an aside, a more idiomatic approach to the motivating problem would be something along the lines of,

trait Document {
  trait Element
  def createElement(): Element
  def appendChild(element: Element): Unit
}

ie. use path dependent types to encode family polymorphism.

[Atry]

@milessabin At least the approach works for Dotty 😄

https://scastie.scala-lang.org/Atry/H5ltvYE9T9iD8IwRSdDESg/5

  trait Witness {
    type T = value.type
    val value: Any
  }
  object Witness {
    type Aux[T0] = Witness {
      type T = T0
      val value: T0
    }
  }

  trait Element[+Owner]

  trait Document {
    def createElement(): Element[this.type]
    def appendChild(element: Element[this.type]): Unit
  }

  def proveSameOwner(w: Witness) = {
    implicitly[Element[w.T] =:= Element[w.value.type]]
  }

  def appendToDocument[Owner <: Document with Singleton](
      element: Element[Owner])(
      implicit w: Witness.Aux[Owner]) = {
    val ev: Element[w.T] =:= Element[w.value.type] = proveSameOwner(w)
    w.value.appendChild(ev(element))
  }

[milessabin]

Could you try modifying the shapeless definition as you suggest and see what (if anything) breaks?

[Atry]

The new Witness encoding need some workaround for Scala 2:

https://scalafiddle.io/sf/c6YMHlX/0

trait Witness {
  type T = value.type
  val value: AnyRef
}

object Witness {
  type Aux[T0] = Witness {
    type T = T0
    val value: T0
  }
}

trait Element[+Owner]

trait Document {
    def createElement(): Element[this.type]
    def appendChild(element: Element[this.type]): Unit
}

trait Prover {
  val w: {
    type T
    val value: AnyRef
  }
  def proveSameOwner: Element[w.T] =:= Element[w.value.type]
}

trait WitnessProver extends Prover {
  val w: Witness
  def proveSameOwner = implicitly[Element[w.T] =:= Element[w.value.type]]
}

def appendToDocument[Owner <: Document with Singleton](
    element: Element[Owner])(
    implicit w0: Witness.Aux[Owner]) = {
  val prover: Prover { val w: Witness.Aux[Owner] } = new WitnessProver { val w = w0 }
  import prover._
  
  w.value.appendChild(prover.proveSameOwner(element))
}

[Atry]

The current Witness.Aux[Succ[P]] does not make sense, as Succ[P] is not a singleton type.
It should be Witness.Lt[Succ[P]].