[GHC] #9211: Untouchable type variable (regression from 7.6)

[GHC]

#9211: Untouchable type variable (regression from 7.6)
-------------------------------------+-------------------------------------
              Reporter:  simonpj     |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.2
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"5770029a1f8509a673b2277287fc8fe90b9b6002/ghc"]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="5770029a1f8509a673b2277287fc8fe90b9b6002"
 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
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9211#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler