In Scala 3, should 2 dependent types that depends on 2 equal & singleton objects perceived to be equal? Why or why not?

by

In the following example (my attempt to mimic section feature of LEAN4 prover), I have declared 2 special axioms that allows 2 objects of type Gen[T] to be perceived equal and can be cast to each other, this means genInt1 = genInt2, and genInt1.type =:= genInt2.type, which can be easily proven:

  trait Section[Self <: Section[Self]] {

    implicit def convertPeer(peer: Self): this.type = peer.asInstanceOf[this.type]
  }

  object Section {

    implicit def allPeersAreEqual[
        Self <: Section[Self],
        S1 <: Self & Singleton,
        S2 <: Self & Singleton
    ]: (S1 =:= S2) =
      ???
  }

  object SectionSpec {

    class Gen[T] extends Section[Gen[T]] {

      trait Fn[R]
    }

    object genInt1 extends Gen[Int] {}
    object genInt2 extends Gen[Int] {}
  }

  class SectionSpec {

    import SectionSpec._

    val t1: genInt1.Fn[String] = ???
    val t2: Gen[Int]#Fn[String] = t1

    summon[genInt1.type =:= genInt2.type]
  }

Under this premise, it should be easy to prove equality of 2 dependent types:

    summon[genInt1.Fn[String] =:= genInt2.Fn[String]]
// not working
//  Cannot prove that LeanSection.SectionSpec.genInt1.Fn[String] =:= LeanSection.SectionSpec.genInt2.Fn[String]..

How did this happen? Can I declare additional axioms in the scope of this program to enable such equality check and conversion?

Leave a Comment