Another exposition of Edward's "Closed kinds aren't as closed as you'd think"

Closed.hs

{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language FlexibleInstances #-}
{-# language ScopedTypeVariables #-}

data Unit = U

class C (k :: Unit) where
  get :: Int

instance C 'U where
  get = 0

-- this can be defined already here
standaloneGet :: forall (t :: Unit) . C t => Int
standaloneGet = get @t

-- the problematic 'matchable' type family
type family Succ :: Unit -> Unit

-- Note that this is different:
type family Succ1 (x :: Unit) :: Unit

instance C (f 'U) where
  get = 1

results :: [Int]
results = [get @'U, get @(Succ 'U)]