content: {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE StandaloneKindSignatures #-}
  
  module T21338 where
  
  import Data.Kind ( Type, Constraint )
  import Data.Proxy ( Proxy(..) )
  
  newtype K a b = K a
  
  type NP :: (Type -> Type) -> [Type] -> Type
  data NP f xs where
  
  data FieldInfo a
  
  type All :: [Type] -> Constraint
  type family All xs where {}
  
  data ConstructorInfo :: [Type] -> Type where
    Record :: All xs => NP (K String) xs -> ConstructorInfo xs
  
  hmap :: (forall a. f a -> g a) -> h f xs -> h g xs
  hmap _ _ = undefined
  
  foo :: forall a flds. ConstructorInfo flds
  foo = undefined
  
  fieldNames :: forall (a :: Type) flds. NP (K String) flds
  fieldNames = case foo @a {- @flds -} of
    Record np -> hmap id np
    _ -> hmap undefined @flds
         -- The last line caused a "No skolem info" panic on GHC 9.2 and below.
  