Never Anyify during kind inference

See Note [Error on unconstrained meta-variables] in TcMType.

Close #17301
Close #17567
Close #17562
Close #15474

2 files changed, 208 insertions, 51 deletions

diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 8d14d9201d..24b7e4d93a 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -83,6 +83,7 @@ module GHC.Tc.Utils.TcMType (
   defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
   quantifyTyVars, isQuantifiableTv,
   skolemiseUnboundMetaTyVar, zonkAndSkolemise, skolemiseQuantifiedTyVar,
+  doNotQuantifyTyVars,
 
   candidateQTyVarsOfType,  candidateQTyVarsOfKind,
   candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
@@ -1299,6 +1300,29 @@ instance Outputable CandidatesQTvs where
                                              , text "dv_tvs =" <+> ppr tvs
                                              , text "dv_cvs =" <+> ppr cvs ])
 
+isEmptyCandidates :: CandidatesQTvs -> Bool
+isEmptyCandidates (DV { dv_kvs = kvs, dv_tvs = tvs })
+  = isEmptyDVarSet kvs && isEmptyDVarSet tvs
+
+-- | Extract out the kind vars (in order) and type vars (in order) from
+-- a 'CandidatesQTvs'. The lists are guaranteed to be distinct. Keeping
+-- the lists separate is important only in the -XNoPolyKinds case.
+candidateVars :: CandidatesQTvs -> ([TcTyVar], [TcTyVar])
+candidateVars (DV { dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
+  = (dep_kvs, nondep_tvs)
+  where
+    dep_kvs = scopedSort $ dVarSetElems dep_kv_set
+      -- scopedSort: put the kind variables into
+      --    well-scoped order.
+      --    E.g.  [k, (a::k)] not the other way round
+
+    nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set)
+      -- See Note [Dependent type variables]
+      -- The `minus` dep_tkvs removes any kind-level vars
+      --    e.g. T k (a::k)   Since k appear in a kind it'll
+      --    be in dv_kvs, and is dependent. So remove it from
+      --    dv_tvs which will also contain k
+      -- NB kinds of tvs are already zonked
 
 candidateKindVars :: CandidatesQTvs -> TyVarSet
 candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
@@ -1377,7 +1401,7 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
     go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs
     -- Uses accumulating-parameter style
     go dv (AppTy t1 t2)    = foldlM go dv [t1, t2]
-    go dv (TyConApp _ tys) = foldlM go dv tys
+    go dv (TyConApp tc tys) = go_tc_args dv (tyConBinders tc) tys
     go dv (FunTy _ w arg res) = foldlM go dv [w, arg, res]
     go dv (LitTy {})        = return dv
     go dv (CastTy ty co)    = do dv1 <- go dv ty
@@ -1395,6 +1419,20 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
       = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv)
            ; collect_cand_qtvs orig_ty is_dep (bound `extendVarSet` tv) dv1 ty }
 
+      -- This makes sure that we default e.g. the alpha in Proxy alpha (Any alpha).
+      -- Tested in polykinds/NestedProxies.
+      -- We just might get this wrong in AppTy, but I don't think that's possible
+      -- with -XNoPolyKinds. And fixing it would be non-performant, as we'd need
+      -- to look at kinds.
+    go_tc_args dv (tc_bndr:tc_bndrs) (ty:tys)
+      = do { dv1 <- collect_cand_qtvs orig_ty (is_dep || isNamedTyConBinder tc_bndr)
+                                      bound dv ty
+           ; go_tc_args dv1 tc_bndrs tys }
+    go_tc_args dv _bndrs tys  -- _bndrs might be non-empty: undersaturation
+                              -- tys might be non-empty: oversaturation
+                              -- either way, the foldlM is correct
+      = foldlM go dv tys
+
     -----------------
     go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
       | tv `elemDVarSet` kvs
