WIP not working

PolyRecord.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Data (Proxy (Proxy))
import Data.Kind (Type)
import Text.Printf (printf)

-- A record is either:
-- - An empty record
-- - Some record with an added field f
data Record (xs :: [(k, Type)]) where
  Empty :: Record '[]
  WithField :: Proxy x -> a -> Record xs -> Record ('(x, a) ': xs)

instance Show (Record '[]) where
  show Empty = "{}"

instance (Show (Record rest), Show t) => Show (Record ('(x, t) ': rest)) where
  show (WithField p t rest) = printf "{ some_field = %s | %s }" (show t) (show rest)

class HasField x r a | x r -> a where
  getField :: r -> a

instance HasField x (Record ('(x, a) ': xs)) a where
  getField (WithField _ v _) = v

instance HasField x (Record xs) a => HasField x (Record ('(u, z) ': xs)) a where
  getField (WithField _ _ r) = getField @x r

-- We use rank 2 polymorphism to make the compiler believe that those x are all
-- different types making the fields "different"
f :: forall xs y . Int -> Record xs -> (forall x . Record ('(x, Int) : xs) -> x -> y) -> y
f v rest cont = cont (WithField Proxy v rest) ()

test = f 1 Empty one
  where
    one :: forall a . Record '[ '(a, Int) ] -> a -> String
    one r k1 = f 2 r (two k1)

    two :: forall a b . a -> Record ('(b, Int) ': '[ '(a, Int) ]) -> b -> String
    two _ r _ = show @Int $ getField @a r