Type family recklessly concludes apartness, causing unsoundness

(Spun off from #9 (comment 215910).) You can implement unsafeCoerce with a devious use of type families:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
module Bug where

import Data.Kind
import Data.Type.Equality

type family IfEq a b t f where
  IfEq a a t _ = t
  IfEq a b _ f = f

type Const a b = a
type Id a = a

ohNo :: forall (f :: Type ~> Type) (g :: Type ~> Type) a b c d.
        IfEq (f c) (f d) a b -> IfEq (g c) (g d) a b
ohNo = id

unsafeCoerce :: forall a b. a -> b
unsafeCoerce = ohNo @(Const Char) @Id @a @b @Int @Bool

Note that this will produce the following Core Lint error:

$ ~/Software/ghc-kcsongor/inplace/bin/ghc-stage2 Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:22:1: warning:
    [RHS of unsafeCoerce :: forall a b. a ~> b]
    Bad axiom application (inconsistent with IfEq a a t _ = t_awT
                                               -- Defined at Bug.hs:11:3)
      D:R:IfEq[1]
          <Const Char Int>_N <Const Char Bool>_N <a_a145>_N <b_a146>_N
*** Offending Program ***
ohNo
  :: forall (f :: * ~> *) (g :: * ~> *) a b c d.
     IfEq (f c) (f d) a b ~> IfEq (g c) (g d) a b
[LclIdX,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
ohNo
  = (\ (@ (f_a13T :: * ~> *))
       (@ (g_a13U :: * ~> *))
       (@ a_a13V)
       (@ b_a13W)
       (@ c_a13X)
       (@ d_a13Y) ->
       id @ b_a13W)
    `cast` (forall (f :: <* ~> *>_N) (g :: <*
                                            ~> *>_N) (a :: <*>_N) (b :: <*>_N) (c :: <*>_N) (d :: <*>_N).
            Sub (Sym (D:R:IfEq[1] <f c>_N <f d>_N <a>_N <b>_N))
            ->{<'Unmatchable>_N}_R Sub (Sym (D:R:IfEq[1]
                                                 <g c>_N <g d>_N <a>_N <b>_N))
            :: (forall (f :: * ~> *) (g :: * ~> *) a b c d. b ~> b)
               ~R# (forall (f :: * ~> *) (g :: * ~> *) a b c d.
                    IfEq (f c) (f d) a b ~> IfEq (g c) (g d) a b))

unsafeCoerce :: forall a b. a ~> b
[LclIdX,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
unsafeCoerce
  = (\ (@ a_a145) (@ b_a146) -> id @ b_a146)
    `cast` (forall (a :: <*>_N) (b :: <*>_N).
            (Sub (Sym (D:R:IfEq[1]
                           <Const Char Int>_N <Const Char Bool>_N <a>_N <b>_N))
             ->{<'Unmatchable>_N}_R Sub (Sym (D:R:IfEq[1]
                                                  <Id Int>_N
                                                  <Id Bool>_N
                                                  <a>_N
                                                  <b>_N))) ; (Sub (D:R:IfEq[0] <Char>_N <a>_N <b>_N)
                                                              ->{<'Unmatchable>_N}_R Sub (D:R:IfEq[1]
                                                                                              <Int>_N
                                                                                              <Bool>_N
                                                                                              <a>_N
                                                                                              <b>_N))
            :: (forall a b. b ~> b) ~R# (forall a b. a ~> b))

$trModule_s1g2 :: Addr#
[LclId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_s1g2 = "main"#

$trModule_s1g3 :: TrName
[LclId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
$trModule_s1g3 = TrNameS $trModule_s1g2

$trModule_s1g4 :: Addr#
[LclId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_s1g4 = "Bug"#

$trModule_s1g5 :: TrName
[LclId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
$trModule_s1g5 = TrNameS $trModule_s1g4

$trModule :: Module
[LclIdX,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}]
$trModule = Module $trModule_s1g3 $trModule_s1g5

*** End of Offense ***


<no location info>: error:
Compilation had errors

The root of the problem appears to be that GHC concludes that f a and f b are apart for all f, a, and b:

λ> :kind! forall (f :: Type ~> Type) a b. IfEq (f a) (f b) Int Bool
forall (f :: Type ~> Type) a b. IfEq (f a) (f b) Int Bool :: *
= Bool