GitLab

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.

This patch finally deals with the super-delicate question of
superclases in possibly-recursive dictionaries.  The key idea
is the DFun Superclass Invariant (see TcInstDcls):

     In the body of a DFun, every superclass argument to the
     returned dictionary is
       either   * one of the arguments of the DFun,
       or       * constant, bound at top level

To establish the invariant, we add new "silent" superclass
argument(s) to each dfun, so that the dfun does not do superclass
selection internally.  There's a bit of hoo-ha to make sure that
we don't print those silent arguments in error messages; a knock
on effect was a change in interface-file format.

A second change is that instead of the complex and fragile
"self dictionary binding" in TcInstDcls and TcClassDcl,
using the same mechanism for existential pattern bindings.
See Note [Subtle interaction of recursion and overlap] in TcInstDcls
and Note [Binding when looking up instances] in InstEnv.

Main notes are here:

  * Note [Silent Superclass Arguments] in TcInstDcls,
    including the DFun Superclass Invariant

Main code changes are:

  * The code for MkId.mkDictFunId and mkDictFunTy

  * DFunUnfoldings get a little more complicated;
    their arguments are a new type DFunArg (in CoreSyn)

  * No "self" argument in tcInstanceMethod
  * No special tcSimplifySuperClasss
  * No "dependents" argument to EvDFunApp

IMPORTANT
   It turns out that it's quite tricky to generate the right
   DFunUnfolding for a specialised dfun, when you use SPECIALISE
   INSTANCE.  For now I've just commented it out (in DsBinds) but
   that'll lose some optimisation, and I need to get back to
   this.

See Trac #4499

This (annoyingly) requires us to re-flatten the class predicate.
See Note [Flattening in error message generation]

Regression testing and user feedback for GHC 7.0 taught
us a lot.  This patch fixes numerous small bugs, and some
major ones (eg Trac #4484, #4492), and improves type
error messages.

The main changes are:

* Entirely remove the "skolem equivalance class" stuff;
  a very useful simplification

* Instead, when flattening "wanted" constraints we generate
  unification variables (not flatten-skolems) for the
  flattened type function application

* We then need a fixup pass at the end, TcSimplify.solveCTyFunEqs,
  which resolves any residual equalities of form
      F xi ~ alpha

* When we come across a definite failure (e.g. Int ~ [a]),
  we now defer reporting the error until the end, in case we
  learn more about 'a'.  That is particularly important for
  occurs-check errors.  These are called "frozen" type errors.

* Other improvements in error message generation.

* Better tracing messages

In particular, instead of
   Cannot match 'a' with 'b'
we get
   Could not deduce (a~b) from context (F a ~ b)
or whatever

A bit yukky; see Note [Runtime skolems] in TcErrors.
But it works, and the debugger just is yukky in places.

Major pass through type checker:(1) prioritizing equalities, (2) improved Derived mechanism, (3) bugfixes

The error cascade caused puzzling errors in T4093b, and
suppressing some seems like a good plan.  Very few test
outputs change.

and remove the temporary DOpt class workaround.

Improves kind error messages in paticular

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.