No proxies thanks to -XTypeApplications!

demoteNat.hs

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}

data Nat = Z | S Nat

class Demote (a :: k) base | a -> base where
    demote :: base

instance Demote 'Z Integer where
    demote = 0

instance forall n. Demote n Integer => Demote ('S n) Integer where
    demote = 1 + demote @n

type Four = S (S (S (S Z)))

main :: IO ()
main = print $ demote @Four

simpleSample.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications    #-}

class ShowType a where
  showType :: String
  
instance ShowType Int where
  showType = "Int"
  
instance ShowType Bool where
  showType = "Bool"
  
main :: IO ()
main = do
  putStrLn $ showType @Int
  putStrLn $ showType @Bool