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

type family If cond tru fls where
  If True tru fls = tru
  If False tru fls = fls

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 undefined  -- inaccessible code warning; can I tell GHC that this is ok?
foo ST k = k 43 "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")