{-# LANGUAGE TypeFamilies #-}

data RefinableUniv a where
  AsString :: RefinableUniv String
  AsInt :: RefinableUniv Int

class Refinable a where refine :: RefinableUniv a
instance Refinable String where refine = AsString
instance Refinable Int where refine = AsInt

data Exists f = forall a. Refinable a => MkExists (f a)

-- functor to use in place of f
data InBounds a where
  MkString :: String -> InBounds String
  MkInt :: Int -> InBounds Int

extract :: forall a. Refinable a => Exists InBounds -> a
extract (MkExists @_ @k v) = case refine @k of
  AsInt -> case refine @a of
    AsInt -> case v of MkInt int -> int
    _ -> undefined
  AsString -> case refine @a of
    AsString -> case v of MkString str -> str
    _ -> undefined

val :: Exists InBounds
val = MkExists (MkString "hello!")

main :: IO ()
main = print (extract @String val)