Fix #16517 by bumping the TcLevel for method sigs
[ghc.git] / compiler / typecheck / TcMType.hs
index 1516480..ce7c1ee 100644 (file)
@@ -759,14 +759,14 @@ writeMetaTyVar tyvar ty
 
 -- Everything from here on only happens if DEBUG is on
   | not (isTcTyVar tyvar)
-  = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
+  = ASSERT2( False, text "Writing to non-tc tyvar" <+> ppr tyvar )
     return ()
 
   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
   = writeMetaTyVarRef tyvar ref ty
 
   | otherwise
-  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
+  = ASSERT2( False, text "Writing to non-meta tyvar" <+> ppr tyvar )
     return ()
 
 --------------------
@@ -993,42 +993,6 @@ newMetaTyVarTyAtLevel tc_lvl kind
 *                                                                      *
 ********************************************************************* -}
 
-data CandidatesQTvs  -- See Note [Dependent type variables]
-                     -- See Note [CandidatesQTvs determinism and order]
-  -- NB: All variables stored here are MetaTvs. No exceptions.
-  = DV { dv_kvs :: DTyVarSet    -- "kind" metavariables (dependent)
-       , dv_tvs :: DTyVarSet    -- "type" metavariables (non-dependent)
-         -- A variable may appear in both sets
-         -- E.g.   T k (x::k)    The first occurrence of k makes it
-         --                      show up in dv_tvs, the second in dv_kvs
-         -- See Note [Dependent type variables]
-       , dv_cvs :: CoVarSet
-         -- These are covars. We will *not* quantify over these, but
-         -- we must make sure also not to quantify over any cv's kinds,
-         -- so we include them here as further direction for quantifyTyVars
-    }
-
-instance Semi.Semigroup CandidatesQTvs where
-   (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 })
-     <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 })
-          = DV { dv_kvs = kv1 `unionDVarSet` kv2
-               , dv_tvs = tv1 `unionDVarSet` tv2
-               , dv_cvs = cv1 `unionVarSet` cv2 }
-
-instance Monoid CandidatesQTvs where
-   mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet }
-   mappend = (Semi.<>)
-
-instance Outputable CandidatesQTvs where
-  ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs })
-    = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs
-                                             , text "dv_tvs =" <+> ppr tvs
-                                             , text "dv_cvs =" <+> ppr cvs ])
-
-
-candidateKindVars :: CandidatesQTvs -> TyVarSet
-candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
-
 {- Note [Dependent type variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In Haskell type inference we quantify over type variables; but we only
@@ -1102,18 +1066,18 @@ we are trying to generalise this type:
   forall arg. ... (alpha[tau]:arg) ...
 
 We have a metavariable alpha whose kind mentions a skolem variable
-boudn inside the very type we are generalising.
+bound inside the very type we are generalising.
 This can arise while type-checking a user-written type signature
 (see the test case for the full code).
 
 We cannot generalise over alpha!  That would produce a type like
   forall {a :: arg}. forall arg. ...blah...
 The fact that alpha's kind mentions arg renders it completely
-ineligible for generaliation.
+ineligible for generalisation.
 
 However, we are not going to learn any new constraints on alpha,
-because its kind isn't even in scope in the outer context.  So alpha
-is entirely unconstrained.
+because its kind isn't even in scope in the outer context (but see Wrinkle).
+So alpha is entirely unconstrained.
 
 What then should we do with alpha?  During generalization, every
 metavariable is either (A) promoted, (B) generalized, or (C) zapped
@@ -1134,18 +1098,75 @@ We do this eager zapping in candidateQTyVars, which always precedes
 generalisation, because at that moment we have a clear picture of
 what skolems are in scope.
 
+Wrinkle:
+
+We must make absolutely sure that alpha indeed is not
+from an outer context. (Otherwise, we might indeed learn more information
+about it.) This can be done easily: we just check alpha's TcLevel.
+That level must be strictly greater than the ambient TcLevel in order
+to treat it as naughty. We say "strictly greater than" because the call to
+candidateQTyVars is made outside the bumped TcLevel, as stated in the
+comment to candidateQTyVarsOfType. The level check is done in go_tv
+in collect_cant_qtvs. Skipping this check caused #16517.
+
 -}
 
+data CandidatesQTvs
+  -- See Note [Dependent type variables]
+  -- See Note [CandidatesQTvs determinism and order]
+  --
+  -- Invariants:
+  --   * All variables stored here are MetaTvs. No exceptions.
+  --   * All variables are fully zonked, including their kinds
+  --
+  = DV { dv_kvs :: DTyVarSet    -- "kind" metavariables (dependent)
+       , dv_tvs :: DTyVarSet    -- "type" metavariables (non-dependent)
+         -- A variable may appear in both sets
+         -- E.g.   T k (x::k)    The first occurrence of k makes it
+         --                      show up in dv_tvs, the second in dv_kvs
+         -- See Note [Dependent type variables]
+
+       , dv_cvs :: CoVarSet
+         -- These are covars. We will *not* quantify over these, but
+         -- we must make sure also not to quantify over any cv's kinds,
+         -- so we include them here as further direction for quantifyTyVars
+    }
+
+instance Semi.Semigroup CandidatesQTvs where
+   (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 })
+     <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 })
+          = DV { dv_kvs = kv1 `unionDVarSet` kv2
+               , dv_tvs = tv1 `unionDVarSet` tv2
+               , dv_cvs = cv1 `unionVarSet` cv2 }
+
+instance Monoid CandidatesQTvs where
+   mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet }
+   mappend = (Semi.<>)
+
+instance Outputable CandidatesQTvs where
+  ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs })
+    = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs
+                                             , text "dv_tvs =" <+> ppr tvs
+                                             , text "dv_cvs =" <+> ppr cvs ])
+
+
+candidateKindVars :: CandidatesQTvs -> TyVarSet
+candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
+
 -- | Gathers free variables to use as quantification candidates (in
 -- 'quantifyTyVars'). This might output the same var
 -- in both sets, if it's used in both a type and a kind.
