Apparent violation of TcLevel invariant in T7173
This is T7173
:
showEnv' env t = se 10 env t
where
se p env (Bind n b sc) = sb env n b
sb env n t = se 10 env t
data TT n = Bind n (TT n) (TT n)
In GHC.Tc.Solver.decideQuantification
, if I collect all metavariables and inspect their TcLevel
s, say with a patch like the following
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index e9d59946d3..20326f4f63 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -1689,7 +1689,7 @@ decideQuantification
decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
= do { -- Step 1: find the mono_tvs
; (candidates, co_vars, mono_tvs0)
- <- decidePromotedTyVars infer_mode name_taus psigs candidates
+ <- decidePromotedTyVars infer_mode rhs_tclvl name_taus psigs candidates
-- Step 2: default any non-mono tyvars, and re-simplify
-- This step may do some unification, but result candidates is zonked
@@ -1797,6 +1797,7 @@ Some rationale and observations
-}
decidePromotedTyVars :: InferMode
+ -> TcLevel
-> [(Name,TcType)]
-> [TcIdSigInst]
-> [PredType]
@@ -1818,7 +1819,7 @@ decidePromotedTyVars :: InferMode
--
-- Also return CoVars that appear free in the final quantified types
-- we can't quantify over these, and we must make sure they are in scope
-decidePromotedTyVars infer_mode name_taus psigs candidates
+decidePromotedTyVars infer_mode rhs_tclvl name_taus psigs candidates
= do { tc_lvl <- TcM.getTcLevel
; (no_quant, maybe_quant) <- pick infer_mode candidates
@@ -1833,7 +1834,18 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
; return (psig_qtvs, psig_theta, taus) }
; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
-
+ all_tvs = tyCoVarsOfTypesList (psig_tys ++ candidates ++ taus)
+
+ ; let bad_tvs = filter (\ tv -> isMetaTyVar tv && metaTyVarTcLevel tv `strictlyDeeperThan` rhs_tclvl) all_tvs
+ ; forM_ bad_tvs $ \ bad_tv ->
+ do { tv_contents <- TcM.readTcRef (metaTyVarRef bad_tv)
+ ; pprTraceM "decideQuantification: bad_tv" $
+ vcat [ text "curr_tclvl:" <+> ppr tc_lvl
+ , text "rhs_tclvl:" <+> ppr rhs_tclvl
+ , text "bad_tv:" <+> ppr bad_tv
+ , text "contents:" <+> ppr tv_contents ] }
+
+ ; let
-- (b) The co_var_tvs are tvs mentioned in the types of covars or
-- coercion holes. We can't quantify over these covars, so we
-- must include the variable in their types in the mono_tvs.
then we find that, when processing the outer showEnv'
binding after having handled the recursive group {se, sb}
, we see a metavariable that violates the TcLevel
invariant:
decideQuantification: bad_tv
curr_tclvl: 0
rhs_tclvl: 1
bad_tv: p_aBU[tau:2]
contents: Flexi
That is, we're at TcLevel
1 but we encounter a metavariable with level 2!
It's perhaps a bit clearer to use named wildcards (with a patch like !10170 to be able to see the user-written variable names):
showEnv' :: _env2 -> TT _n -> _res
showEnv' env t = se 10 env t
where
se :: Num _bad => _bad -> _env -> TT _n -> _res
se p env (Bind n b sc) = sb env n b
sb :: _env -> _n -> TT _n -> _res
sb env n t = se 10 env t
decideQuantification: bad_tv
curr_tclvl: 0
rhs_tclvl: 1
bad_tv: _bad_aBL[tau:2]
contents: Flexi
Note that, for some reason, if I change the metavariable _env2
to _env
, then the problem goes away.
I came across this while attempting to implement the defaulting plan in #20686. @simonpj @rae