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, 77 insertions, 45 deletions

diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 0fc6407da4..edd4b127ee 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -7,6 +7,9 @@
 module GHC.Tc.Errors.Ppr
   ( pprTypeDoesNotHaveFixedRuntimeRep
   , pprScopeError
+  --
+  , tidySkolemInfo
+  , tidySkolemInfoAnon
   )
   where
 
@@ -74,6 +77,8 @@ import Data.Function (on)
 import Data.List ( groupBy, sortBy, tails
                  , partition, unfoldr )
 import Data.Ord ( comparing )
+import Data.Bifunctor
+import GHC.Types.Name.Env
 
 
 instance Diagnostic TcRnMessage where
@@ -2117,9 +2122,9 @@ pprTcReportInfo _ (Ambiguity prepend_msg (ambig_kvs, ambig_tvs)) = msg
       | otherwise -- "The type variable 't0' is ambiguous"
       = text "The" <+> what <+> text "variable" <> plural tkvs
         <+> pprQuotedList tkvs <+> isOrAre tkvs <+> text "ambiguous"
-pprTcReportInfo ctxt (TyVarInfo tv) =
+pprTcReportInfo ctxt (TyVarInfo tv ) =
   case tcTyVarDetails tv of
-    SkolemTv {}   -> pprSkols ctxt [tv]
+    SkolemTv sk_info _ _   -> pprSkols ctxt [(getSkolemInfo sk_info, [tv])]
     RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem"
     MetaTv {}     -> empty
 pprTcReportInfo _ (NonInjectiveTyFam tc) =
@@ -2210,7 +2215,7 @@ pprHoleError _ (Hole { hole_ty, hole_occ = occ }) (OutOfScopeHole imp_errs)
       | boring_type = hang herald 2 (ppr occ)
       | otherwise   = hang herald 2 (pp_occ_with_type occ hole_ty)
     boring_type = isTyVarTy hole_ty
-pprHoleError ctxt (Hole { hole_ty, hole_occ }) (HoleError sort) =
+pprHoleError ctxt (Hole { hole_ty, hole_occ}) (HoleError sort other_tvs hole_skol_info) =
   vcat [ hole_msg
        , tyvars_msg
        , case sort of { ExprHole {} -> expr_hole_hint; _ -> type_hole_hint } ]
@@ -2241,10 +2246,7 @@ pprHoleError ctxt (Hole { hole_ty, hole_occ }) (HoleError sort) =
     tyvars = tyCoVarsOfTypeList hole_ty
     tyvars_msg = ppUnless (null tyvars) $
                  text "Where:" <+> (vcat (map loc_msg other_tvs)
-                                    $$ pprSkols ctxt skol_tvs)
-       where
-         (skol_tvs, other_tvs) = partition is_skol tyvars
-         is_skol tv = isTcTyVar tv && isSkolemTyVar tv
+                                    $$ pprSkols ctxt hole_skol_info)
                       -- Coercion variables can be free in the
                       -- hole, via kind casts
     expr_hole_hint                       -- Give hint for, say,   f x = _x
@@ -2379,7 +2381,7 @@ ctxtFixes has_ambig_tvs pred implics
     ppr_skol (PatSkol (PatSynCon ps)   _) = text "the pattern synonym"  <+> quotes (ppr ps)
     ppr_skol skol_info = ppr skol_info
 
-usefulContext :: [Implication] -> PredType -> [SkolemInfo]
+usefulContext :: [Implication] -> PredType -> [SkolemInfoAnon]
 -- usefulContext picks out the implications whose context
 -- the programmer might plausibly augment to solve 'pred'
 usefulContext implics pred
@@ -2464,15 +2466,67 @@ pprWithArising (ct:cts)
 *                                                                      *
 **********************************************************************-}
 
