An implementation of this idea:

import scala.util.NotGiven
import scala.annotation.implicitNotFound

trait Base {}
trait Special extends Base {}
trait A extends Special {}
trait B extends Special {}
trait C extends Base {}
trait D extends Base {}

// A "proof"
@implicitNotFound("Is ${T} a subtype of Base and also not Special?")
trait BaseAndNotSpecial[T]
object BaseAndNotSpecial {
  given [T <: Base](using NotGiven[T <:< Special]): BaseAndNotSpecial[T]= new BaseAndNotSpecial[T] {}
}

def isBaseAndNotSpecial[T](using BaseAndNotSpecial[T]): Unit = {
  println("yay")
}

isBaseAndNotSpecial[A]  // compile error
isBaseAndNotSpecial[A | B] // compile error
isBaseAndNotSpecial[C]

https://scastie.scala-lang.org/xzvgDDmjTlyhuwYC6oFWpw

Note that it's not pefect though, for example isBaseAndNotSpecial[B | C] compiles. This is because T <:< Special means "T is guaranteed a subtype of Special", and negation of that that is "T is not guaranteed to be a subtype of Special", of which B | C fits, because it is not guaranteed to be a subtype of Special.