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

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 sb k = k 42 case sb of
  ST -> "was true"

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