content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE EmptyCase #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# OPTIONS_GHC -Wincomplete-patterns #-}
  module Bug where
  
  import Data.Kind (Type)
  import Data.Type.Equality ((:~:)(..))
  import Data.Void (Void)
  
  data SBool :: Bool -> Type where
    SFalse :: SBool False
    STrue  :: SBool True
  data SUnit :: () -> Type where
    SUnit :: SUnit '()
  
  type family IsUnit (u :: ()) :: Bool where
    IsUnit '() = True
  
  sIsUnit :: SUnit u -> SBool (IsUnit u)
  sIsUnit SUnit = STrue
  
  type family If (c :: Bool) (t :: Type) (f :: Type) :: Type where
    If True  t _ = t
    If False _ f = f
  
  type family F (u1 :: ()) (u2 :: ()) :: Type where
    F u1 u2 =
      If (IsUnit u1) (Case u2) Int
  
  type family Case (u :: ()) :: Type where
    Case '() = Int
  
  g1 :: F u1 u2 :~: Char
     -> SUnit u1 -> SUnit u2
     -> Void
  g1 Refl su1 su2
    | STrue <- sIsUnit su1
    = case su2 of {}
  
  g2 :: F u1 u2 :~: Char
     -> SUnit u1 -> SUnit u2
     -> Void
  g2 Refl su1 su2
    = case sIsUnit su1 of
        STrue ->
          case su2 of {}
  
  