What's the difference between implicitly and summon?

In Scala 3 summon seems to do the same thing as the old implicitly. But when we dig into actual examples we see that isn't the case. For example

case class A(i: Int, s: String)

val mirror    = implicitly[Mirror.Of[A]]    
type ValueOfs = Tuple.Map[mirror.MirroredElemLabels, ValueOf]
val valueOfs  = summonAll[ValueOfs]

def values(t: Tuple): Tuple = t match
  case (h: ValueOf[_]) *: t1 => h.value *: values(t1)
  case EmptyTuple => EmptyTuple

produces the error

cannot reduce inline match with  
 scrutinee:  compiletime.erasedValue[App.ValueOfs] : App.ValueOfs  
 patterns :  case _:EmptyTuple  
             case _:*:[t @ _, ts @ _]

However replacing implicitly[Mirror.Of[A]] with summon[Mirror.Of[A]] compiles fine.

What are the subtleties of summon vs implicitly in this case and in general?

Given

case class A(i: Int, s: String)

we can see that summon and implicitly return the same runtime value

assert(implicitly[Mirror.Of[A]] eq summon[Mirror.Of[A]])

but they have different compile time types

def fun[A,B]( a: A, b: B )( implicit ev: A =:= B ) = ???
fun(implicitly[Mirror.Of[A]], summon[Mirror.Of[A]])
    Cannot prove that deriving.Mirror.Of[Worksheet.A] =:= (
      deriving.Mirror{
        MirroredType = Worksheet.A; MirroredMonoType = Worksheet.A; 
          MirroredElemTypes <: Tuple
      }
     & 
      scala.deriving.Mirror.Product{
        MirroredMonoType = Worksheet.A; MirroredType = Worksheet.A; 
          MirroredLabel = ("A" : String)
      }
    ){
      MirroredElemTypes = (Int, String); 
        MirroredElemLabels = (("i" : String), ("s" : String))
    }.

The one returned by summon is more specific because summon is defined using transparent inline which allow it to evaluate to a more precise type than requested.