Type equality in constraint not used?

{-# LANGUAGE TypeInType #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

import Data.Kind

data TyRep :: forall k. k -> Type where
  TyInt   :: TyRep Int
  TyBool  :: TyRep Bool
  TyMaybe :: TyRep Maybe
  TyApp   :: TyRep f -> TyRep x -> TyRep (f x)

zero :: Type ~ k => TyRep (a :: k) -> a
zero = undefine

fails with the error

ttest.hs:13:39: error:
    • Expected a type, but ‘a’ has kind ‘k’
    • In the type signature: zero :: Type ~ k => TyRep (a :: k) -> a

But if you replace zero with

zero :: TypeRep (a :: Type) -> a
zero = undefined

then the program compiles.