Difference between overriding and subtyping for `def -> val` overriding

[KacperFKorban]

Compiler version

c3d6c48

Minimized code

//> using scala 3.nightly

sealed trait HElem:
  type T
  def elem: T

object HElem:
  def apply[T0](elem0: T0): HElem { type T = T0; val elem: T0 } = new HElem:
    type T = T0
    val elem: T0 = elem0

  def apply1[T0](elem0: T0): HElem { type T = T0; def elem: T0 } = new HElem:
    type T = T0
    val elem: T0 = elem0

def Test =
  val helem1 = HElem.apply1(1) // no error
  val helem = HElem(1) // error

Output

-- [E007] Type Mismatch Error: /home/kpi/wiadro/refinement_typing.scala:18:11 --
18 |  val helem = HElem(1) // error
   |           ^
   |           Found:    HElem{type T = Int; val elem: Int}
   |           Required: HElem{type T = Int; val elem: Int}
   |----------------------------------------------------------------------------
   | Explanation (enabled by `-explain`)
   |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   |
   | Tree: HElem{type T = Int; val elem: Int}
   | I tried to show that
   |   HElem{type T = Int; val elem: Int}
   | conforms to
   |   HElem{type T = Int; val elem: Int}
   | but none of the attempts shown below succeeded:
   |
   |   ==> HElem{type T = Int; val elem: Int}  <:  HElem{type T = Int; val elem: Int}
   |     ==> hasMatchingMember(HElem{type T = Int; val elem: Int} . elem, Int), member = => Int
   |       ==> => Int  <:  Int  = false
   |
   | The tests were made under the empty constraint
    ----------------------------------------------------------------------------

Expectation

I don't know if this should compile or not.

My main issues are:

• the behavior is different for overriding and for subtyping with refinements
• the error (without -explain) has a confusing message
• the error is a Type Mismatch Error when assigning to a val without an expected type