Unexpected warning "redundant constraint" when a Constraint type family is used to limit GADT patterns
Summary
GHC shows a warning "redundant constraint" when a total type family of kind Constraint is used to reduce the list of GADT constructors that have to be used for a complete pattern match.
Steps to reproduce
{-# LANGUAGE GADTs, KindSignatures, DataKinds, ConstraintKinds, TypeFamilies #-}
import Data.Kind
main :: IO ()
main = print $ f SA SC
data T1 = A | B
data T2 = C | D
data ST1 (a :: T1) where
SA :: ST1 'A
SB :: ST1 'B
data ST2 (b :: T2) where
SC :: ST2 'C
SD :: ST2 'D
type family Compatible (a :: T1) (b :: T2) :: Constraint where
Compatible 'A 'C = ()
Compatible 'A 'D = ()
Compatible 'B 'D = ()
Compatible _ _ = Int ~ Bool
f :: Compatible a b => ST1 a -> ST2 b -> Int
f SA SC = 0
f SA SD = 1
f SB SD = 2
GHC warning: Redundant constraint: Compatible a b
Removing the constraint makes pattern match incomplete, so it is not redundant.
Expected behavior
No GHC warning
Environment
- GHC version used: 8.10.7
Optional:
- Operating System: MacOS
- System Architecture: x86