[GHC] #12526: regression in type inference with respect to type families

[GHC]

#12526: regression in type inference with respect to type families
-------------------------------------+-------------------------------------
        Reporter:  Lemming           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #10634            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

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

 In [changeset:"1eec1f21268af907f59b5d5c071a9a25de7369c7/ghc"
 1eec1f21/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="1eec1f21268af907f59b5d5c071a9a25de7369c7"
 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, including fixing Trac #12821.
 }}}

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