content: {-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
  {-# LANGUAGE BangPatterns #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE EmptyCase #-}
  module Lib where
  
  import Data.Type.Equality
  import Data.Functor.Identity
  import Data.Void
  
  f :: a :~: Int -> a :~: Bool -> ()
  f !_ x = case x of {}
  
  g :: Identity (a :~: Int) -> a :~: Bool -> ()
  g (Identity _) Refl = ()
  
  data SMaybe a = SNothing
                | SJust !a
  
  -- | Exhaustive. Note how in addition to @{(a,b) | b /~ True}@, the value set
  -- @{(a,b) | y /~ SNothing, b ~ True}@ flows into the next equation, but @y@ is
  -- no longer in scope. Normally, we have no way of matching on that without a
  -- wildcard match, but in this case we refute @y ~ SJust z@ by unleashing type
  -- evidence saying that @z@ must be 'Void' by matching on 'Refl'.
  h :: forall a. a :~: Void -> Bool -> ()
  h _     True  | let y = undefined :: SMaybe a, SNothing <- y = ()
  h Refl  False                                    = ()
  