This transformation transforms type families into a single variant user-defined
type.

This is achieved through the following steps:

• Transform variant and struct instances of the type family into their own
  user-defined type, using the binds as their respective dependent type arguments.
• Transform the type family itself as a variant type with many as many cases as there
  were instances before, encoding the pattern matching as equality premises.
• Projection functions are made for each instance that go from type family to the
  sub type.
• Implicit conversions going from type family to sub type and vice-versa are made
  explicit through the use of the constructor and projections made before. This is achieved
  by inspecting the expression and generating its "real type", and match that to the type
  given by elaboration.

As an example,
given the following type family:

syntax foo(p)
syntax foo{v : t}(a) = t_alias(a)
syntax foo{v : t}(b) = | case_1 | case_2 | ... | case_n
syntax foo{v : t}(c) = { field_1, field_2, ... , field_n }

where p is a parameter type, a, b and c are arguments that match their respective parameter type,
v is a bind that appears in a, b, and c with type t.

This is transformed into:

syntax foo_case_2(v : t) = | case_1 | case_2 | ... | case_n
syntax foo_case_3(v : t) = { field_1, field_2, ... , field_n }

syntax foo(p) =
  | foo_make_case_1{v : t, x : t_alias(a)}(v : t, x : t_alias(a))
    -- if a == p
  | foo_make_case_2{v : t, x : foo_case_2(b)}(v : t, x : foo_case_2(b))
    -- if b == p
  | foo_make_case_3{v : t, x : foo_case_3(c)}(v : t, x : foo_case_2(c))
    -- if c == p

An example of the projection function is as follows:

def $proj_foo_case_1(v : t, x : foo(a)) : t_alias(a)?
def $proj_foo_case_1{v : t, x : t_alias(a)}(v, foo_make_case_1(v, x)) = ?(x)
def $proj_foo_case_1{v : t, x : foo(a)}(v, x) = ?()

Names were specifically chosen here for simplicity.

An interesting case is for iteration types.
When a real type is an iter type of a sub type and it is expected for it to be an iter type of the type family, then special handling is required.

The specific expression that has this mismatch will become an iteration with that expression specifically being the entity that is being iterated on. With the new variable made, that specific conversion is then applied.

For example, take an expression e with real type t_alias(a)* and expected type foo(a)*. It is transformed into:

foo_make_case_1(iter_0)*{iter_0 <- e}

Limitations to this pass are as follows:

• Only expressions are really allowed when having a parameter of a type family. This is due to the syntactic restriction of
  comparisons, since they only allow expressions.

Things to do later/watch out for:

• Name clash avoidance of generated variables has not been implemented. I believe some sort of name generation functionality should probably exist in the IL somewhere.

This pass also introduces a quick fix to totalize which just ensures that the extra clause added does indeed add the bind for type parameters.

For Wasm 2.0 to pass (and also 3.0), this validation error needs to be fixed:

../specification/wasm-2.0/8-reduction.spectec:303.15-303.36: (after pass typefamily-removal) validation error: expression's type
`lane_($lanetype(`%X%`_shape((Pnn : Pnn <: lanetype), `%`_dim(M))))` = `lane_((Pnn : Pnn <: lanetype))` does not equal expected
type `lane_((Pnn : packtype <: lanetype))`

This is due to the sub typing expressions, when checking for equivalence in typing, does not account for equivalence in the sub types. This can be either be fixed in validation or just making Pnn an alias of packtype. Similar issue with 3.0, but with Inn and addrtype.