Suppose I want to create two variations of a data type, one that has a certain constructor and one that does not have it, otherwise they are identical. I came up with this:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

data Foo (a :: Bool) where
  A :: Int -> Foo True
  B :: String -> Foo a
  C :: [Int] -> [String] -> Foo a
  None :: Foo a

So far so good. I have Foo True which has A data constructor enabled, and Foo False that has it effectively disabled. But there is a problem.

I cannot come up with a terse way to transform Foo True to Foo False. Here's what works:

removeA :: Foo True -> Foo False
removeA (A _) = None
removeA (B x) = B x
removeA (C xs ys) = C xs ys
removeA None = None

but this is ugly since I have to duplicate all the non-A constructors at both sides of =.

Here's what doesn't work:

removeA :: Foo True -> Foo False
removeA (A _) = None
removeA a = a -- type mismatch: Foo True vs Foo False
removeA a = coerce a -- type mismatch: True vs False

I understand why the first attempt doesn't work, but what about the second? Isn't it supposed to be a phantom type? If not, can I force it to become one? What other options are there?

A smaller problem is that when I try to pattern match a Foo False on A, GHC only emits a warning. Can it be made into a full blown error without enabling -Werror and the like?