Simon's fixes to the generated type instances in Generics
This BIG PATCH contains most of the work for the New Coercion Representation See the paper "Practical aspects of evidence based compilation in System FC" * Coercion becomes a data type, distinct from Type * Coercions become value-level things, rather than type-level things, (although the value is zero bits wide, like the State token) A consequence is that a coerion abstraction increases the arity by 1 (just like a dictionary abstraction) * There is a new constructor in CoreExpr, namely Coercion, to inject coercions into terms
Major refactoring of the type inference engine This patch embodies many, many changes to the contraint solver, which make it simpler, more robust, and more beautiful. But it has taken me ages to get right. The forcing issue was some obscure programs involving recursive dictionaries, but these eventually led to a massive refactoring sweep. Main changes are: * No more "frozen errors" in the monad. Instead "insoluble constraints" are now part of the WantedConstraints type. * The WantedConstraint type is a product of bags, instead of (as before) a bag of sums. This eliminates a good deal of tagging and untagging. * This same WantedConstraints data type is used - As the way that constraints are gathered - As a field of an implication constraint - As both argument and result of solveWanted - As the argument to reportUnsolved * We do not generate any evidence for Derived constraints. They are purely there to allow "impovement" by unifying unification variables. * In consequence, nothing is ever *rewritten* by a Derived constraint. This removes, by construction, all the horrible potential recursive-dictionary loops that were making us tear our hair out. No more isGoodRecEv search either. Hurrah! * We add the superclass Derived constraints during canonicalisation, after checking for duplicates. So fewer superclass constraints are generated than before. * Skolem tc-tyvars no longer carry SkolemInfo. Instead, the SkolemInfo lives in the GivenLoc of the Implication, where it can be tidied, zonked, and substituted nicely. This alone is a major improvement. * Tidying is improved, so that we tend to get t1, t2, t3, rather than t1, t11, t111, etc Moreover, unification variables are always printed with a digit (thus a0, a1, etc), so that plain 'a' is available for a skolem arising from a type signature etc. In this way, (a) We quietly say which variables are unification variables, for those who know and care (b) Types tend to get printed as the user expects. If he writes f :: a -> a f = ...blah... then types involving 'a' get printed with 'a', rather than some tidied variant. * There are significant improvements in error messages, notably in the "Cannot deduce X from Y" messages.
Fix an ASSERT failure in FamInstEnv I added a lot of comments too, to explain the preconditions; esp Note [FamInstEnv]
Use mkAppTy Using AppTy in CoreLint was giving a bogus Lint failure
Improve pretty-printing of family instances Fixed Trac #4246
Super-monster patch implementing the new typechecker -- at last This major patch implements the new OutsideIn constraint solving algorithm in the typecheker, following our JFP paper "Modular type inference with local assumptions". Done with major help from Dimitrios Vytiniotis and Brent Yorgey.
FIX #3405
Remove unused imports
FIX #2677
Robustify lookupFamInstEnv, plus some refactoring This patch deals with the following remark Suppose we have type family T a :: * -> * type instance T Int = [] and now we encounter the type (T Int Bool). If we call lookupFamInstEnv on (T Int Bool) we'll fail, because T has arity 1. Indeed, I *think* it's a precondition of lookupFamInstEnv that the supplied types exactly match the arity of the type function. But that precondition is neither stated, nor is there an assertion to check it. With this patch, lookupFamInstEnv can take "extra" type arguments in the over-saturated case, and does the Right Thing. There was a nearly-identical function lookupFamInstEnvUnify, which required the precisely analogous change, so I took the opportunity to combine the two into one function, so that bugs can be fixed in one place. This was a bit harder than I expected, but I think the result is ok. The conflict-decision function moves from FamInst to FamInstEnv. Net lines code decreases, although there are more comments.
Robustify lookupFamInstEnv Suppose we have type family T a :: * -> * type instance T Int = [] and now we encounter the type (T Int Bool). That is perfectly fine, even though T is over-saturated here. This patch makes lookupFamInstEnv robust to such over-saturation. Previously one caller (TcTyFuns.tcUnfoldSynFamInst) dealt with the over-saturation case, but the others did not. It's better to desl with the issue at the root, in lookupFamInstEnv itself.
Minor refactoring to share InstEnv.instanceBindFun
Fix the bug part of Trac #1930
(F)SLIT -> (f)sLit in FamInstEnv
Remove GADT refinements, part 5 - TcGadt RIP - The non-side effecting unification code is now in types/Unify.lhs along with the refinement code needed for GADT record selectors.
Don't import FastString in HsVersions.h Modules that need it import it themselves instead.
Remove leftover NoteTy/FTVNote bits
Fixed warnings in types/FamInstEnv
Make the treatment of equalities more uniform This patch (which is part of the fix for Trac #2018) makes coercion variables be handled more uniformly. Generally, they are treated like dictionaries in the type checker, not like type variables, but in a couple of places we were treating them like type variables. Also when zonking we should use zonkDictBndr not zonkIdBndr.