Rework the handling of SkolemInfo

The main purpose of this patch is to attach a SkolemInfo directly to
each SkolemTv. This fixes the large number of bugs which have
accumulated over the years where we failed to report errors due to
having "no skolem info" for particular type variables. Now the origin of
each type varible is stored on the type variable we can always report
accurately where it cames from.

Fixes #20969 #20732 #20680 #19482 #20232 #19752 #10946
  #19760 #20063 #13499 #14040

The main changes of this patch are:

* SkolemTv now contains a SkolemInfo field which tells us how the
  SkolemTv was created. Used when reporting errors.

* Enforce invariants relating the SkolemInfoAnon and level of an implication (ic_info, ic_tclvl)
  to the SkolemInfo and level of the type variables in ic_skols.
    * All ic_skols are TcTyVars -- Check is currently disabled
    * All ic_skols are SkolemTv
    * The tv_lvl of the ic_skols agrees with the ic_tclvl
    * The ic_info agrees with the SkolInfo of the implication.

  These invariants are checked by a debug compiler by
  checkImplicationInvariants.

* Completely refactor kcCheckDeclHeader_sig which kept
  doing my head in. Plus, it wasn't right because it wasn't skolemising
  the binders as it decomposed the kind signature.

  The new story is described in Note [kcCheckDeclHeader_sig].  The code
  is considerably shorter than before (roughly 240 lines turns into 150
  lines).

  It still has the same awkward complexity around computing arity as
  before, but that is a language design issue.
  See Note [Arity inference in kcCheckDeclHeader_sig]

* I added new type synonyms MonoTcTyCon and PolyTcTyCon, and used
  them to be clear which TcTyCons have "finished" kinds etc, and
  which are monomorphic. See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]

* I renamed etaExpandAlgTyCon to splitTyConKind, becuase that's a
  better name, and it is very useful in kcCheckDeclHeader_sig, where
  eta-expansion isn't an issue.

* Kill off the nasty `ClassScopedTvEnv` entirely.

Co-authored-by: Simon Peyton Jones <simon.peytonjones@gmail.com>

1 files changed, 44 insertions, 26 deletions

diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 5319a52ad0..6a1f2d3315 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -1,4 +1,4 @@
-
+{-# LANGUAGE RecursiveDo #-}
 
 module GHC.Tc.Solver(
        InferMode(..), simplifyInfer, findInferredDiff,
@@ -59,6 +59,7 @@ import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.TcType
 import GHC.Core.Type
 import GHC.Core.Ppr
+import GHC.Core.TyCon    ( TyConBinder )
 import GHC.Builtin.Types ( liftedRepTy, manyDataConTy, liftedDataConTy )
 import GHC.Core.Unify    ( tcMatchTyKi )
 import GHC.Utils.Misc
@@ -164,17 +165,17 @@ simplifyTop wanteds
 
        ; return (evBindMapBinds binds1 `unionBags` binds2) }
 
-pushLevelAndSolveEqualities :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
+pushLevelAndSolveEqualities :: SkolemInfoAnon -> [TyConBinder] -> TcM a -> TcM a
 -- Push level, and solve all resulting equalities
 -- If there are any unsolved equalities, report them
 -- and fail (in the monad)
 --
 -- Panics if we solve any non-equality constraints.  (In runTCSEqualities
 -- we use an error thunk for the evidence bindings.)
-pushLevelAndSolveEqualities skol_info skol_tvs thing_inside
+pushLevelAndSolveEqualities skol_info_anon tcbs thing_inside
   = do { (tclvl, wanted, res) <- pushLevelAndSolveEqualitiesX
                                       "pushLevelAndSolveEqualities" thing_inside
-       ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
+       ; report_unsolved_equalities skol_info_anon (binderVars tcbs) tclvl wanted
        ; return res }
 
 pushLevelAndSolveEqualitiesX :: String -> TcM a
@@ -228,11 +229,11 @@ simplifyAndEmitFlatConstraints wanted
                          -- Emit the bad constraints, wrapped in an implication
                          -- See Note [Wrapping failing kind equalities]
                          ; tclvl  <- TcM.getTcLevel
-                         ; implic <- buildTvImplication UnkSkol [] (pushTcLevel tclvl) wanted
-                                    --                  ^^^^^^   |  ^^^^^^^^^^^^^^^^^
-                                    -- it's OK to use UnkSkol    |  we must increase the TcLevel,
-                                    -- because we don't bind     |  as explained in
-                                    -- any skolem variables here |  Note [Wrapping failing kind equalities]
+                         ; implic <- buildTvImplication unkSkolAnon [] (pushTcLevel tclvl) wanted
+                                        --                  ^^^^^^   |  ^^^^^^^^^^^^^^^^^
+                                        -- it's OK to use unkSkol    |  we must increase the TcLevel,
+                                        -- because we don't bind     |  as explained in
+                                        -- any skolem variables here |  Note [Wrapping failing kind equalities]
                          ; emitImplication implic
                          ; failM }
            Just (simples, holes)
