error "illegal type synonym family application" in a dependent type family

Take a look at this example:

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# OPTIONS_GHC -Wno-star-is-type #-}

module Example where

import Data.Type.Bool
import Data.Type.Ord
import GHC.Base
import GHC.Natural

type TypeOf ∷ Symbol → ★
type family TypeOf symbol

type Baseline ∷ ∀ (symbol ∷ Symbol) → TypeOf symbol
type family Baseline symbol

type CompareWithBaseline ∷ ∀ (symbol ∷ Symbol) → TypeOf symbol → Ordering
type family CompareWithBaseline symbol (input ∷ TypeOf symbol) where
  CompareWithBaseline symbol input = Compare input (Baseline symbol)

So far so good:

λ type instance TypeOf "x" = Natural
λ type instance Baseline "x" = 0
λ :kind! CompareWithBaseline "x" 0
CompareWithBaseline "x" 0 ∷ Ordering
= 'EQ

However, this slightly more complicated variant does not compile:

type CompareSingletonListWithBaseline ∷ ∀ (symbol ∷ Symbol) → [TypeOf symbol] → Ordering
type family CompareSingletonListWithBaseline symbol (input ∷ [TypeOf symbol]) where
  CompareSingletonListWithBaseline symbol '[input] = Compare input (Baseline symbol)

λ :reload
[1 of 1] Compiling Example          ( Example.hs, interpreted )

Example.hs:27:3: error:
    • Illegal type synonym family application ‘TypeOf
                                                 symbol’ in instance:
        CompareSingletonListWithBaseline
          symbol ((':) @(TypeOf symbol) input ('[] @(TypeOf symbol)))
    • In the equations for closed type family ‘CompareSingletonListWithBaseline’
      In the type family declaration for ‘CompareSingletonListWithBaseline’
   |
27 |   CompareSingletonListWithBaseline symbol '[input] = Compare input (Baseline symbol)
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

What is it saying? In what instance? Why illegal? Since when? Everything was legal 4 lines above!

Here is a more realistic example:

type BelowBaseline ∷ ∀ (symbol ∷ Symbol) → [TypeOf symbol] → [TypeOf symbol]
type family BelowBaseline symbol (input ∷ [TypeOf symbol]) where
  BelowBaseline symbol '[] = '[]
  BelowBaseline symbol (value : values) =
    If
      (Baseline symbol <=? value)
      (BelowBaseline symbol values)
      (value : BelowBaseline symbol values)

This should only keep those items of a given list which are less than the baseline.

Writing a specific symbol instead of a variable makes things work:

type CompareSingletonListWithBaseline' ∷ ∀ (symbol ∷ Symbol) → [TypeOf symbol] → Ordering
type family CompareSingletonListWithBaseline' symbol (input ∷ [TypeOf symbol]) where
  CompareSingletonListWithBaseline' "x" '[input] = Compare input (Baseline "x")

type BelowBaseline' ∷ ∀ (symbol ∷ Symbol) → [TypeOf symbol] → [TypeOf symbol]
type family BelowBaseline' symbol (input ∷ [TypeOf symbol]) where
  BelowBaseline' "x" '[] = '[]
  BelowBaseline' "x" (value : values) =
    If
      (Baseline "x" <=? value)
      (BelowBaseline' "x" values)
      (value : BelowBaseline' "x" values)

type instance TypeOf "x" = Natural

— But only if the type instance of TypeOf for this symbol is given alongside, as here. Likewise, saying:

type instance TypeOf symbol = ( )

— Makes all these errors go away. However, my goal is to allow someone else to import this module, define their own symbols with type instances of TypeOf and Baseline, and have the function BelowBaseline work with those yet unknown symbols. Listing all allowed cases of symbol defeats the purpose of this exercise.

I am not sure if this is a bug, a documentation issue or a feature request. It seems like a feature that should work is not working, the feature being dependent quantification in kind checking of type families. But the error I get is usually seen when working with classes, not with closed type families. In the setting of classes this error is easy to understand — type synonyms should not show up in heads of instances. Do closed type families have instances? Do those instances have heads? Why is it that the simple example above works but a tiny bit more complicated one does not? Is dependent quantification supposed to work like this to begin with?