-pprSkols :: ReportErrCtxt -> [TcTyVar] -> SDoc
-pprSkols ctxt tvs
-  = vcat (map pp_one (getSkolemInfo (cec_encl ctxt) tvs))
+
+tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
+tidySkolemInfo env (SkolemInfo u sk_anon) = SkolemInfo u (tidySkolemInfoAnon env sk_anon)
+
+----------------
+tidySkolemInfoAnon :: TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon
+tidySkolemInfoAnon env (DerivSkol ty)         = DerivSkol (tidyType env ty)
+tidySkolemInfoAnon env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
+tidySkolemInfoAnon env (InferSkol ids)        = InferSkol (mapSnd (tidyType env) ids)
+tidySkolemInfoAnon env (UnifyForAllSkol ty)   = UnifyForAllSkol (tidyType env ty)
+tidySkolemInfoAnon _   info                   = info
+
+tidySigSkol :: TidyEnv -> UserTypeCtxt
+            -> TcType -> [(Name,TcTyVar)] -> SkolemInfoAnon
+-- We need to take special care when tidying SigSkol
+-- See Note [SigSkol SkolemInfo] in "GHC.Tc.Types.Origin"
+tidySigSkol env cx ty tv_prs
+  = SigSkol cx (tidy_ty env ty) tv_prs'
+  where
+    tv_prs' = mapSnd (tidyTyCoVarOcc env) tv_prs
+    inst_env = mkNameEnv tv_prs'
+
+    tidy_ty env (ForAllTy (Bndr tv vis) ty)
+      = ForAllTy (Bndr tv' vis) (tidy_ty env' ty)
+      where
+        (env', tv') = tidy_tv_bndr env tv
+
+    tidy_ty env ty@(FunTy InvisArg w arg res) -- Look under  c => t
+      = ty { ft_mult = tidy_ty env w,
+             ft_arg = tidyType env arg,
+             ft_res = tidy_ty env res }
+
+    tidy_ty env ty = tidyType env ty
+
+    tidy_tv_bndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
+    tidy_tv_bndr env@(occ_env, subst) tv
+      | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
+      = ((occ_env, extendVarEnv subst tv tv'), tv')
+
+      | otherwise
+      = tidyVarBndr env tv
+
+pprSkols :: ReportErrCtxt -> [(SkolemInfoAnon, [TcTyVar])] -> SDoc
+pprSkols ctxt zonked_ty_vars
+  =
+      let tidy_ty_vars = map (bimap (tidySkolemInfoAnon (cec_tidy ctxt)) id) zonked_ty_vars
+      in vcat (map pp_one tidy_ty_vars)
   where
-    pp_one (UnkSkol, tvs)
+
+    no_msg = text "No skolem info - we could not find the origin of the following variables" <+> ppr zonked_ty_vars
+       $$ text "This should not happen, please report it as a bug following the instructions at:"
+       $$ text "https://gitlab.haskell.org/ghc/ghc/wikis/report-a-bug"
+
+
+    pp_one (UnkSkol cs, tvs)
       = vcat [ hang (pprQuotedList tvs)
                  2 (is_or_are tvs "a" "(rigid, skolem)")
              , nest 2 (text "of unknown origin")
-             , nest 2 (text "bound at" <+> ppr (foldr1 combineSrcSpans (map getSrcSpan tvs)))
+             , nest 2 (text "bound at" <+> ppr (skolsSpan tvs))
+             , no_msg
+             , prettyCallStackDoc cs
              ]
     pp_one (RuntimeUnkSkol, tvs)
       = hang (pprQuotedList tvs)
@@ -2481,13 +2535,16 @@ pprSkols ctxt tvs
       = vcat [ hang (pprQuotedList tvs)
                   2 (is_or_are tvs "a"  "rigid" <+> text "bound by")
              , nest 2 (pprSkolInfo skol_info)
-             , nest 2 (text "at" <+> ppr (foldr1 combineSrcSpans (map getSrcSpan tvs))) ]
+             , nest 2 (text "at" <+> ppr (skolsSpan tvs)) ]
 
     is_or_are [_] article adjective = text "is" <+> text article <+> text adjective
                                       <+> text "type variable"
     is_or_are _   _       adjective = text "are" <+> text adjective
                                       <+> text "type variables"
 
