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

(cherry picked from commit b202e7a4)

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 )
 
@@ -661,19 +661,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.
@@ -891,13 +889,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
      ; if isEmptyWC wanted && isEmptyBag relevantCts