@@ -1415,7 +1453,7 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
            ; cur_lvl <- getTcLevel
            ; if |  tcTyVarLevel tv <= cur_lvl
                 -> return dv   -- this variable is from an outer context; skip
-                               -- See Note [Use level numbers ofor quantification]
+                               -- See Note [Use level numbers for quantification]
 
                 |  intersectsVarSet bound tv_kind_vars
                    -- the tyvar must not be from an outer context, but we have
@@ -1566,7 +1604,7 @@ are about to wrap in a forall.
 
 It takes these free type/kind variables (partitioned into dependent and
 non-dependent variables) skolemises metavariables with a TcLevel greater
-than the ambient level (see Note [Use level numbers of quantification]).
+than the ambient level (see Note [Use level numbers for quantification]).
 
 * This function distinguishes between dependent and non-dependent
   variables only to keep correct defaulting behavior with -XNoPolyKinds.
@@ -1642,46 +1680,21 @@ quantifyTyVars :: CandidatesQTvs   -- See Note [Dependent type variables]
 -- invariants on CandidateQTvs, we do not have to filter out variables
 -- free in the environment here. Just quantify unconditionally, subject
 -- to the restrictions in Note [quantifyTyVars].
-quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
+quantifyTyVars dvs
        -- short-circuit common case
-  | isEmptyDVarSet dep_kv_set
-  , isEmptyDVarSet nondep_tkv_set
+  | isEmptyCandidates dvs
   = do { traceTc "quantifyTyVars has nothing to quantify" empty
        ; return [] }
 
   | otherwise
   = do { traceTc "quantifyTyVars {" (ppr dvs)
 
-       ; let dep_kvs = scopedSort $ dVarSetElems dep_kv_set
-              -- scopedSort: put the kind variables into
-              --    well-scoped order.
-              --    E.g.  [k, (a::k)] not the other way round
-
-             nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set)
-                 -- See Note [Dependent type variables]
-                 -- The `minus` dep_tkvs removes any kind-level vars
-                 --    e.g. T k (a::k)   Since k appear in a kind it'll
-                 --    be in dv_kvs, and is dependent. So remove it from
-                 --    dv_tvs which will also contain k
-                 -- NB kinds of tvs are already zonked
-
-             -- In the non-PolyKinds case, default the kind variables
-             -- to *, and zonk the tyvars as usual.  Notice that this
-             -- may make quantifyTyVars return a shorter list
-             -- than it was passed, but that's ok
-       ; poly_kinds  <- xoptM LangExt.PolyKinds
-       ; dep_kvs'    <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
-       ; nondep_tvs' <- mapMaybeM (zonk_quant False)            nondep_tvs
-       ; let final_qtvs = dep_kvs' ++ nondep_tvs'
-           -- Because of the order, any kind variables
-           -- mentioned in the kinds of the nondep_tvs'
-           -- now refer to the dep_kvs'
+       ; undefaulted <- defaultTyVars dvs
+       ; final_qtvs  <- mapMaybeM zonk_quant undefaulted
 
        ; traceTc "quantifyTyVars }"
