[commit: ghc] wip/new-flatten-skolems-Oct14: Simon's major commit to re-engineer the constraint solver (78a0fcb)

Mon Nov 3 17:23:49 UTC 2014

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/new-flatten-skolems-Oct14
Link       : http://ghc.haskell.org/trac/ghc/changeset/78a0fcb13046a86708d683350d844a77849f0ad5/ghc

>---------------------------------------------------------------

commit 78a0fcb13046a86708d683350d844a77849f0ad5
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Nov 3 17:23:11 2014 +0000

    Simon's major commit to re-engineer the constraint solver

    The driving change is this:

    * The canonical CFunEqCan constraints now have the form
           [G] F xis ~ fsk
           [W] F xis ~ fmv
      where fsk is a flatten-skolem, and fmv is a flatten-meta-variable
      Think of them as the name of the type-function application

    See Note [The flattening story] in TcFlatten.  A flatten-meta-variable
    is distinguishable by its MetaInfo of FlatMetaTv

    This in turn led to an enormous cascade of other changes, which simplify
    and modularise the constraint solver.  In particular:

    * Basic data types
        * I got rid of inert_solved_funeqs altogether. It serves no useful
          role that inert_flat_cache does not solve.

        * I added wl_implics to the WorkList, as a convenient place to
          accumulate newly-emitted implications; see Note [Residual
          implications] in TcSMonad.

        * I eliminated tcs_ty_binds altogether. These were the bindings
          for unification variables that we have now solved by
          unification.  We kept them in a finite map and did the
          side-effecting unification later.  But in cannonicalisation we
          had to look up in the side-effected mutable tyvars anyway, so
          nothing was being gained.

          Our original idea was that the solver would be pure, and would
          be a no-op if you discarded its results, but this was already
          not-true for implications since we update their evidence
          bindings in an imperative way.  So rather than the uneasy
          compromise, it's now clearly imperative!

    * I split out the flatten/unflatten code into a new module, TcFlatten

    * I simplified and articulated explicitly the (rather hazy) invariants
      for the inert substitution inert_eqs.  See Note [eqCanRewrite] and
      See Note [Applying the inert substitution] in TcFlatten

    * Unflattening is now done (by TcFlatten.unflatten) after solveFlats,
      before solving nested implications.  This turned out to simplify a
      lot of code. Previously, unflattening was done as part of zonking, at
      the very very end.

        * Eager unflattening allowed me to remove the unpleasant ic_fsks
          field of an Implication (hurrah)

        * Eager unflattening made the TcSimplify.floatEqualities function
          much simpler (just float equalities looking like a ~ ty, where a
          is an untouchable meta-tyvar).

        * Likewise the idea of "pushing wanteds in as givens" could be
          completely eliminated.

    * I radically simplified the code that determines when there are
      'given' equalities, and hence whether we can float 'wanted' equalies
      out.  See TcSMonad.getNoGivenEqs, and Note [When does an implication
      have given equalities?].

      This allowed me to get rid of the unpleasant inert_no_eqs flag in InertCans.

    * As part of this given-equality stuff, I fixed Trac #9211. See Note
      [Let-bound skolems] in TcSMonad

    * Orientation of tyvar/tyvar equalities (a ~ b) was partly done during
      canonicalisation, but then repeated in the spontaneous-solve stage
      (trySpontaneousSolveTwoWay). Now it is done exclusively during
      canonicalisation, which keeps all the code in one place.  See
      Note [Canonical orientation for tyvar/tyvar equality constraints]
      in TcCanonical

>---------------------------------------------------------------

78a0fcb13046a86708d683350d844a77849f0ad5
 compiler/ghc.cabal.in               |    1 +
 compiler/typecheck/Flattening-notes |   13 +-
 compiler/typecheck/Inst.lhs         |   19 +-
 compiler/typecheck/TcCanonical.lhs  |  929 ++++++++-------------------
 compiler/typecheck/TcFlatten.lhs    | 1147 +++++++++++++++++++++++++++++++++
 compiler/typecheck/TcInteract.lhs   |  895 +++++++++++++-------------
 compiler/typecheck/TcMType.lhs      |  139 +---
 compiler/typecheck/TcRnTypes.lhs    |  185 +++---
 compiler/typecheck/TcRules.lhs      |    2 -
 compiler/typecheck/TcSMonad.lhs     | 1205 ++++++++++++++++++-----------------
 compiler/typecheck/TcSimplify.lhs   |  403 +++++-------
 compiler/typecheck/TcType.lhs       |  107 +++-
 compiler/typecheck/TcUnify.lhs      |    1 -
 13 files changed, 2835 insertions(+), 2211 deletions(-)

Diff suppressed because of size. To see it, use:

    git diff-tree --root --patch-with-stat --no-color --find-copies-harder --ignore-space-at-eol --cc 78a0fcb13046a86708d683350d844a77849f0ad5