f.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilyDependencies #-}

import Data.Typeable

data Mode = Field | Descr

newtype Tagged tag a = Tagged { runTagged :: a }

type family Inner mode field = r | r -> mode field where
  Inner Field f = Maybe f
  Inner Descr f = Tagged f String

data Pair l r = Pair l r

data ArgF (f :: Mode) = ArgF
  { field1 :: Inner f Char
  , field2 :: Inner f Char
  }

type Sel pat = forall mode. ArgF mode -> Inner mode pat

f :: Sel pat -> IO pat
f sel = undefined

g :: Sel () -> IO tok
g sel = do
  f sel
  undefined

describe :: forall a pat. (Typeable a, Tagged a String ~ Inner Descr pat) => Sel pat -> TypeRep
describe _ = typeOf (undefined :: a)