un-reduced summonFrom does not fallback to implicitNotFound

[bishabosha]

Compiler version

3.3.1

Minimized code

@annotation.implicitNotFound("there is no Missing!")
trait Missing

inline def summonMissing = compiletime.summonFrom {
  case m: Missing => m
}
inline def summonMissing2 = compiletime.summonInline[Missing]
val x = summonMissing
val y = summonMissing2

Output

-- Error: ----------------------------------------------------------------------
8 |val x = summonMissing
  |        ^^^^^^^^^^^^^
  |        cannot reduce summonFrom with
  |         patterns :  case given m @ _:Missing
  |-----------------------------------------------------------------------------
  |Inline stack trace
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |This location contains code that was inlined from rs$line$1:4
4 |inline def summonMissing = compiletime.summonFrom {
  |                           ^
5 |  case m: Missing => m
6 |}
   -----------------------------------------------------------------------------
1 error found

Expectation

Like with summonInline we should show the custom error message:

-- [E172] Type Error: ----------------------------------------------------------
9 |val y = summonMissing2
  |        ^^^^^^^^^^^^^^
  |        there is no Missing!
  |-----------------------------------------------------------------------------
  |Inline stack trace
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |This location contains code that was inlined from rs$line$1:7
7 |inline def summonMissing2 = compiletime.summonInline[Missing]
  |                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   -----------------------------------------------------------------------------
2 errors found

[bishabosha]

@soronpo I assigned you since you fixed the report for summonInline with https://github.com/lampepfl/dotty/pull/12428

[soronpo]

I'll try to look at it. Things are kind of hectic here in Israel now, and I could use the distraction.

[nicolasstucki]

Alternative / workaround

inline def summonMissing = compiletime.summonFrom {
  case m: Missing => m
  case _ => compiletime.error("there is no Missing!")
}