• Simon Peyton Jones's avatar
    Improve kick-out in the constraint solver · 3acd6164
    Simon Peyton Jones authored
    This patch was provoked by Trac #14363.  Turned out that we were
    kicking out too many constraints in TcSMonad.kickOutRewritable, and
    that mean that the work-list never became empty: infinite loop!
    That in turn made me look harder at the Main Theorem in
    Note [Extending the inert equalities].
    Main changes
    * Replace TcType.isTyVarExposed by TcType.isTyVarHead.  The
      over-agressive isTyVarExposed is what caused Trac #14363.
      See Note [K3: completeness of solving] in TcSMonad.
    * TcType.Make anyRewriteableTyVar role-aware.  In particular,
          a ~R ty
      cannot rewrite
          b ~R f a
      See Note [anyRewriteableTyVar must be role-aware].  That means
      it has to be given a role argument, which forces a little
      I think this change is fixing a bug that hasn't yet been reported.
      The actual reported bug is handled by the previous bullet.  But
      this change is definitely the Right Thing
    The main changes are in TcSMonad.kick_out_rewritable, and in TcType
    (isTyVarExposed ---> isTyVarHead).
    I did a little unforced refactoring:
     * Use the cc_eq_rel field of a CTyEqCan when it is available, rather
       than recomputing it.
     * Define eqCanRewrite :: EqRel -> EqRel -> EqRel, and use it, instead
       of duplicating its logic
TcType.hs 102 KB