[commit: ghc] master: Fix a bug in occurs checking (66a8c19)

git at git.haskell.org git at git.haskell.org
Fri Sep 30 11:54:29 UTC 2016


Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/66a8c194520aadcaa0482736f3fdd4d2f31a5586/ghc

>---------------------------------------------------------------

commit 66a8c194520aadcaa0482736f3fdd4d2f31a5586
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Thu Sep 22 22:18:22 2016 +0100

    Fix a bug in occurs checking
    
    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.


>---------------------------------------------------------------

66a8c194520aadcaa0482736f3fdd4d2f31a5586
 compiler/typecheck/TcCanonical.hs                  | 154 ++---------
 compiler/typecheck/TcInteract.hs                   |  66 ++---
 compiler/typecheck/TcType.hs                       | 129 ++++++---
 compiler/typecheck/TcUnify.hs                      | 304 ++++++++++++---------
 testsuite/tests/polykinds/T12593.hs                |  14 +
 testsuite/tests/polykinds/T12593.stderr            |  31 +++
 testsuite/tests/polykinds/all.T                    |   1 +
 .../tests/typecheck/should_compile/tc141.stderr    |  10 +-
 testsuite/tests/typecheck/should_fail/T9605.stderr |   6 +-
 .../tests/typecheck/should_fail/tcfail122.stderr   |   2 +-
 10 files changed, 370 insertions(+), 347 deletions(-)

Diff suppressed because of size. To see it, use:

    git diff-tree --root --patch-with-stat --no-color --find-copies-harder --ignore-space-at-eol --cc 66a8c194520aadcaa0482736f3fdd4d2f31a5586


More information about the ghc-commits mailing list