+skolsSpan :: [TcTyVar] -> SrcSpan
+skolsSpan skol_tvs = foldr1 combineSrcSpans (map getSrcSpan skol_tvs)
+
 {- *********************************************************************
 *                                                                      *
                 Utilities for expected/actual messages
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index d05a2cc6da..04b3acefa0 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -35,7 +35,7 @@ module GHC.Tc.Errors.Types (
   , SolverReport(..), SolverReportSupplementary(..)
   , ReportWithCtxt(..)
   , ReportErrCtxt(..)
-  , getUserGivens, discardProvCtxtGivens, getSkolemInfo
+  , getUserGivens, discardProvCtxtGivens
   , TcReportMsg(..), TcReportInfo(..)
   , CND_Extra(..)
   , mkTcReportWithInfo
@@ -57,9 +57,9 @@ import {-# SOURCE #-} GHC.Tc.Types (TcIdSigInfo)
 import {-# SOURCE #-} GHC.Tc.Errors.Hole.FitTypes (HoleFit)
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Evidence (EvBindsVar)
-import GHC.Tc.Types.Origin (CtOrigin (ProvCtxtOrigin), TypedThing, TyVarBndrs, SkolemInfo (SigSkol, UnkSkol, RuntimeUnkSkol), FRROrigin, UserTypeCtxt (PatSynCtxt))
+import GHC.Tc.Types.Origin (CtOrigin (ProvCtxtOrigin), SkolemInfoAnon (SigSkol), UserTypeCtxt (PatSynCtxt), TyVarBndrs, TypedThing, FRROrigin)
 import GHC.Tc.Types.Rank (Rank)
-import GHC.Tc.Utils.TcType (TcType, isRuntimeUnkSkol)
+import GHC.Tc.Utils.TcType (TcType)
 import GHC.Types.Error
 import GHC.Types.FieldLabel (FieldLabelString)
 import GHC.Types.Name (Name, OccName, getSrcLoc)
@@ -83,13 +83,11 @@ import GHC.Unit.State (UnitState)
 import GHC.Unit.Module.Name (ModuleName)
 import GHC.Types.Basic
 import GHC.Utils.Misc (filterOut)
-import GHC.Utils.Trace (pprTraceUserWarning)
 import qualified GHC.LanguageExtensions as LangExt
 
 import qualified Data.List.NonEmpty as NE
 import           Data.Typeable hiding (TyCon)
 import qualified Data.Semigroup as Semigroup
-import Data.List (partition)
 
 {-
 Note [Migrating TcM Messages]
@@ -188,7 +186,7 @@ data TcRnMessage where
 
       Test cases: T9939, T10632, T18036a, T20602, PluralS, T19296.
   -}
-  TcRnRedundantConstraints :: [Id] -> (SkolemInfo, Bool) -> TcRnMessage
+  TcRnRedundantConstraints :: [Id] -> (SkolemInfoAnon, Bool) -> TcRnMessage
 
   {-| TcRnInaccessibleCode is a warning that is emitted when the RHS of a pattern
       match is inaccessible, because the constraint solver has detected a contradiction.
@@ -1979,31 +1977,6 @@ discardProvCtxtGivens orig givens  -- See Note [discardProvCtxtGivens]
     discard _ _                                                  = False
 
 
-getSkolemInfo :: [Implication] -> [TcTyVar]
-              -> [(SkolemInfo, [TcTyVar])]                    -- #14628
--- Get the skolem info for some type variables
--- from the implication constraints that bind them.
---
--- In the returned (skolem, tvs) pairs, the 'tvs' part is non-empty
-getSkolemInfo _ []
-  = []
-
-getSkolemInfo [] tvs
-  | all isRuntimeUnkSkol tvs = [(RuntimeUnkSkol, tvs)]        -- #14628
-  | otherwise = -- See https://gitlab.haskell.org/ghc/ghc/-/issues?label_name[]=No%20skolem%20info
-      pprTraceUserWarning msg [(UnkSkol,tvs)]
-  where
-    msg = text "No skolem info - we could not find the origin of the following variables" <+> ppr tvs
-       $$ text "This should not happen, please report it as a bug following the instructions at:"
-       $$ text "https://gitlab.haskell.org/ghc/ghc/wikis/report-a-bug"
-
-
-getSkolemInfo (implic:implics) tvs
-  | null tvs_here =                            getSkolemInfo implics tvs
-  | otherwise   = (ic_info implic, tvs_here) : getSkolemInfo implics tvs_other
-  where
-    (tvs_here, tvs_other) = partition (`elem` ic_skols implic) tvs
-
 -- | An error reported after constraint solving.
 -- This is usually, some sort of unsolved constraint error,
 -- but we try to be specific about the precise problem we encountered.
@@ -2313,6 +2286,8 @@ data HoleError
   = OutOfScopeHole [ImportError]
   -- | Report a typed hole, or wildcard, with additional information.
   | HoleError HoleSort
+              [TcTyVar]                     -- Other type variables which get computed on the way.
+              [(SkolemInfoAnon, [TcTyVar])] -- Zonked and grouped skolems for the type of the hole.
 
 -- | A message that aims to explain why two types couldn't be seen
 -- to be representationally equal.