• Simon Peyton Jones's avatar
    Another major constraint-solver refactoring · 1eec1f21
    Simon Peyton Jones authored
    This patch takes further my refactoring of the constraint
    solver, which I've been doing over the last couple of months
    in consultation with Richard.
    
    It fixes a number of tricky bugs that made the constraint
    solver actually go into a loop, including
    
      Trac #12526
      Trac #12444
      Trac #12538
    
    The main changes are these
    
    * Flatten unification variables (fmvs/fuvs) appear on the LHS
      of a tvar/tyvar equality; thus
               fmv ~ alpha
      and not
               alpha ~ fmv
    
      See Note [Put flatten unification variables on the left]
      in TcUnify.  This is implemented by TcUnify.swapOverTyVars.
    
    * Don't reduce a "loopy" CFunEqCan where the fsk appears on
      the LHS:
          F t1 .. tn ~ fsk
      where 'fsk' is free in t1..tn.
      See Note [FunEq occurs-check principle] in TcInteract
    
      This neatly stops some infinite loops that people reported;
      and it allows us to delete some crufty code in reduce_top_fun_eq.
      And it appears to be no loss whatsoever.
    
      As well as fixing loops, ContextStack2 and T5837 both terminate
      when they didn't before.
    
    * Previously we generated "derived shadow" constraints from
      Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly
      generate a derived shadow from the same Wanted.
    
      A big change in this patch is to have two kinds of Wanteds:
         [WD] behaves like a pair of a Wanted and a Derived
         [W]  behaves like a Wanted only
      See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh
      field of a Wanted.
    
      This turned out to be a lot simpler.  A [WD] gets split into a
      [W] and a [D] in TcSMonad.maybeEmitShaodow.
    
      See TcSMonad Note [The improvement story and derived shadows]
    
    * Rather than have a separate inert_model in the InertCans, I've
      put the derived equalities back into inert_eqs.  We weren't
      gaining anything from a separate field.
    
    * Previously we had a mode for the constraint solver in which it
      would more aggressively solve Derived constraints; it was used
      for simplifying the context of a 'deriving' clause, or a 'default'
      delcaration, for example.
    
      But the complexity wasn't worth it; now I just make proper Wanted
      constraints.  See TcMType.cloneWC
    
    * Don't generate injectivity improvement for Givens; see
      Note [No FunEq improvement for Givens] in TcInteract
    
    * solveSimpleWanteds leaves the insolubles in-place rather than
      returning them.  Simpler.
    
    I also did lots of work on comments, including fixing Trac #12821.
    1eec1f21
TcSimplify.hs 88.8 KB