In scala, what can be done to prevent compiler from cyclic summoning of implicit premises? And how to avoid them

Question

I'm writing an implementation for Curry-Howard isomorphism in scala, a family of proofs can be defined as an object implementing the following trait:

(the full code repo is uploaded to https://github.com/tribbloid/shapesafe/blob/djl/prove-debug/macro/src/main/scala/org/shapesafe/core/shape/unary/WithNames.scala)

trait ProofSystem[OUB] { // TODO: no IUB?

  trait Proposition extends Serializable {

    type Codomain <: OUB
    def value: Codomain
  }

  case object Proposition {

    type Aux[O <: OUB] = Proposition {
      type Codomain = O
    }

    type Lt[+O <: OUB] = Proposition {
      type Codomain <: O
    }

    // Can't use Aux, syntax not supported by scala
    trait Of[O <: OUB] extends Proposition {
      final type Codomain = O
    }

    case class ToBe[O <: OUB](override val value: O) extends Of[O]
  }

  // doesn't extend T => R intentionally
  // each ProofSystem use a different one to alleviate search burden of compiler (or is it redundant?)

  trait CanProve[-I, +P <: Proposition] {
    def apply(v: I): P

    final def valueOf(v: I): P#Codomain = apply(v).value // TODO: this should be real apply? The above should be 'prove'
  }

  object CanProve {}

  /**
    * representing 2 morphism:
    *
    * - value v --> value apply(v)
    *
    * - type I --> type O
    *
    * which is why it uses =>>
    * @tparam I src type
    * @tparam P tgt type
    */
  class =>>^^[-I, P <: Proposition](
      val toProof: I => P
  ) extends CanProve[I, P] {

    override def apply(v: I): P = toProof(v)
  }

  type -->[-I, O <: OUB] = CanProve[I, Proposition.Aux[O]]
  type ~~>[-I, +O <: OUB] = CanProve[I, Proposition.Lt[O]]

  class =>>[-I, O <: OUB](
      val toOut: I => O
  ) extends =>>^^[I, Proposition.ToBe[O]](v => Proposition.ToBe(toOut(v)))

  def from[I]: Factory[I] = new Factory[I]()

  class Factory[I]() {

    def =>>^^[P <: Proposition](fn: I => P) = new (I =>>^^ P)(fn)

    def =>>[O <: OUB](fn: I => O) = new (I =>> O)(fn)

  }

  def at[I](v: I) = new Summoner[I](v)

  class Summoner[I](v: I) extends Factory[I] {

    implicit def summon[P <: Proposition](
        implicit
        ev: CanProve[I, P]
    ): P = ev.apply(v)

    implicit def summonValue[P <: Proposition](
        implicit
        ev: CanProve[I, P]
    ): P#Codomain = summon(ev).value
  }
}

In one particular case, the compiler got into a dead loop when 2 implicits are defined in a scope:

case class WithNames[
    S1 <: Shape,
    N <: Names
](
    s1: S1,
    newNames: N
) extends Shape {}

object WithNames {

  // TODO: DEAD LOOP!
  implicit def axiom[
      P1 <: LeafShape,
      N <: Names,
      HO <: HList,
      O <: LeafShape
  ](
      implicit
      zip: ZipWithKeys.Aux[N#Keys, P1#_Dimensions#Static, HO],
      toShape: LeafShape.FromRecord.==>[HO, O]
  ): WithNames[P1, N] =>> O = {
    from[WithNames[P1, N]].=>> { src =>
      val keys: N#Keys = src.newNames.keys
      val p1: P1 = src.s1

      val values: P1#_Dimensions#Static = p1.dimensions.static

      val zipped: HO = values.zipWithKeys(keys)
      LeafShape.FromRecord(zipped)
    }
  }

  implicit def theorem[
      S1 <: Shape,
      N <: Names,
      P1 <: LeafShape,
      O <: LeafShape
  ](
      implicit
      lemma1: S1 ~~> P1,
      lemma2: WithNames[P1, N] --> O
  ): WithNames[S1, N] =>> O = {
    from[WithNames[S1, N]].=>> { src =>
      val p1: P1 = lemma1.valueOf(src.s1)

      lemma2.valueOf(
        src.copy(p1)
      )
    }
  }
}

The compiler seems to be stuck on a cyclic proof resolution: it tries to fulfil lemma2 of theorem with itself. If I merge 2 implicits into 1, the problem disappeared:

  implicit def asLeaf[
      S1 <: Shape,
      P1 <: LeafShape,
      N <: Names,
      HO <: HList,
      O <: LeafShape
  ](
      implicit
      lemma: S1 ~~> P1,
      zip: ZipWithKeys.Aux[N#Keys, P1#_Dimensions#Static, HO],
      toShape: LeafShape.FromRecord.==>[HO, O]
  ): WithNames[S1, N] =>> O = {
    from[WithNames[S1, N]].=>> { src =>
      val keys: N#Keys = src.newNames.keys
      val p1: P1 = lemma.valueOf(src.s1)

      val values: P1#_Dimensions#Static = p1.dimensions.static

      val zipped: HO = values.zipWithKeys(keys)
      LeafShape.FromRecord(zipped)
    }
  }

So my questions are:

1. Why this could happen and what change of the scala compiler algorithm could eliminate any cyclic search for proves?

2. How to manually circumvent this error?

I also realised that the canonical implementation of homotopy type theory (https://github.com/siddhartha-gadgil/ProvingGround) actually does most of the inference in runtime, instead of compile-time, which seems to be defeating the purpose. Perhaps this bug is part of the reason?