@@ -461,13 +462,20 @@ reportUnsolvedEqualities :: SkolemInfo -> [TcTyVar] -> TcLevel
 --
 -- The provided SkolemInfo and [TcTyVar] arguments are used in an implication to
 -- provide skolem info for any errors.
---
 reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
+  = report_unsolved_equalities (getSkolemInfo skol_info) skol_tvs tclvl wanted
+
+report_unsolved_equalities :: SkolemInfoAnon -> [TcTyVar] -> TcLevel
+                           -> WantedConstraints -> TcM ()
+report_unsolved_equalities skol_info_anon skol_tvs tclvl wanted
   | isEmptyWC wanted
   = return ()
-  | otherwise
+
+  | otherwise  -- NB: we build an implication /even if skol_tvs is empty/,
+               -- just to ensure that our level invariants hold, specifically
+               -- (WantedInv).  See Note [TcLevel invariants].
   = checkNoErrs $   -- Fail
-    do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
+    do { implic <- buildTvImplication skol_info_anon skol_tvs tclvl wanted
        ; reportAllUnsolved (mkImplicWC (unitBag implic)) }
 
 
@@ -903,7 +911,7 @@ tcCheckGivens inerts given_ids = do
   (sat, new_inerts) <- runTcSInerts inerts $ do
     traceTcS "checkGivens {" (ppr inerts <+> ppr given_ids)
     lcl_env <- TcS.getLclEnv
-    let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
+    let given_loc = mkGivenLoc topTcLevel (getSkolemInfo unkSkol) lcl_env
     let given_cts = mkGivens given_loc (bagToList given_ids)
     -- See Note [Superclasses and satisfiability]
     solveSimpleGivens given_cts
@@ -1052,7 +1060,9 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                                    , pred <- sig_inst_theta sig ]
 
        ; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus)
-       ; qtkvs <- quantifyTyVars DefaultNonStandardTyVars dep_vars
+
+       ; skol_info <- mkSkolemInfo (InferSkol name_taus)
+       ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars dep_vars
        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
        ; return (qtkvs, [], emptyTcEvBinds, False) }
 
@@ -1104,10 +1114,16 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        -- NB: bound_theta are constraints we want to quantify over,
        --     including the psig_theta, which we always quantify over
        -- NB: bound_theta are fully zonked
-       ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl
+       ; rec { (qtvs, bound_theta, co_vars) <- decideQuantification skol_info infer_mode rhs_tclvl
                                                      name_taus partial_sigs
                                                      quant_pred_candidates
-       ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
+             ;  bound_theta_vars <- mapM TcM.newEvVar bound_theta
+
+             ; let full_theta = map idType bound_theta_vars
+             ; skol_info <- mkSkolemInfo (InferSkol [ (name, mkSigmaTy [] full_theta ty)
+                                                    | (name, ty) <- name_taus ])
+       }
+
 
        -- Now emit the residual constraint
        ; emitResidualConstraints rhs_tclvl ev_binds_var