-           (vcat [ text "nondep:"     <+> pprTyVars nondep_tvs
-                 , text "dep:"        <+> pprTyVars dep_kvs
-                 , text "dep_kvs'"    <+> pprTyVars dep_kvs'
-                 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
+           (vcat [ text "undefaulted:" <+> pprTyVars undefaulted
+                 , text "final_qtvs:"  <+> pprTyVars final_qtvs ])
 
        -- We should never quantify over coercion variables; check this
        ; let co_vars = filter isCoVar final_qtvs
@@ -1691,9 +1704,8 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
   where
     -- zonk_quant returns a tyvar if it should be quantified over;
     -- otherwise, it returns Nothing. The latter case happens for
-    --    * Kind variables, with -XNoPolyKinds: don't quantify over these
-    --    * RuntimeRep variables: we never quantify over these
-    zonk_quant default_kind tkv
+    -- non-meta-tyvars
+    zonk_quant tkv
       | not (isTyVar tkv)
       = return Nothing   -- this can happen for a covar that's associated with
                          -- a coercion hole. Test case: typecheck/should_compile/T2494
@@ -1703,11 +1715,7 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
                            -- kind signature, we have the class variables in
                            -- scope, and they are TyVars not TcTyVars
       | otherwise
-      = do { deflt_done <- defaultTyVar default_kind tkv
-           ; case deflt_done of
-               True  -> return Nothing
-               False -> do { tv <- skolemiseQuantifiedTyVar tkv
-                           ; return (Just tv) } }
+      = Just <$> skolemiseQuantifiedTyVar tkv
 
 isQuantifiableTv :: TcLevel   -- Level of the context, outside the quantification
                  -> TcTyVar
@@ -1817,6 +1825,24 @@ defaultTyVar default_kind tv
       where
         (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
 
+-- | Default some unconstrained type variables:
+--     RuntimeRep tyvars default to LiftedRep
+--     Multiplicity tyvars default to Many
+--     Type tyvars from dv_kvs default to Type, when -XNoPolyKinds
+--     (under -XNoPolyKinds, non-defaulting vars in dv_kvs is an error)
+defaultTyVars :: CandidatesQTvs  -- ^ all candidates for quantification
+              -> TcM [TcTyVar]   -- ^ those variables not defaulted
+defaultTyVars dvs
+  = do { poly_kinds <- xoptM LangExt.PolyKinds
+       ; defaulted_kvs <- mapM (defaultTyVar (not poly_kinds)) dep_kvs
+       ; defaulted_tvs <- mapM (defaultTyVar False)            nondep_tvs
+       ; let undefaulted_kvs = [ kv | (kv, False) <- dep_kvs    `zip` defaulted_kvs ]
+             undefaulted_tvs = [ tv | (tv, False) <- nondep_tvs `zip` defaulted_tvs ]
+       ; return (undefaulted_kvs ++ undefaulted_tvs) }
+          -- NB: kvs before tvs because tvs may depend on kvs
+  where
+    (dep_kvs, nondep_tvs) = candidateVars dvs
+
 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
 -- We have a Meta tyvar with a ref-cell inside it
 -- Skolemise it, so that we are totally out of Meta-tyvar-land
@@ -1851,6 +1877,134 @@ skolemiseUnboundMetaTyVar tv
                Indirect ty -> WARN( True, ppr tv $$ ppr ty )
                               return () }
 
+{- Note [Error on unconstrained meta-variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  type C :: Type -> Type -> Constraint
+  class (forall a. a b ~ a c) => C b c
+
+or
+
+  type T = forall a. Proxy a
+
+or
+
+  data (forall a. a b ~ a c) => T b c
+
+We will infer a :: Type -> kappa... but then we get no further information
+on kappa. What to do?
+
+ A. We could choose kappa := Type. But this only works when the kind of kappa
+    is Type (true in this example, but not always).
+ B. We could default to Any.
+ C. We could quantify.
+ D. We could error.
+
+We choose (D), as described in #17567. Discussion of alternatives is below.
+
+(One last example: type instance F Int = Proxy Any, where the unconstrained
+kind variable is the inferred kind of Any. The four examples here illustrate
+all cases in which this Note applies.)
+
+To do this, we must take an extra step before doing the final zonk to create
+e.g. a TyCon. (There is no problem in the final term-level zonk. See the
+section on alternative (B) below.) This extra step is needed only for
+constructs that do not quantify their free meta-variables, such as a class
+constraint or right-hand side of a type synonym.
+
+Specifically: before the final zonk, every construct must either call
+quantifyTyVars or doNotQuantifyTyVars. The latter issues an error
+if it is passed any free variables. (Exception: we still default
+RuntimeRep and Multiplicity variables.)
+
+Because no meta-variables remain after quantifying or erroring, we perform
+the zonk with NoFlexi, which panics upon seeing a meta-variable.
+
+Alternatives not implemented:
+
+A. As stated above, this works only sometimes. We might have a free
+   meta-variable of kind Nat, for example.
+
+B. This is what we used to do, but it caused Any to appear in error
+   messages sometimes. See #17567 for several examples. Defaulting to
+   Any during the final, whole-program zonk is OK, though, because
+   we are completely done type-checking at that point. No chance to
+   leak into an error message.
+
+C. Examine the class declaration at the top of this Note again.
+   Where should we quantify? We might imagine quantifying and
+   putting the kind variable in the forall of the quantified constraint.
+   But what if there are nested foralls? Which one should get the
+   variable? Other constructs have other problems. (For example,
+   the right-hand side of a type family instance equation may not
+   be a poly-type.)
+
+   More broadly, the GHC AST defines a set of places where it performs
+   implicit lexical generalization. For example, in a type
+   signature
+
+     f :: Proxy a -> Bool
+
+   the otherwise-unbound a is lexically quantified, giving us
+
+     f :: forall a. Proxy a -> Bool
+
+   The places that allow lexical quantification are marked in the AST with
+   HsImplicitBndrs. HsImplicitBndrs offers a binding site for otherwise-unbound
+   variables.
+
+   Later, during type-checking, we discover that a's kind is unconstrained.
+   We thus quantify *again*, to
+
+     f :: forall {k} (a :: k). Proxy @k a -> Bool
+
+   It is this second quantification that this Note is really about --
+   let's call it *inferred quantification*.
+   So there are two sorts of implicit quantification in types:
+     1. Lexical quantification: signalled by HsImplicitBndrs, occurs over
+        variables mentioned by the user but with no explicit binding site,
+        suppressed by a user-written forall (by the forall-or-nothing rule,
+        in Note [forall-or-nothing rule] in GHC.Hs.Type).
+     2. Inferred quantification: no signal in HsSyn, occurs over unconstrained
+        variables invented by the type-checker, possible only with -XPolyKinds,
+        unaffected by forall-or-nothing rule
+   These two quantifications are performed in different compiler phases, and are
+   essentially unrelated. However, it is convenient
+   for programmers to remember only one set of implicit quantification
+   sites. So, we choose to use the same places (those with HsImplicitBndrs)
+   for lexical quantification as for inferred quantification of unconstrained
+   meta-variables. Accordingly, there is no quantification in a class
+   constraint, or the other constructs that call doNotQuantifyTyVars.
+-}
+
+doNotQuantifyTyVars :: CandidatesQTvs
+                    -> (TidyEnv -> TcM (TidyEnv, SDoc))
+                            -- ^ like "the class context (D a b, E foogle)"
+                    -> TcM ()
+doNotQuantifyTyVars dvs where_found
+  | isEmptyCandidates dvs
+  = traceTc "doNotQuantifyTyVars has nothing to error on" empty
+
+  | otherwise
+  = do { traceTc "doNotQuantifyTyVars" (ppr dvs)
+       ; undefaulted <- defaultTyVars dvs
+          -- could have regular TyVars here, in an associated type RHS, or
+          -- bound by a type declaration head. So filter looking only for
+          -- metavars. e.g. b and c in `class (forall a. a b ~ a c) => C b c`
+          -- are OK
+       ; let leftover_metas = filter isMetaTyVar undefaulted
+       ; unless (null leftover_metas) $
+         do { let (tidy_env1, tidied_tvs) = tidyOpenTyCoVars emptyTidyEnv leftover_metas
+            ; (tidy_env2, where_doc) <- where_found tidy_env1
+            ; let doc = vcat [ text "Uninferrable type variable"
+                               <> plural tidied_tvs
+                               <+> pprWithCommas pprTyVar tidied_tvs
+                               <+> text "in"
+                             , where_doc ]
+            ; failWithTcM (tidy_env2, pprWithExplicitKindsWhen True doc) }
+       ; traceTc "doNotQuantifyTyVars success" empty }
+
 {- Note [Defaulting with -XNoPolyKinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index acfa24dd10..fbcc8444ed 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -33,10 +33,10 @@ module GHC.Tc.Utils.Zonk (
         zonkTopDecls, zonkTopExpr, zonkTopLExpr,
         zonkTopBndrs,
         ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv,
-        zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX,
+        zonkTyVarBindersX, zonkTyVarBinderX,
         zonkTyBndrs, zonkTyBndrsX,
         zonkTcTypeToType,  zonkTcTypeToTypeX,
-        zonkTcTypesToTypes, zonkTcTypesToTypesX, zonkScaledTcTypesToTypesX,
+        zonkTcTypesToTypesX, zonkScaledTcTypesToTypesX,
         zonkTyVarOcc,
         zonkCoToCo,
         zonkEvBinds, zonkTcEvBinds,
@@ -284,6 +284,10 @@ There are three possibilities:
   It's a way to have a variable that is not a mutable
   unification variable, but doesn't have a binding site
   either.
+
+* NoFlexi: See Note [Error on unconstrained meta-variables]
+  in GHC.Tc.Utils.TcMType. This mode will panic on unfilled
+  meta-variables.
 -}
 
 data ZonkFlexi   -- See Note [Un-unified unification variables]
@@ -291,6 +295,9 @@ data ZonkFlexi   -- See Note [Un-unified unification variables]
   | SkolemiseFlexi  -- Skolemise unbound unification variables
                     -- See Note [Zonking the LHS of a RULE]
   | RuntimeUnkFlexi -- Used in the GHCi debugger
+  | NoFlexi         -- Panic on unfilled meta-variables
+                    -- See Note [Error on unconstrained meta-variables]
+                    -- in GHC.Tc.Utils.TcMType
 
 instance Outputable ZonkEnv where
   ppr (ZonkEnv { ze_tv_env = tv_env
@@ -452,10 +459,6 @@ zonkTyBndrX env tv
        ; let tv' = mkTyVar (tyVarName tv) ki
        ; return (extendTyZonkEnv env tv', tv') }
 
-zonkTyVarBinders ::  [VarBndr TcTyVar vis]
-                 -> TcM (ZonkEnv, [VarBndr TyVar vis])
-zonkTyVarBinders tvbs = initZonkEnv $ \ ze -> zonkTyVarBindersX ze tvbs
-
 zonkTyVarBindersX :: ZonkEnv -> [VarBndr TcTyVar vis]
                              -> TcM (ZonkEnv, [VarBndr TyVar vis])
 zonkTyVarBindersX = mapAccumLM zonkTyVarBinderX
@@ -1847,6 +1850,9 @@ commitFlexi flexi tv zonked_kind
                         -- otherwise-unconstrained unification variables are
                         -- turned into RuntimeUnks as they leave the
                         -- typechecker's monad
+
+      NoFlexi -> pprPanic "NoFlexi" (ppr tv <+> dcolon <+> ppr zonked_kind)
+
   where
      name = tyVarName tv
 
@@ -1899,9 +1905,6 @@ zonkTcTyConToTyCon tc
 zonkTcTypeToType :: TcType -> TcM Type
 zonkTcTypeToType ty = initZonkEnv $ \ ze -> zonkTcTypeToTypeX ze ty
 
-zonkTcTypesToTypes :: [TcType] -> TcM [Type]
-zonkTcTypesToTypes tys = initZonkEnv $ \ ze -> zonkTcTypesToTypesX ze tys
-
 zonkScaledTcTypeToTypeX :: ZonkEnv -> Scaled TcType -> TcM (Scaled TcType)
 zonkScaledTcTypeToTypeX env (Scaled m ty) = Scaled <$> zonkTcTypeToTypeX env m
                                                    <*> zonkTcTypeToTypeX env ty