Implicit summoning fail at where variable assignment succeed

[tribbloid]

Reproduction steps

Scala version: 2.13.11

object `this.type <: Compat` {

  trait Law

  trait NodeK[+L <: Law] {
    type Value

    {
      implicitly[this.type <:< NodeK.Compat[L, Value]] // oops, doesn't work

      val k: NodeK.Compat[L, Value] = this // works
    }
  }

  object NodeK {
    type Compat[L <: Law, V] = NodeK[L] { type Value <: V }
  }
}

Problem

The error for the implicit summon is:

Cannot prove that NodeK.this.type <:< ai.acyclic.prover.commons.graph.this.type <: Compat.NodeK.Compat[L,NodeK.this.Value].

Does <:< summoning use different algorithm comparing to type inference of expressions? How weird.

This problem doesn't exist on Scala 3.3.x

[SethTisue]

see my remarks on https://github.com/scala/bug/issues/12952 about filing quality bug reports