f.hs

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

data Mode = Field | Descr
type family Inner mode field where
  Inner Field f = f
  Inner Descr 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

gistfile1.txt

foo.hs:25:5: error:
    • Couldn't match type ‘Inner mode ()’ with ‘Inner mode a0’
      Expected type: ArgF mode -> Inner mode a0
        Actual type: ArgF mode -> Inner mode ()
      NB: ‘Inner’ is a non-injective type family
      The type variable ‘a0’ is ambiguous
    • In the first argument of ‘f’, namely ‘sel’
      In a stmt of a 'do' block: f sel
      In the expression:
        do f sel
           undefined
   |
25 |   f sel