• Simon Peyton Jones's avatar
    Fix a bug in occurs checking · 66a8c194
    Simon Peyton Jones authored
    1. Trac #12593 exposed a long-standing bug in the occurs
       checking machinery.  When unifying two type variables
              a ~ b
       where a /= b, we were assuming that there could be
       no occurs-check error.  But there can: 'a' can occur
       in b's kind!  When the RHS was a non-tyvar we used
       occurCheckExpand, which /did/ look in kinds, but not
       when the RHS was a tyvar.
    
       This bug has been lurking ever since TypeInType, maybe
       longer.  And it was present both in TcUnify (the on-the-fly
       unifier), and in TcInteract.
    
       I ended up refactoring both so that the tyvar/tyvar
       path naturally goes through the same occurs-check as
       non-tyvar rhss.  It's simpler and more robust now.
    
       One good thing is that both unifiers now share
           TcType.swapOverVars
           TcType.canSolveByUnification
       previously they had different logic for the same goals
    
    2. Fixing this bug exposed another!  In T11635 we end
       up unifying
       (alpha :: forall k. k->*) ~ (beta :: forall k. k->*)
       Now that the occurs check is done for tyvars too, we
       look inside beta's kind.  And then reject the program
       becuase of the forall inside there.  But in fact that
       forall is fine -- it does not count as impredicative
       polymoprhism.   See Note [Checking for foralls]
       in TcType.
    
    3. All this fuss around occurrence checking forced me
       to look at TcUnify.checkTauTvUpdate
              and TcType.occurCheckExpand
       There's a lot of duplication there, and I managed
       to elminate quite a bit of it. For example,
       checkTauTvUpdate called a local 'defer_me'; and then
       called occurCheckExpand, which then used a very
       similar 'fast_check'.
    
       Things are better, but there is more to do.
    66a8c194
tc141.stderr 1.75 KB