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: