Composition is the act of taking a stack and a function, and producing the type signature of the resulting stack. It can also be equivalenty seen as the composition of two functions' execution.

1. Generate constraints from the stated type sigs of your functions.
2. Match the RHS of the LHF, and the LHS of the RHF, from right to left. If the two symbols are:
   • Base types: Fail if one is not a parent type of the other. Otherwise, move on.
   • Both function types: Recursively generate constraints, starting with {a} = {b} and expanding the functions using the rule {--} ==> {a -- a} until one constraint set successfully unifies. If nothing works, fail.
   • One is a variardic type: Recursively generate constraints, starting with a = and epanding the constraint to capture more values on the other side until one constraint set successfully unifies. If nothing works, move on.
   • Else: generate a constraint a = b and move on.
3. Solve constraints.
4. Find the combined signature of the first unification that succeeds. If you unify a -- b x and c x -- d, where x is the matched portion and b/c are unmatched ones, you get c a -- b d. Note that either b or c must be empty because of how matching works.
5. For each type variable, find all the consrtaints the mention it and find the most specific type among them. Replace.

Let's compose -- {Int --} and a {a --} -- a; All* a.

1. Our inital constraint set is a = All*.
2. We're matching {Int --} with a {a --}. We compare {Int --} with {a --}. This causes a sub-constraint-solve, starting with no expansions:
   1. {Int --} = {a --} is added to our constraints (also producing rules like Int = a).
   2. We next match with a. This causes a sub-constraint-solve:
      1. a = . This fails because Int = is unsolvable.
      2. Nothing worked, and we have no symbols to consume, so we add no constrants and move on. Luckily, this succeeds.
3. We've found a set of constraints that cause no issues: a = All*; Int = a.
4. For a, the common type among All* and Int is Int.
5. The un-expanded composition type is a -- a. Substituted, our answer is Int -- Int.

Using this method, the type signature of a function suddenly influences how the function operates - A function with a silly signature such as {a -- b} a -- b suddenly knows how many arguments to take as a in every situation, despite not knowing where the function is relative to the latter arguments, for example.

This is bad. Here might be a simpler (yet less robust) composition method:

• Finite arguments must ALWAYS come before indefinite ones.
• No function expansion. {--} to {a -- a} is dangerous.