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:
- 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. - 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. - The solver contains a unification-like algorithm in
TcCanonicalthat 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 |