Kind error with type equality

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)

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire
Operating system
Architecture