3 classes for Symbol

[Ebmtranceboy]

Three classes resolved by the typechecker (any instance of those would be useless, as for KnownSymbol or KnownNat).

• class SymbolEq symb1 symb2 symbool sets symbool to "True" or "False" according to symb1 == symb2 or not.
  This avoids overlaps when some user instances are only distinguished by a Symbol.

• class AppendSymbol symb1 symb2 symb12 concatenates two Symbols, or extracts the prefix, or extracts the suffix.

• class ConsSymbol symbh symbtail symb either concatenates a 1-character Symbol with a tail, or splits a Symbol according to its first character and its tail.

An example using those classes is provided in tests/ConsSymbolEq.hs

[augustss]

Is this what GHC does? I try to be compatible.

[Ebmtranceboy]

Title: GHC-compatible AppendSymbol (and possibly CmpSymbol) for Data.TypeLits

Motivation

MicroHs already supports Symbol, KnownSymbol, and symbolVal, resolved
specially in TypeCheck.hs (the solvers table, alongside KnownNat and
Coercible). This makes a lot of type-level Symbol programming possible, but
one common building block from GHC.TypeLits is still missing:
AppendSymbol.

In GHC, AppendSymbol is declared as a closed type family with no visible
equations — its reduction is entirely wired into the constraint
solver/normalizer, not written in user-level Haskell:

type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol

Crucially, it is used inline, in type position, and reduces during
unification wherever it appears, e.g.:

f :: Proxy (AppendSymbol "foo" "bar") -> ...

What I tried as a workaround

Without DataKinds or general type families, I prototyped AppendSymbol (and
a couple of related primitives, ConsSymbol and SymbolEq) as an ordinary
multi-parameter class with functional dependencies, resolved specially by the
typechecker exactly like KnownSymbol/Coercible are — i.e. intercepted in
the solvers table by class name, before falling through to solveInst:

class AppendSymbol (s :: Symbol) (t :: Symbol) (st :: Symbol)
  | s t -> st, st t -> s, st s -> t

solveAppendSymbol :: SolveOne
solveAppendSymbol loc iCls [s, t, st] = ...
  -- pattern-matches on ELit (LStr ...) literals, computes the concatenation
  -- or the missing side (given the other two), unifies via Improve, or
  -- errors out on a literal mismatch
solveAppendSymbol loc iCls ts = solveInst loc iCls ts

This works well as a relation: it can check, complete, or reject a triple
of Symbols at compile time, with proper deferral when one side is still a
unification variable. (Happy to share the full patch — it also required a
ConsSymbol h t s primitive for structural decomposition of a literal
Symbol, and a SymbolEq s t b primitive returning "True"/"False" as
disjoint literals, needed to route around what looks like a specificity gap
in instance selection between a concrete Symbol literal and a type
variable — getBestMatches/findMatches in TypeCheck.hs did not seem to
prefer the more specific literal instance over a fully polymorphic one, even
with OverlappingInstances enabled.)

Where this workaround falls short

A class-based relation can never be GHC-compatible in the way
AppendSymbol is normally used, because AppendSymbol "foo" "bar" in GHC is
a type-level expression that reduces to "foobar" wherever it occurs — it
is not merely related to it through an external constraint. Concretely, code
that expects to write Proxy (AppendSymbol "foo" "bar") inline, or to nest
AppendSymbol inside a bigger type, cannot be made to work through a
class/fundep encoding; only three separate, explicitly-threaded type
variables with a constraint between them are possible that way. Since
"a type-level application that reduces during unification" is definitionally
what a type family is (whether user-defined or, as here, wired into the
compiler with no equations), matching GHC's actual AppendSymbol seems to
require some form of type family support, even a very restricted one.

Proposed scope

Given MicroHs's stated goal of GHC compatibility, and that a similarly
special-cased mechanism already exists for KnownSymbol/KnownNat/
Coercible, would you be open to a narrowly-scoped patch that:

1. Parses a closed, equation-free type family signature —
   type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol — without
   supporting the general type family machinery (open families, user
   equations, associated families, etc.).
2. Registers AppendSymbol with kind Symbol -> Symbol -> Symbol in the
   kind checker.
3. Recognizes AppendSymbol lit1 lit2 (both Symbol literals) during type
   normalization/unification (unifyR, or an expandSyn-like pass run
   beforehand) and reduces it directly to the concatenated literal, deferring
   via the existing unification-variable machinery when one side isn't a
   literal yet.

This would be intentionally much narrower than general TypeFamilies
support — closer in spirit to how AppendSymbol itself is "wired in" rather
than user-defined in GHC — and could plausibly extend later to CmpSymbol
if useful, following the same pattern.

If this is out of scope for MicroHs's design goals, the class/fundep
workaround above is a perfectly usable substitute for most purposes (proving
and computing Symbol relations at compile time) — it just can't be a drop-in
replacement for code written against GHC.TypeLits.AppendSymbol syntax.

Happy to share the full prototype (AppendSymbol/ConsSymbol/SymbolEq +
TypeCheck.hs solvers) if useful as a starting point, and to help test a
patch along these lines if you'd like to attempt it.

[augustss]

English, please

[augustss]

Spelling

[augustss]

Please, don't mix formatting changes with actual changes. It makes it harder to see what's actually changed.

[Ebmtranceboy]

ok, sorry