+-- The variables to quantify must have a TcLevel strictly greater than
+-- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
 -- See Note [CandidatesQTvs determinism and order]
 -- See Note [Dependent type variables]
 candidateQTyVarsOfType :: TcType       -- not necessarily zonked
                        -> TcM CandidatesQTvs
 candidateQTyVarsOfType ty = collect_cand_qtvs False emptyVarSet mempty ty
 
--- | Like 'splitDepVarsOfType', but over a list of types
+-- | Like 'candidateQTyVarsOfType', but over a list of types
+-- The variables to quantify must have a TcLevel strictly greater than
+-- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
 candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs
 candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempty tys
 
@@ -1153,11 +1174,11 @@ candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempt
 -- to be dependent. This is appropriate when generalizing a *kind*,
 -- instead of a type. (That way, -XNoPolyKinds will default the variables
 -- to Type.)
-candidateQTyVarsOfKind :: TcKind       -- not necessarily zonked
+candidateQTyVarsOfKind :: TcKind       -- Not necessarily zonked
                        -> TcM CandidatesQTvs
 candidateQTyVarsOfKind ty = collect_cand_qtvs True emptyVarSet mempty ty
 
-candidateQTyVarsOfKinds :: [TcKind]       -- not necessarily zonked
+candidateQTyVarsOfKinds :: [TcKind]    -- Not necessarily zonked
                        -> TcM CandidatesQTvs
 candidateQTyVarsOfKinds tys = foldM (collect_cand_qtvs True emptyVarSet) mempty tys
 
@@ -1167,9 +1188,24 @@ delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
        , dv_tvs = tvs `delDVarSetList` vars
        , dv_cvs = cvs `delVarSetList`  vars }
 
