Proposal for representing sort injections

@goodlyrottenapple says:

we could perhaps get rid of them at the Term level and instead push them into the Sort type?
I think this would make code like the matcher and unifier easier to read,

This is an intriguing idea! 👍 I also believe it will be easier to write the unifier/matcher if we get it right (see below)
Might be worth its own issue, as we need to think this through a bit more. Writing down some ideas here for now.

we would only be matching on actual structure, such as constructors or values and we could handle the matching/unification of the types of both terms in a separate function.
In theory, it could be as simple as having [Sort] in Terms, where e.g.

DomainValue [s1,..sn] x ~ inj{s2, s1}(inj{s3,s2}(...inj{sn, sn-1}(\dv{sn}(x)) ...))

• IIUC that would mean generally transforming terms with such inj chains into a single flat constructor with an ordered (wrt. subsorts), non-empty list of sorts (called sort-chain below), at the time when we convert from text/json to the internal representation (and vice versa).
  inj{s2,s1}(inj{s3,s2}(<constructor>(x)) becomes <constructor'>{s1 :| [s2, s3]}(x)
  where :| is a non-empty list constructor, and s3 subsort s2 subsort s1
• The ordering property would not really matter to us, we assume the injections are correctly-arranged.
• If I understand correctly, a rule match with such sort representation would match a subject term's sort-chain's prefixes to the sort-chain of the pattern term on the LHS. The match would quite probably need to reflect the actual prefix that was matched, as we want to replace that part by whatever the RHS makes from it (if it is a variable), _leaving the suffix intact for subsequent matches).
• I am unsure how this would interact with "shortcut injections" where another component removes the middle sort from a chain like the above (turning inj{s2,s1}(inj{s3,s2}(<constructor>(x)) into inj{s3,s1}(<constructor>(x)) - which is apparently something that the LLVM backend does.

Originally posted by @jberthold in https://github.com/runtimeverification/hs-backend-booster/issues/4#issuecomment-1301485695

Review the current Term and Sort representations, then trace how the matcher and unifier handle sort injections. Compare the proposed flat, ordered sort-chain representation with text/JSON conversion and the mentioned shortcut-injection behavior. Done means the representation and its effects on matching, unification, and conversion are agreed and documented well enough to implement.