So, one way we can get unification is by doing it in “the stupidest way possible”, i.e. by just saying “this is so”. We introduce *type quotients* (I’m guessing the type theorists have their own name for this concept). Essentially, we’d want to allow introduction of rules like the following (warning, ad-hoc syntax).

```
quot<A, B> UnitMul<A, B> = UnitMul<B, A> where ..;
```

More specifically, we have a grammar like

```
quot_type := "quot" TyParams? Ty = Ty Where? ";"
```

which does more-or-less what you expect: two copies of `Mul`

are glued together along the given equality. Unfortunately there’s a few problems with this:

- There’s no good way to say “ah yes this is
*how* these types are equivalent”, unless we require the types to both be ZSTs or uninhabited, unless we require a `const`

body after the declaration or whatever.
- This is probably a coherence and inference disaster.

As a neat example, type aliases desugar to quotients:

```
type New<T, ..> = Ty<F<T>, ..>;
// becomes
struct New<T, ..> = { /* fields of Ty<F<T>, ..> */ }
quot<T, ..> New<T, ..> = Ty<F<T>, ..> where ..;
```

which is admittedly a pretty silly example.

I rather like this solution, because it doesn’t require us to bake units into the language, *and* we can build much more hilariously complicated structures than what is essentially the polynomial ring `Z[x1, x2, ...]`

. Of course, it’s also hilariouslly unfeasible.