content: {-# LANGUAGE EmptyCase #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  module T15305 where
  
  import Data.Void
  
  -- Example 1
  
  data (:+:) f g a = Inl !(f a) | Inr !(g a)
  
  data A
  data B
  
  data Foo l where
    Foo :: Foo A
  
  data Bar l where
    Bar :: Bar B
  
  type Sig = Foo :+: Bar
  
  fun :: Sig B -> Int
  fun (Inr Bar) = 1
  
  -- Example 2
  
  data GhcPass c
  type family XXHsImplicitBndrs x
  type instance XXHsImplicitBndrs (GhcPass _) = Void
  
  data HsImplicitBndrs pass
    = UsefulConstructor
    | XHsImplicitBndrs !(XXHsImplicitBndrs pass)
  
  fun2 :: HsImplicitBndrs (GhcPass pass) -> ()
  fun2 UsefulConstructor = ()
  
  fun2' :: (p ~ GhcPass pass) => HsImplicitBndrs p -> ()
  fun2' UsefulConstructor = ()
  
  -- Example 3
  
  data Abyss = MkAbyss !Abyss
  
  stareIntoTheAbyss :: Abyss -> a
  stareIntoTheAbyss x = case x of {}
  {-
  Alas, this function is marked non-exhaustive, since the way GHC solves
  NonVoid constraints at the moment isn't sophisticated enough to handle
  recursive strict argument types like MkAbyss exhibits. Maybe some day.
  -}
  