{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}

import           Data.Kind
import           Data.Proxy
import           GHC.TypeLits

type family TypeId (tp :: k) :: Nat

type instance TypeId Int    = 1
type instance TypeId String = 2

-- Fails:
getTypeId :: forall tp . tp -> Int
getTypeId _ = fromIntegral . natVal $ Proxy @ (TypeId tp)

-- main.hs:21:30: error:
--     • No instance for (KnownNat (TypeId tp))
--         arising from a use of ‘natVal’
--     • In the second argument of ‘(.)’, namely ‘natVal’
--       In the expression: fromIntegral . natVal
--       In the expression: fromIntegral . natVal $ Proxy @(TypeId tp)

-- Works
getTypeId' :: forall tp . KnownNat (TypeId tp) => tp -> Int
getTypeId' _ = fromIntegral . natVal $ Proxy @ (TypeId tp)

main = do print (getTypeId (123     :: Int))
          print (getTypeId ("hello" :: String))