When I say

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies,
             UndecidableInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module Bug where

import GHC.TypeLits
import GHC.Exts ( Constraint )

type family NotInt a where
  NotInt Int = TypeError (Text "That's Int, silly.")
  NotInt _   = (() :: Constraint)

data T a where
  MkT1 :: a -> T a
  MkT2 :: NotInt a => T a

foo :: T Int -> Int
foo (MkT1 x) = x

I get

Bug.hs:19:1: warning:
    Pattern match(es) are non-exhaustive
    In an equation for ‘foo’: Patterns not matched: MkT2

But I shouldn't.

Even worse, perhaps, GHC accepts my pattern-match against MkT2 if I add it. If I change the TypeError to False ~ True, I get the correct behavior.