With ConsSymbol, we now have a way of deconstructing Symbols, but in its current implementation, the resulting head is also a Symbol, and it is only implicitly implied that this will be a single character (it doesn't get solved otherwise).

This is not ideal, as it's not clear from the kind signatures what's happening. My proposal is to introduce a kind Char, which would have literal syntax just like that at the existing value-level Char literals.

With this, the signature of ConsSymbol would be

class ConsSymbol (h :: Char) (t :: Symbol) (s :: Symbol) | h t -> s, s -> h t