This code

{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}

import Data.Kind

data Dict c where
  Dict :: c => Dict c

data T (t :: k)

type family UnT (a :: Type) :: k where
  UnT (T t) = t

untt :: Dict (UnT (T "a") ~ "a")
untt = Dict

tunt :: Dict (T (UnT (T "a")) ~ T "a")
tunt = Dict

fails with this error:

tunt.hs:17:8: error:
    • Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’
      ‘k’ is a rigid type variable bound by
        the type signature for:
          tunt :: forall k. Dict T (UnT (T "a")) ~ T "a"
        at tunt.hs:16:1-38
      When matching types
        UnT (T "a") :: k
        "a" :: GHC.Types.Symbol
    • In the expression: Dict
      In an equation for ‘tunt’: tunt = Dict
    • Relevant bindings include
        tunt :: Dict T (UnT (T "a")) ~ T "a" (bound at tunt.hs:17:1)
   |
17 | tunt = Dict
   | 

Instead I would expect these reductions to take place:

 1. T (UnT (T "a")) ~ T "a"
 2. T "a" ~ T "a"
 3. constraint satisfied (refl)