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>

2 files changed, 18 insertions, 15 deletions

diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index db1c3c1652..b7c702e5b9 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -872,13 +872,13 @@ solveForAll ev tvs theta pred pend_sc
   | CtWanted { ctev_dest = dest } <- ev
   = -- See Note [Solving a Wanted forall-constraint]
     setLclEnv (ctLocEnv loc) $
-       -- This setLclEnv is important: the emitImplicationTcS uses that
-       -- TcLclEnv for the implication, and that in turn sets the location
-       -- for the Givens when solving the constraint (#21006)
-    do { let skol_info = QuantCtxtSkol
-             empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
+    -- This setLclEnv is important: the emitImplicationTcS uses that
+    -- TcLclEnv for the implication, and that in turn sets the location
+    -- for the Givens when solving the constraint (#21006)
+    do { skol_info <- mkSkolemInfo QuantCtxtSkol
+       ; let empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
                            tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
-       ; (subst, skol_tvs) <- tcInstSkolTyVarsX empty_subst tvs
+       ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
        ; given_ev_vars <- mapM newEvVar (substTheta subst theta)
 
        ; (lvl, (w_id, wanteds))
@@ -888,7 +888,7 @@ solveForAll ev tvs theta pred pend_sc
                    ; return ( ctEvEvId wanted_ev
                             , unitBag (mkNonCanonical wanted_ev)) }
 
-      ; ev_binds <- emitImplicationTcS lvl skol_info skol_tvs
+      ; ev_binds <- emitImplicationTcS lvl (getSkolemInfo skol_info) skol_tvs
                                        given_ev_vars wanteds
 
       ; setWantedEvTerm dest $
@@ -1352,11 +1352,11 @@ can_eq_nc_forall ev eq_rel s1 s2
         else
    do { traceTcS "Creating implication for polytype equality" $ ppr ev
       ; let empty_subst1 = mkEmptyTCvSubst $ mkInScopeSet free_tvs
-      ; (subst1, skol_tvs) <- tcInstSkolTyVarsX empty_subst1 $
+      ; skol_info <- mkSkolemInfo (UnifyForAllSkol phi1)
+      ; (subst1, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst1 $
                               binderVars bndrs1
 
-      ; let skol_info = UnifyForAllSkol phi1
-            phi1' = substTy subst1 phi1
+      ; let phi1' = substTy subst1 phi1
 
             -- Unify the kinds, extend the substitution
             go :: [TcTyVar] -> TCvSubst -> [TyVarBinder]
@@ -1384,7 +1384,7 @@ can_eq_nc_forall ev eq_rel s1 s2
 
       ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $
                                     go skol_tvs empty_subst2 bndrs2
-      ; emitTvImplicationTcS lvl skol_info skol_tvs wanteds
+      ; emitTvImplicationTcS lvl (getSkolemInfo skol_info) skol_tvs wanteds
 
       ; setWantedEq orig_dest all_co
       ; stopWith ev "Deferred polytype equality" } }
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 25bde37642..963768ca47 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -1228,6 +1228,9 @@ instance Monad TcS where
   m >>= k   = mkTcS $ \ebs -> do
     unTcS m ebs >>= (\r -> unTcS (k r) ebs)
 
+instance MonadIO TcS where
+  liftIO act = TcS $ \_env -> liftIO act
+
 instance MonadFail TcS where
   fail err  = mkTcS $ \_ -> fail err
 
@@ -1503,7 +1506,7 @@ nestTcS (TcS thing_inside)
 
        ; return res }
 
-emitImplicationTcS :: TcLevel -> SkolemInfo
+emitImplicationTcS :: TcLevel -> SkolemInfoAnon
                    -> [TcTyVar]        -- Skolems
                    -> [EvVar]          -- Givens
                    -> Cts              -- Wanteds
@@ -1524,7 +1527,7 @@ emitImplicationTcS new_tclvl skol_info skol_tvs givens wanteds
        ; emitImplication imp
        ; return (TcEvBinds (ic_binds imp)) }
 
-emitTvImplicationTcS :: TcLevel -> SkolemInfo
+emitTvImplicationTcS :: TcLevel -> SkolemInfoAnon
                      -> [TcTyVar]        -- Skolems
                      -> Cts              -- Wanteds
                      -> TcS ()
@@ -2001,8 +2004,8 @@ matchGlobalInst :: DynFlags
 matchGlobalInst dflags short_cut cls tys
   = wrapTcS (TcM.matchGlobalInst dflags short_cut cls tys)
 
-tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
-tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs
+tcInstSkolTyVarsX :: SkolemInfo -> TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
+tcInstSkolTyVarsX skol_info subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX skol_info subst tvs
 
 -- Creating and setting evidence variables and CtFlavors
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~