import GHC.TypeLits (Nat, natVal, KnownNat)

data Foo = Bar Nat

data SFoo = SBar Int
  deriving (Show)

type family ExtractNat (a :: Foo) :: Nat where
  ExtractNat (Bar x) = x

sing :: forall a. KnownNat (ExtractNat a) => Proxy a -> SFoo