@@ -1189,7 +1205,7 @@ findInferredDiff annotated_theta inferred_theta
     do { lcl_env   <- TcM.getLclEnv
        ; given_ids <- mapM TcM.newEvVar annotated_theta
        ; wanteds   <- newWanteds AnnOrigin inferred_theta
-       ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
+       ; let given_loc = mkGivenLoc topTcLevel (getSkolemInfo unkSkol) lcl_env
              given_cts = mkGivens given_loc given_ids
 
        ; residual <- runTcSDeriveds $
@@ -1332,7 +1348,8 @@ If the monomorphism restriction does not apply, then we quantify as follows:
 -}
 
 decideQuantification
-  :: InferMode
+  :: SkolemInfo
+  -> InferMode
   -> TcLevel
   -> [(Name, TcTauType)]   -- Variables to be generalised
   -> [TcIdSigInst]         -- Partial type signatures (if any)
@@ -1341,7 +1358,7 @@ decideQuantification
          , [PredType]      -- and this context (fully zonked)
          , VarSet)
 -- See Note [Deciding quantification]
-decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
+decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
   = do { -- Step 1: find the mono_tvs
        ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode
                                               name_taus psigs candidates
@@ -1351,7 +1368,7 @@ decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
        ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
 
        -- Step 3: decide which kind/type variables to quantify over
-       ; qtvs <- decideQuantifiedTyVars name_taus psigs candidates
+       ; qtvs <- decideQuantifiedTyVars skol_info name_taus psigs candidates
 
        -- Step 4: choose which of the remaining candidate
        --         predicates to actually quantify over
@@ -1436,7 +1453,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
 
        -- If possible, we quantify over partial-sig qtvs, so they are
        -- not mono. Need to zonk them because they are meta-tyvar TyVarTvs
-       ; psig_qtvs <- mapM zonkTcTyVarToTyVar $ binderVars $
+       ; psig_qtvs <-  zonkTcTyVarsToTcTyVars $ binderVars $
                       concatMap (map snd . sig_inst_skols) psigs
 
        ; psig_theta <- mapM TcM.zonkTcType $
@@ -1587,12 +1604,13 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
 
 ------------------
 decideQuantifiedTyVars
-   :: [(Name,TcType)]   -- Annotated theta and (name,tau) pairs
+   :: SkolemInfo
+   -> [(Name,TcType)]   -- Annotated theta and (name,tau) pairs
    -> [TcIdSigInst]     -- Partial signatures
    -> [PredType]        -- Candidates, zonked
    -> TcM [TyVar]
 -- Fix what tyvars we are going to quantify over, and quantify them
-decideQuantifiedTyVars name_taus psigs candidates
+decideQuantifiedTyVars skol_info name_taus psigs candidates
   = do {     -- Why psig_tys? We try to quantify over everything free in here
              -- See Note [Quantification and partial signatures]
              --     Wrinkles 2 and 3
@@ -1631,7 +1649,7 @@ decideQuantifiedTyVars name_taus psigs candidates
            , text "grown_tcvs =" <+> ppr grown_tcvs
            , text "dvs =" <+> ppr dvs_plus])
 
-       ; quantifyTyVars DefaultNonStandardTyVars dvs_plus }
+       ; quantifyTyVars skol_info DefaultNonStandardTyVars dvs_plus }
 
 ------------------
 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
@@ -2192,7 +2210,7 @@ checkBadTelescope (Implic { ic_info  = info
       | otherwise
       = go (later_skols `extendVarSet` one_skol) earlier_skols
 
-warnRedundantGivens :: SkolemInfo -> Bool
+warnRedundantGivens :: SkolemInfoAnon -> Bool
 warnRedundantGivens (SigSkol ctxt _ _)
   = case ctxt of
        FunSigCtxt _ rrc -> reportRedundantConstraints rrc
@@ -2835,7 +2853,7 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
       | Just subst <- mb_subst
       = do { lcl_env <- TcS.getLclEnv
            ; tc_lvl <- TcS.getTcLevel
-           ; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env
+           ; let loc = mkGivenLoc tc_lvl (getSkolemInfo unkSkol) lcl_env
            -- Equality constraints are possible due to type defaulting plugins
            ; wanted_evs <- mapM (newWantedNC loc . substTy subst . ctPred)
                                 wanteds