Redundant constraint warning does not account for pattern checking

Summary

Constraints that are only required for pattern checking are falsely reported as redundant.

Steps to reproduce

{-# language DataKinds, GADTs, TypeOperators, AllowAmbiguousTypes #-}
{-# options_ghc -Wall -Wredundant-constraints #-}

import Data.Type.Bool 
import Data.Type.Equality

-- | Singletons for 'Bool'
data SBool b where
  SFalse :: SBool 'False
  STrue :: SBool 'True

-- | If a disjunction is false, so is its left argument.
orL :: (a || b) ~ 'False => SBool a -> a :~: 'False
orL SFalse = Refl

GHC tells me the (a || b) ~ 'False constraint is redundant.

Expected behavior

I expect the above to compile without warnings.

Discussion

The constraint is redundant—for type checking: orR will pass the type checker if it's removed. However, it's not redundant for pattern checking—the pattern checker will produce a warning if it's removed. Is there a way to account for which constraints the pattern checker "uses", and avoid warning about ones that it does?

Environment

• GHC version used: 9.4.1

Optional:

• Operating System:
• System Architecture: