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.
Showing
- compiler/typecheck/TcCanonical.hs 27 additions, 127 deletionscompiler/typecheck/TcCanonical.hs
- compiler/typecheck/TcInteract.hs 23 additions, 43 deletionscompiler/typecheck/TcInteract.hs
- compiler/typecheck/TcType.hs 94 additions, 35 deletionscompiler/typecheck/TcType.hs
- compiler/typecheck/TcUnify.hs 171 additions, 133 deletionscompiler/typecheck/TcUnify.hs
- testsuite/tests/polykinds/T12593.hs 14 additions, 0 deletionstestsuite/tests/polykinds/T12593.hs
- testsuite/tests/polykinds/T12593.stderr 31 additions, 0 deletionstestsuite/tests/polykinds/T12593.stderr
- testsuite/tests/polykinds/all.T 1 addition, 0 deletionstestsuite/tests/polykinds/all.T
- testsuite/tests/typecheck/should_compile/tc141.stderr 5 additions, 5 deletionstestsuite/tests/typecheck/should_compile/tc141.stderr
- testsuite/tests/typecheck/should_fail/T9605.stderr 3 additions, 3 deletionstestsuite/tests/typecheck/should_fail/T9605.stderr
- testsuite/tests/typecheck/should_fail/tcfail122.stderr 1 addition, 1 deletiontestsuite/tests/typecheck/should_fail/tcfail122.stderr
Loading
Please register or sign in to comment