[commit: ghc] wip/spj-temp: Fix a bug in occurs checking (f3832cf)

[git at git.haskell.org]

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

On branch  : wip/spj-temp
Link       : http://ghc.haskell.org/trac/ghc/changeset/f3832cfb347a1359a91c5b30ebb4eb7d94dc3f0d/ghc

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

commit f3832cfb347a1359a91c5b30ebb4eb7d94dc3f0d
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 #1593 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.


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

f3832cfb347a1359a91c5b30ebb4eb7d94dc3f0d
 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 +-
 utils/haddock                                      |   2 +-
 11 files changed, 371 insertions(+), 348 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 f3832cfb347a1359a91c5b30ebb4eb7d94dc3f0d