-collect_cand_qtvs :: Bool   -- True <=> consider every fv in Type to be dependent
-                  -> VarSet -- bound variables (both locally bound and globally bound)
-                  -> CandidatesQTvs -> Type -> TcM CandidatesQTvs
+collect_cand_qtvs
+  :: Bool            -- True <=> consider every fv in Type to be dependent
+  -> VarSet          -- Bound variables (locals only)
+  -> CandidatesQTvs  -- Accumulating parameter
+  -> Type            -- Not necessarily zonked
+  -> TcM CandidatesQTvs
+
+-- Key points:
+--   * Looks through meta-tyvars as it goes;
+--     no need to zonk in advance
+--
+--   * Needs to be monadic anyway, because it does the zap-naughty
+--     stuff; see Note [Naughty quantification candidates]
+--
+--   * Returns fully-zonked CandidateQTvs, including their kinds
+--     so that subsequent dependency analysis (to build a well
+--     scoped telescope) works correctly
+
 collect_cand_qtvs is_dep bound dvs ty
   = go dvs ty
   where
@@ -1199,34 +1235,37 @@ collect_cand_qtvs is_dep bound dvs ty
 
     -----------------
     go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
-      | is_dep
-      = case tv `elemDVarSet` kvs of
-         True  -> return dv    -- We have met this tyvar aleady
-         False | intersectsVarSet bound (tyCoVarsOfType tv_kind)
-               -> -- See Note [Naughty quantification candidates]
-                  zap_naughty
-               | otherwise
-               -> collect_cand_qtvs True emptyVarSet dv' tv_kind
-               where
-                  dv' = dv { dv_kvs = kvs `extendDVarSet` tv }
-                        -- See Note [Order of accumulation]
+      | tv `elemDVarSet` kvs
+      = return dv  -- We have met this tyvar aleady
+
+      | not is_dep
+      , tv `elemDVarSet` tvs
+      = return dv  -- We have met this tyvar aleady
 
       | otherwise
-      = case tv `elemDVarSet` kvs || tv `elemDVarSet` tvs of
-         True  -> return dv    -- We have met this tyvar aleady
-         False | intersectsVarSet bound (tyCoVarsOfType tv_kind)
-               -> -- See Note [Naughty quantification candidates]
-                  zap_naughty
-               | otherwise
-               -> collect_cand_qtvs True emptyVarSet dv' tv_kind
-               where
-                  dv' = dv { dv_tvs = tvs `extendDVarSet` tv }
-                        -- See Note [Order of accumulation]
-      where
-        tv_kind = tyVarKind tv
-        zap_naughty = do { traceTc "Zapping naughty quantifier" (pprTyVar tv)
-                         ; writeMetaTyVar tv (anyTypeOfKind tv_kind)
-                         ; collect_cand_qtvs True bound dv tv_kind }
+      = do { tv_kind <- zonkTcType (tyVarKind tv)
+                 -- This zonk is annoying, but it is necessary, both to
+                 -- ensure that the collected candidates have zonked kinds
+                 -- (Trac #15795) and to make the naughty check
+                 -- (which comes next) works correctly
+
+           ; cur_lvl <- getTcLevel
+           ; if tcTyVarLevel tv `strictlyDeeperThan` cur_lvl &&
+                   -- this tyvar is from an outer context: see Wrinkle
+                   -- in Note [Naughty quantification candidates]
+
+                intersectsVarSet bound (tyCoVarsOfType tv_kind)
+
+             then -- See Note [Naughty quantification candidates]
+                  do { traceTc "Zapping naughty quantifier" (pprTyVar tv)
+                     ; writeMetaTyVar tv (anyTypeOfKind tv_kind)
+                     ; collect_cand_qtvs True bound dv tv_kind }
+
+             else do { let tv' = tv `setTyVarKind` tv_kind
+                           dv' | is_dep    = dv { dv_kvs = kvs `extendDVarSet` tv' }
+                               | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' }
+                               -- See Note [Order of accumulation]
+                     ; collect_cand_qtvs True emptyVarSet dv' tv_kind } }
 
 collect_cand_qtvs_co :: VarSet -- bound variables
                      -> CandidatesQTvs -> Coercion