[commit: ghc] master: Fix the TcLevel not being set correctly when finding valid hole fits (b202e7a)

[git at git.haskell.org]

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

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

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

commit b202e7a48401bd8e805a92dcfe5ea059cbd8e41c
Author: Matthías Páll Gissurarson <mpg at mpg.is>
Date:   Sat Jul 21 15:48:53 2018 +0200

    Fix the TcLevel not being set correctly when finding valid hole fits
    
    Summary:
    This fixes the problem revealed by a new assert as it relates to valid
    hole fits. However, tests `T10384`, `T14040a` and `TcStaticPointersFail02`
    still fail the assert, but they are unrelated to valid hole fits.
    
    Reviewers: bgamari, simonpj
    
    Reviewed By: simonpj
    
    Subscribers: simonpj, rwbarton, thomie, carter
    
    GHC Trac Issues: #15384
    
    Differential Revision: https://phabricator.haskell.org/D4994


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

b202e7a48401bd8e805a92dcfe5ea059cbd8e41c
 compiler/typecheck/TcHoleErrors.hs | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

diff --git a/compiler/typecheck/TcHoleErrors.hs b/compiler/typecheck/TcHoleErrors.hs
index 16429fb..173abbd 100644
--- a/compiler/typecheck/TcHoleErrors.hs
+++ b/compiler/typecheck/TcHoleErrors.hs
@@ -29,7 +29,7 @@ import FV ( fvVarList, fvVarSet, unionFV, mkFVs, FV )
 import Control.Arrow ( (&&&) )
 
 import Control.Monad    ( filterM, replicateM )
-import Data.List        ( partition, sort, sortOn, nubBy, foldl' )
+import Data.List        ( partition, sort, sortOn, nubBy )
 import Data.Graph       ( graphFromEdges, topSort )
 import Data.Function    ( on )
 
@@ -700,19 +700,17 @@ findValidHoleFits tidy_env implics simples ct | isExprHoleCt ct =
     isFlexiTyVar tv | isMetaTyVar tv = isFlexi <$> readMetaTyVar tv
     isFlexiTyVar _ = return False
 
-    -- Takes a list of free variables and makes sure that the given action
-    -- is run with the right TcLevel and restores any Flexi type
-    -- variables after the action is run.
+    -- Takes a list of free variables and restores any Flexi type variables
+    -- in free_vars after the action is run.
     withoutUnification :: FV -> TcM a -> TcM a
     withoutUnification free_vars action
       = do { flexis <- filterM isFlexiTyVar fuvs
-            ; result <- setTcLevel deepestFreeTyVarLvl action
+            ; result <- action
               -- Reset any mutated free variables
             ; mapM_ restore flexis
             ; return result }
       where restore = flip writeTcRef Flexi . metaTyVarRef
             fuvs = fvVarList free_vars
-            deepestFreeTyVarLvl = foldl' max topTcLevel $ map tcTyVarLevel fuvs
 
     -- The real work happens here, where we invoke the type checker using
     -- tcCheckHoleFit to see whether the given type fits the hole.
@@ -931,13 +929,25 @@ tcSubsumes ty_a ty_b = fst <$> tcCheckHoleFit emptyBag [] ty_a ty_b
 -- free type variables to avoid side-effects.
 tcCheckHoleFit :: Cts                   -- Any relevant Cts to the hole.
                -> [Implication]         -- The nested implications of the hole
+                                        -- with the innermost implication first
                -> TcSigmaType           -- The type of the hole.
                -> TcSigmaType           -- The type to check whether fits.
                -> TcM (Bool, HsWrapper)
 tcCheckHoleFit _ _ hole_ty ty | hole_ty `eqType` ty
     = return (True, idHsWrapper)
 tcCheckHoleFit relevantCts implics hole_ty ty = discardErrs $
-  do { (wrp, wanted) <- captureConstraints $ tcSubType_NC ExprSigCtxt ty hole_ty
+  do { -- We wrap the subtype constraint in the implications to pass along the
+       -- givens, and so we must ensure that any nested implications and skolems
+       -- end up with the correct level. The implications are ordered so that
+       -- the innermost (the one with the highest level) is first, so it
+       -- suffices to get the level of the first one (or the current level, if
+       -- there are no implications involved).
+       innermost_lvl <- case implics of
+                          [] -> getTcLevel
+                          -- imp is the innermost implication
+                          (imp:_) -> return (ic_tclvl imp)
+     ; (wrp, wanted) <- setTcLevel innermost_lvl $ captureConstraints $
+                          tcSubType_NC ExprSigCtxt ty hole_ty
      ; traceTc "Checking hole fit {" empty
      ; traceTc "wanteds are: " $ ppr wanted
      -- We add the relevantCts to the wanteds generated by the call to