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