Constraint solver again

[Simon Peyton Jones]

Richard,

I’ve taken another run at the constraint solver.   It’s on wip/spj-tc-branch3 (you’ll need a forced update).

I think I can safely commit it to HEAD in the light of your earlier comments, so I’ll do that soon, but I thought I’d just give you (and other ghc-devs) a heads-up.

The two main commits are below.  The former is small; the latter is the main event.

Simon



commit 570c3181342386b5cee1862f85a8ebed7d98d712

Author: Simon Peyton Jones <simonpj at microsoft.com>

Date:   Wed Nov 23 16:00:00 2016 +0000



    Allow TyVars in TcTypes



    Up to now we've had a rule that a TyVar can't apppear in a type

    seen by the type checker; they should all be TcTyVars.  But:



    a) With -XTypeInType it becomes much harder to exclude them;

       see Note [TcTyVars in the typechecker] in TcType.



    b) It's unnecessary to exculde them; instead we can just treat

       a TyVar just like vanillaSkolemTv.



    This is what was causing an ASSERT error in

    indexed-types/should_fail/T12041, reported in Trac #12826.



    That patch allows a TyVar in a TcType.  The most significant

    change is to make Var.tcTyVarDetails return vanillaSkolemTv.

    In fact it already did, but (a) it was not documented, and

    (b) we never exploited it.  Now we rely on it.



commit 6e6d93b8b713339dc5f74e8f93e35d0d94014d63

Author: Simon Peyton Jones <simonpj at microsoft.com>

Date:   Tue Oct 25 17:41:45 2016 +0100



    Another major constraint-solver refactoring



    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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20161124/620b26b7/attachment-0001.html>