Major refactoring of the type inference engine
authorsimonpj@microsoft.com <unknown>
Wed, 12 Jan 2011 14:56:04 +0000 (14:56 +0000)
committersimonpj@microsoft.com <unknown>
Wed, 12 Jan 2011 14:56:04 +0000 (14:56 +0000)
commit27310213397bb89555bb03585e057ba1b017e895
tree6ef7f4b2dd55b95d6e83f83c5ddeb963210e0a80
parentfd6de028d045654e42dc375e8c73b074c530f883
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.
34 files changed:
compiler/basicTypes/Name.lhs
compiler/basicTypes/OccName.lhs
compiler/basicTypes/Var.lhs
compiler/ghci/RtClosureInspect.hs
compiler/main/HscTypes.lhs
compiler/main/InteractiveEval.hs
compiler/typecheck/FamInst.lhs
compiler/typecheck/Inst.lhs
compiler/typecheck/TcArrows.lhs
compiler/typecheck/TcBinds.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcClassDcl.lhs
compiler/typecheck/TcEnv.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcExpr.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcMatches.lhs
compiler/typecheck/TcPat.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcRnMonad.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcRules.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcSplice.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs
compiler/types/FamInstEnv.lhs
compiler/types/Unify.lhs
compiler/utils/Bag.lhs