Singletons-like type to value association

Wrapper.hs

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes     #-}
{-# LANGUAGE TypeFamilies   #-}
import           Protolude

data Tag = Foo | Bar

data RTag (t :: Tag) where
  RFoo :: RTag 'Foo
  RBar :: RTag 'Bar

data Wrapped (t :: Tag) =
  Wrapped { innerType :: Inner t }

type family Inner (t :: Tag) :: * where
  Inner 'Foo = Int
  Inner 'Bar = Double


data Wrapper where
  Wrapper :: forall sr . Wrapped sr -> RTag sr -> Wrapper


foo :: Wrapper -> IO ()
foo (Wrapper (Wrapped i) RFoo) = print (i :: Int)
foo (Wrapper (Wrapped d) RBar) = print (d :: Double)