[GHC] #15106: Explore using pure unifier instead of monadic one

#15106: Explore using pure unifier instead of monadic one -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15106 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15106: Explore using pure unifier instead of monadic one -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15106#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC