Explore using pure unifier instead of monadic one

GHC contains no fewer than three unifiers! This ticket is about removing one of them.

Here are the three:

1. The eager monadic unifier, implemented in TcUnify, takes the first stab at unification during type inference. If it runs into trouble, it defers the equality to the solver. It returns a coercion.
2. The pure unifier works to sort out type family reductions, instance selection, and rule matching. It's implemented in Unify. This unifier returns, upon success, a substitution.
3. The solver contains a unification-like algorithm in TcCanonical that decomposes equalities en route to solving them.

Simon and I hit upon a radical idea this morning: what if eager unification simply called the pure unifier? The pure unifier can also take a set (or description) of variables that can be in the domain of the returned substitution. In the case of the eager unifier, this domain would be the metavariables. The pure unifier would, if successful, return a substitution from metavariables to types, and the monadic code would simply use this substitution to fill in the types.

It's not yet clear what the implications of this change would be on performance, but it seems like an interesting idea to try.

Trac metadata

Trac field	Value
Version	8.2.2
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed milestone to %8.6.1

changed weight to 5

added Ttask Trac import labels

Simon and I hit upon a radical idea this morning: what if eager unification simply called the pure unifier?

One problem with this: we'd need to zonk, and then call the pure unifier; two passes, which seems sub-optimal.

changed milestone to %8.8.1

These won't be addressed for GHC 8.6.

changed milestone to %8.10.1

Bumping milestones of low-priority tickets.

added Pnormal label

removed milestone