Cannot extract type from refinement in match type

[prolativ]

Compiler version

According to our bisecting tool:
Last good release: 3.1.3-RC1-bin-20220403-a26a2c3-NIGHTLY
First bad release: 3.1.3-RC1-bin-20220404-ad2553d-NIGHTLY

Minimized code

type FAux[A0] = {type A = A0}

type F[t] =
  t match
    case FAux[a] => a

val a: F[{type A = Int}] = 10
val b: F[{type A = String}] = "asd"

Output

[error] /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/StructMatch.scala:7:28: Found:    (10 : Int)
[error] Required: F[Object{A = Int}]
[error] val a: F[{type A = Int}] = 10
[error]                            ^^
[error] /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/StructMatch.scala:8:31: Found:    ("asd" : String)
[error] Required: F[Object{A = String}]
[error] val b: F[{type A = String}] = "asd"
[error] 

Expectation

This should compile without an error as it used to before the regression.

[odersky]

That looks like a duplicate of a bug we closed recently

[prolativ]

Which one? Indeed I had an impression that I've already seen something similar to that but I couldn't find this. Anyway, this still doesn't work on nightly so the fix might have been incomplete

[odersky]

It was #15155. The code looks similar, not sure whether the error is the same.

[prolativ]

Well, the fix for #15155 made the error message more verbose but this still does not compile (I'm checking this directly on the main branch as the nightly release currently available on maven seems to be one day older and does not incorporate the fix)

-- [E007] Type Mismatch Error: /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/StructMatch.scala:9:27 
9 |val a: F[{type A = Int}] = 10
  |                           ^^
  |                      Found:    (10 : Int)
  |                      Required: F[Object{A = Int}]
  |
  |                      Note: a match type could not be fully reduced:
  |
  |                        trying to reduce  F[Object{A = Int}]
  |                        failed since selector  Object{A = Int}
  |                        does not match  case FAux[a] => a
  |                        and cannot be shown to be disjoint from it either.
  |
  | longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/StructMatch.scala:10:30 
10 |val b: F[{type A = String}] = "asd"
   |                              ^^^^^
   |                    Found:    ("asd" : String)
   |                    Required: F[Object{A = String}]
   |
   |                    Note: a match type could not be fully reduced:
   |
   |                      trying to reduce  F[Object{A = String}]
   |                      failed since selector  Object{A = String}
   |                      does not match  case FAux[a] => a
   |                      and cannot be shown to be disjoint from it either.
   |
   | longer explanation available when compiling with `-explain`
2 errors found

As suggested by the compiler i tried compiling it with -explain:

-- [E007] Type Mismatch Error: /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/StructMatch.scala:7:27 
7 |val a: F[{type A = Int}] = 10
  |                           ^^
  |                      Found:    (10 : Int)
  |                      Required: F[Object{A = Int}]
  |
  |                      Note: a match type could not be fully reduced:
  |
  |                        trying to reduce  F[Object{A = Int}]
  |                        failed since selector  Object{A = Int}
  |                        does not match  case FAux[a] => a
  |                        and cannot be shown to be disjoint from it either.
  |-----------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree: 10
  | I tried to show that
  |   (10 : Int)
  | conforms to
  |   F[Object{A = Int}]
  | but the comparison trace ended with `false`:
  |
  |   ==> (10 : Int)  <:  F[Object{A = Int}]
  |     ==> Int  <:  F[Object{A = Int}] (left is approximated)
  |       ==> Int  <:  Object{A = Int} match {   case FAux[a] => a } (left is approximated) (right is approximated)
  |       <== Int  <:  Object{A = Int} match {   case FAux[a] => a } (left is approximated) (right is approximated) = false
  |     <== Int  <:  F[Object{A = Int}] (left is approximated) = false
  |     ==> (10 : Int)  <:  Object{A = Int} match {   case FAux[a] => a } (right is approximated)
  |       ==> Int  <:  Object{A = Int} match {   case FAux[a] => a } (left is approximated) (right is approximated)
  |       <== Int  <:  Object{A = Int} match {   case FAux[a] => a } (left is approximated) (right is approximated) = false
  |     <== (10 : Int)  <:  Object{A = Int} match {   case FAux[a] => a } (right is approximated) = false
  |   <== (10 : Int)  <:  F[Object{A = Int}] = false
  |
  | The tests were made under the empty constraint
   -----------------------------------------------------------------------------
-- [E007] Type Mismatch Error: /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/StructMatch.scala:8:30 
8 |val b: F[{type A = String}] = "asd"
  |                              ^^^^^
  |                      Found:    ("asd" : String)
  |                      Required: F[Object{A = String}]
  |
  |                      Note: a match type could not be fully reduced:
  |
  |                        trying to reduce  F[Object{A = String}]
  |                        failed since selector  Object{A = String}
  |                        does not match  case FAux[a] => a
  |                        and cannot be shown to be disjoint from it either.
  |-----------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree: "asd"
  | I tried to show that
  |   ("asd" : String)
  | conforms to
  |   F[Object{A = String}]
  | but the comparison trace ended with `false`:
  |
  |   ==> ("asd" : String)  <:  F[Object{A = String}]
  |     ==> String  <:  F[Object{A = String}] (left is approximated)
  |       ==> String  <:  Object{A = String} match {   case FAux[a] => a } (left is approximated) (right is approximated)
  |       <== String  <:  Object{A = String} match {   case FAux[a] => a } (left is approximated) (right is approximated) = false
  |     <== String  <:  F[Object{A = String}] (left is approximated) = false
  |     ==> ("asd" : String)  <:  Object{A = String} match {   case FAux[a] => a } (right is approximated)
  |       ==> String  <:  Object{A = String} match {   case FAux[a] => a } (left is approximated) (right is approximated)
  |       <== String  <:  Object{A = String} match {   case FAux[a] => a } (left is approximated) (right is approximated) = false
  |     <== ("asd" : String)  <:  Object{A = String} match {   case FAux[a] => a } (right is approximated) = false
  |   <== ("asd" : String)  <:  F[Object{A = String}] = false
  |
  | The tests were made under the empty constraint
   -----------------------------------------------------------------------------
2 errors found

This case seems simpler than #15155
Do we still have any doubts here regarding whether this should reduce or not?
@OlivierBlanvillain what do you think?