The latest work is OutsideIn(X): http://www.haskell.org/haskellwiki/Simonpj/Talk:OutsideIn This is quite long paper. It describes a framework for constraint-based type inference and then instantiates it with a constraint solver that supports type families, GADTs and type classes. Constraint-based type inference divides type checking into two phases: constraint-generation and solving. In practice the two may be interleaved for efficiency reasons, of course. As an example (does not type check): type family C a type instance C Int = Int c :: a -> C a f :: Int -> Bool f = \n -> c n In order to type check f we generate the *wanted* constraints ("~" denotes equality) (c -> C c) ~ (d -> e) -- from c - n (d -> e) ~ (Int -> Bool) -- from type signature

From the type family declarations we additionally get the top-level axiom:

C Int ~ Int The wanted constraints are now simplified, e.g., c ~ d, C c ~ e -- from the first constraint d ~ Int, e ~ Bool -- from the second constraint c ~ Int, C c ~ Bool, d ~ Int, e ~ Bool -- from the above constraints C Int ~ Bool -- also Now we get an error when combining this with the top-level axiom. If the user specifies type class constraints in the type signature or performs a GADT pattern match we additionally get *given* constraints. The general solver state thus takes the form: G => W where G are the given constraints and W the wanted constraints and "=>" is implication. The solver then "reacts" two constraints from G, two constraints from W, or one from each, until no more simplifications are possible. To make this efficient, the solver also regularly canonicalises constraints. E.g., function symbols go to the left and constructors to the right. Further performance improvements must come from clever indexing the current state to make the search for applicable rules efficient. This solver is currently being implemented in GHC (there's a branch on darcs.h.o), but correctness comes first. It'll probably take a while until this new solver becomes efficient. The paper does not talk about efficiency, but it lists all the rules and many other details. / Thomas On 14 July 2010 18:39, Corey O'Connor wrote:

I believe I have run headlong into issue #3064 in ghc (http://hackage.haskell.org/trac/ghc/ticket/3064). All I think I know is this: * this is a performance issue with the system used to solve type constraints. * the solver is undergoing an overhaul to resolve performance issues in addition to other issues. * An efficient constraint solver is difficult. NP-Complete in the general case?

Beyond that I'm at a loss. What can I read to understand the constraint satisfaction problem as it stands in GHC? Is there a paper on the implementation of the current solver? Anything on how the new solver will differ from the current?

I think I located one page on the new solver: http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsSolving

Cheers, Corey O'Connor _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- If it looks like a duck, and quacks like a duck, we have at least to consider the possibility that we have a small aquatic bird of the family Anatidae on our hands.