Skip to content
  • Simon Peyton Jones's avatar
    Simon's major commit to re-engineer the constraint solver · 5770029a
    Simon Peyton Jones authored
    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
    5770029a