Improve kind generalisation, error messages

This patch does two things:

* It refactors GHC.Tc.Errors a bit.  In debugging Quick Look I was
  forced to look in detail at error messages, and ended up doing a bit
  of refactoring, esp in mkTyVarEqErr'.  It's still quite a mess, but
  a bit better, I think.

* It makes a significant improvement to the kind checking of type and
  class declarations. Specifically, we now ensure that if kind
  checking fails with an unsolved constraint, all the skolems are in
  scope.  That wasn't the case before, which led to some obscure error
  messages; and occasional failures with "no skolem info" (eg #16245).

Both of these, and the main Quick Look patch itself, affect a /lot/ of
error messages, as you can see from the number of files changed.  I've
checked them all; I think they are as good or better than before.

Smaller things

* I documented the various instances of VarBndr better.
  See Note [The VarBndr tyep and its uses] in GHC.Types.Var

* Renamed GHC.Tc.Solver.simpl_top to simplifyTopWanteds

* A bit of refactoring in bindExplicitTKTele, to avoid the
  footwork with Either.  Simpler now.

* Move promoteTyVar from GHC.Tc.Solver to GHC.Tc.Utils.TcMType

Fixes #16245 (comment 211369), memorialised as
  typecheck/polykinds/T16245a
Also fixes the three bugs in #18640

1 files changed, 44 insertions, 28 deletions

diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index d597c95b72..93c047ca32 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -69,7 +69,7 @@ import GHC.Utils.FV ( fvVarList, unionFV )
 
 import Control.Monad    ( when )
 import Data.Foldable    ( toList )
-import Data.List        ( partition, mapAccumL, nub, sortBy, unfoldr )
+import Data.List        ( partition, mapAccumL, sortBy, unfoldr )
 
 import {-# SOURCE #-} GHC.Tc.Errors.Hole ( findValidHoleFits )
 
@@ -215,7 +215,13 @@ report_unsolved type_errors expr_holes
             -- If we are deferring we are going to need /all/ evidence around,
             -- including the evidence produced by unflattening (zonkWC)
        ; let tidy_env = tidyFreeTyCoVars emptyTidyEnv free_tvs
-             free_tvs = tyCoVarsOfWCList wanted
+             free_tvs = filterOut isCoVar $
+                        tyCoVarsOfWCList wanted
+                        -- tyCoVarsOfWC returns free coercion *holes*, even though
+                        -- they are "bound" by other wanted constraints. They in
+                        -- turn may mention variables bound further in, which makes
+                        -- no sense. Really we should not return those holes at all;
+                        -- for now we just filter them out.
 
        ; traceTc "reportUnsolved (after zonking):" $
          vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
@@ -832,7 +838,11 @@ eq_lhs_type ct1 ct2
        _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
 
 cmp_loc :: Ct -> Ct -> Ordering
-cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
+cmp_loc ct1 ct2 = get ct1 `compare` get ct2
+  where
+    get ct = realSrcSpanStart (ctLocSpan (ctLoc ct))
+             -- Reduce duplication by reporting only one error from each
+             -- /starting/ location even if the end location differs
 
 reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
 reportGroup mk_err ctxt cts =
@@ -1451,14 +1461,15 @@ mkTyVarEqErr dflags ctxt report ct tv1 ty2
        ; mkTyVarEqErr' dflags ctxt report ct tv1 ty2 }
 
 mkTyVarEqErr' dflags ctxt report ct tv1 ty2
-  | isUserSkolem ctxt tv1  -- ty2 won't be a meta-tyvar; we would have
-                           -- swapped in Solver.Canonical.canEqTyVarHomo
+  | isSkolemTyVar tv1  -- ty2 won't be a meta-tyvar; we would have
+                       -- swapped in Solver.Canonical.canEqTyVarHomo
     || isTyVarTyVar tv1 && not (isTyVarTy ty2)
     || ctEqRel ct == ReprEq
      -- The cases below don't really apply to ReprEq (except occurs check)
   = mkErrorMsgFromCt ctxt ct $ mconcat
         [ headline_msg
         , extraTyVarEqInfo ctxt tv1 ty2
+        , suggestAddSig ctxt ty1 ty2
         , report
         ]
 
@@ -1594,17 +1605,6 @@ mkEqInfoMsg ct ty1 ty2
                 <+> text "is a non-injective type family"
               | otherwise = empty
 
-isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
--- See Note [Reporting occurs-check errors]
-isUserSkolem ctxt tv
-  = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
-  where
-    is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
-      = tv `elem` sks && is_user_skol_info skol_info
-
-    is_user_skol_info (InferSkol {}) = False
-    is_user_skol_info _ = True
-
 misMatchOrCND :: Bool -> ReportErrCtxt -> Ct
               -> TcType -> TcType -> Report
 -- If oriented then ty1 is actual, ty2 is expected
@@ -1724,21 +1724,29 @@ extraTyVarInfo ctxt tv
 
 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> Report
 -- See Note [Suggest adding a type signature]
-suggestAddSig ctxt ty1 ty2
-  | null inferred_bndrs
+suggestAddSig ctxt ty1 _ty2
+  | null inferred_bndrs   -- No let-bound inferred binders in context
   = mempty
   | [bndr] <- inferred_bndrs
   = important $ text "Possible fix: add a type signature for" <+> quotes (ppr bndr)
   | otherwise
   = important $ text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs)
   where
-    inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
-    get_inf ty | Just tv <- tcGetTyVar_maybe ty
-               , isSkolemTyVar tv
-               , ((InferSkol prs, _) : _) <- getSkolemInfo (cec_encl ctxt) [tv]
-               = map fst prs
-               | otherwise
-               = []
+    inferred_bndrs = case tcGetTyVar_maybe ty1 of
+                       Just tv | isSkolemTyVar tv -> find (cec_encl ctxt) False tv
+                       _                          -> []
+
+    -- 'find' returns the binders of an InferSkol for 'tv',
+    -- provided there is an intervening implication with
+    -- ic_no_eqs = False (i.e. a GADT match)
+    find [] _ _ = []
+    find (implic:implics) seen_eqs tv
+       | tv `elem` ic_skols implic
+       , InferSkol prs <- ic_info implic
+       , seen_eqs
+       = map fst prs
+       | otherwise
+       = find implics (seen_eqs || not (ic_no_eqs implic)) tv
 
 --------------------
 misMatchMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> Report
@@ -2183,9 +2191,8 @@ sameOccExtra ty1 ty2
          mod = nameModule nm
          loc = nameSrcSpan nm
 
-{-
-Note [Suggest adding a type signature]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Suggest adding a type signature]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The OutsideIn algorithm rejects GADT programs that don't have a principal
 type, and indeed some that do.  Example:
    data T a where
@@ -2199,6 +2206,15 @@ untouchable type variable.  So suggestAddSig sees if the offending
 type variable is bound by an *inferred* signature, and suggests
 adding a declared signature instead.
 
+More specifically, we suggest adding a type sig if we have p ~ ty, and
+p is a skolem bound by an InferSkol.  Those skolems were created from
+unification variables in simplifyInfer.  Why didn't we unify?  It must
+have been because of an intervening GADT or existential, making it
+untouchable. Either way, a type signature would help.  For GADTs, it
+might make it typeable; for existentials the attempt to write a
+signature will fail -- or at least will produce a better error message
+next time
+
 This initially came up in #8968, concerning pattern synonyms.
 
 Note [Disambiguating (X ~ X) errors]