• simonpj@microsoft.com's avatar
    Major refactoring of the type inference engine · 27310213
    simonpj@microsoft.com authored
    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
     * 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
     * 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.
FamInst.lhs 7.32 KB