Skip to content
  • Simon Peyton Jones's avatar
    Fix a number of subtle solver bugs · 9308c736
    Simon Peyton Jones authored
    As a result of some other unrelated changes I found that
    IndTypesPerf was failing, and opened Trac #11408.  There's
    a test in indexed-types/should-compile/T11408.
    
    The bug was that a type like
     forall t. (MT (UL t) (UR t) ~ t) => UL t -> UR t -> Int
    is in fact unambiguous, but it's a bit subtle to prove
    that it is unambiguous.
    
    In investigating, Dimitrios and I found several subtle
    bugs in the constraint solver, fixed by this patch
    
    * canRewrite was missing a Derived/Derived case.  This was
      lost by accident in Richard's big kind-equality patch.
    
    * Interact.interactTyVarEq would discard [D] a ~ ty if there
      was a [W] a ~ ty in the inert set.  But that is wrong because
      the former can rewrite things that the latter cannot.
      Fix: a new function eqCanDischarge
    
    * In TcSMonad.addInertEq, the process was outright wrong for
      a Given/Wanted in the (GWModel) case.  We were adding a new
      Derived without kicking out things that it could rewrite.
      Now the code is simpler (no special GWModel case), and works
      correctly.
    
    * The special case in kickOutRewritable for [W] fsk ~ ty,
      turns out not to be needed.  (We emit a [D] fsk ~ ty which
      will do the job.
    
    I improved comments and documentation, esp in TcSMonad.
    9308c736