This fix introduces capture-avoiding substitution using the rapier
algorithm described in the "Secrets of the Glasgow Haskell Compiler
inliner" paper.

Local uniques are generated by the mkLocalUnique function in the Env
module. See Note [Local uniques]

Added a draft that explains the ambiguity of the syntax of types.

The solver correctly identifies `Bool ~ Maybe Bool` as an irreducible
constraint, but the typechecker forgets it because I had defined
solveIrredCt as "pure ()".

The problem was that we weren't emmiting equalities between
the taus we created before inferring the type of bindings,
and the taus that tcValBinds returns.