{-# LANGUAGE DataKinds, GADTs, TypeFamilies, BlockArguments, LambdaCase #-}

import Data.Type.Equality((:~:)(..))

data SBool b where
  SF :: SBool False
  ST :: SBool True
deriving instance Show (SBool b)

foo :: SBool b -> (Int -> (b :~: True -> String) -> r) -> r
foo SF k = k 42 \case{}
foo ST k = k 43 \_ -> "was true"

main :: IO ()
main = do
  foo SF (\n _ -> print n)  -- 42
  -- foo SF (\n s -> print (s Refl))  -- error! As desired :)
  foo ST (\n s -> print (n, s Refl))  -- (43, "was true")