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.
   • Both are choice types: decompose A?B = C?D; into A = C; B = D; and move on.
   • One is a variardic type: Move past the variardic types until both symbols being compared are finite ones.
   • Else: generate a constraint a = b and move on.
3. When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols. Save these for step (5).
4. Compute the closure of the constraint set.
5. 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.
6. For each type variable, find all the consrtaints the mention it and find the most specific type among them. Replace.

UNIFY (-- {(?) -- Int?Int}.) AND (C A {C A -- C A?B} -- C B; *A; *B; *C.):
    CONSTRAINTS:
        A = All*
        B = All*
        C = All*
        {(?) -- (?)?Int} = {C A -- C A?B}
        (?) = C A
        (?)?Int = A?B
        (?) = A
        Int = B
        (?) = C (?)
        C = 
    WE KNOW:
        A = (?); B = Int; C = ;
    FINALLY:
        C A -- C B
        (?) -- Int