[Git][ghc/ghc][wip/T24359] Capture bound tyvars of rules in zonker
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Nov 27 17:44:16 UTC 2024
Simon Peyton Jones pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
17c7320d by Simon Peyton Jones at 2024-11-27T17:42:18+00:00
Capture bound tyvars of rules in zonker
- - - - -
4 changed files:
- compiler/GHC/Runtime/Eval.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Zonk/Env.hs
- compiler/GHC/Tc/Zonk/Type.hs
Changes:
=====================================
compiler/GHC/Runtime/Eval.hs
=====================================
@@ -135,6 +135,7 @@ import Control.Monad
import Control.Monad.Catch as MC
import Data.Array
import Data.Dynamic
+import Data.IORef( newIORef )
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.List (find,intercalate)
@@ -1072,8 +1073,10 @@ parseInstanceHead str = withSession $ \hsc_env0 -> do
(ty, _) <- liftIO $ runInteractiveHsc hsc_env0 $ do
hsc_env <- getHscEnv
ty <- hscParseType str
- ioMsgMaybe $ hoistTcRnMessage $ tcRnType hsc_env SkolemiseFlexi True ty
-
+ skol_tv_ref <- liftIO (newIORef [])
+ ioMsgMaybe $ hoistTcRnMessage $
+ tcRnType hsc_env (SkolemiseFlexi skol_tv_ref) True ty
+ -- I'm not sure what to do about those zonked skolems
return ty
-- Get all the constraints required of a dictionary binding
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -957,57 +957,6 @@ tcSpecPrag poly_id (SpecSigE nm bndrs spec_e inl)
, spe_call = lhs_call
, spe_inl = inl }] }
-{-
- -- Solve unification constraints
- -- c.f. Note [The SimplifyRule Plan] step 1
- ; cloned_wanted <- cloneWC wanted -- See Note [Simplify cloned constraints]
- ; _ <- setTcLevel tc_lvl $ runTcS $ solveWanteds cloned_wanted
-
- -- Apply the unifications
- -- c.f. Note [The SimplifyRule Plan] step 2
- ; wanted <- liftZonkM $ zonkWC wanted
- ; seed_tys <- liftZonkM (mapM zonkTcType (rho : map idType id_bndrs))
-
- -- Quantify
- ; let (quant_cts, residual_wanted) = getRuleQuantCts wanted
- quant_preds = ctsPreds quant_cts
- ; dvs <- candidateQTyVarsOfTypes (quant_preds ++ seed_tys)
- ; let grown_tcvs = growThetaTyVars quant_preds (tyCoVarsOfTypes seed_tys)
- weeded_dvs = weedOutCandidates (`dVarSetIntersectVarSet` grown_tcvs) dvs
- ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars weeded_dvs
-
- -- Left hand side of the RULE
- ; lhs_evs <- mk_quant_evs quant_cts
- ; (implic1, lhs_binds) <- buildImplicationFor tc_lvl skol_info_anon
- qtkvs lhs_evs residual_wanted
-
- -- rhs_binds uses rhs_evs to build `wanted` (NB not just `residual_wanted`)
- ; rhs_evs <- mapM newEvVar quant_preds
- ; (implic2, rhs_binds) <- buildImplicationFor tc_lvl skol_info_anon
- qtkvs rhs_evs
- (emptyWC { wc_simple = quant_cts })
-
- ; emitImplications (implic1 `unionBags` implic2)
-
- ; traceTc "tcSpecPrag:SpecSigE" $
- vcat [ text "nm:" <+> ppr nm
- , text "bndrs:" <+> ppr bndrs
- , text "spec_e:" <+> ppr spec_e
- , text "tv/id bndrs:" <+> ppr qtkvs <+> ppr id_bndrs
- , text "lhs_evs:" <+> ppr lhs_evs
- , text "rhs_evs:" <+> ppr rhs_evs
- , text "spec_e:" <+> ppr spec_e'
- , text "inl:" <+> ppr inl ]
- ; return [SpecPragE { spe_poly_id = poly_id
- , spe_tv_bndrs = qtkvs
- , spe_id_bndrs = id_bndrs
- , spe_lhs_ev_bndrs = lhs_evs
- , spe_lhs_binds = lhs_binds
- , spe_lhs_call = spec_e'
- , spe_rhs_ev_bndrs = rhs_evs
- , spe_rhs_binds = rhs_binds
- , spe_inl = inl }] }
--}
tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
--------------
=====================================
compiler/GHC/Tc/Zonk/Env.hs
=====================================
@@ -61,10 +61,14 @@ data ZonkEnv
--
-- See Note [Un-unified unification variables]
data ZonkFlexi
- = DefaultFlexi -- ^ Default unbound unification variables to Any
- | SkolemiseFlexi -- ^ Skolemise unbound unification variables
- -- See Note [Zonking the LHS of a RULE]
+ = DefaultFlexi -- ^ Default unbound unification variables to Any
+
+ | SkolemiseFlexi -- ^ Skolemise unbound unification variables
+ (IORef [TyVar]) -- See Note [Zonking the LHS of a RULE]
+ -- Records the tyvars thus skolemised
+
| RuntimeUnkFlexi -- ^ Used in the GHCi debugger
+
| NoFlexi -- ^ Panic on unfilled meta-variables
-- See Note [Error on unconstrained meta-variables]
-- in GHC.Tc.Utils.TcMType
=====================================
compiler/GHC/Tc/Zonk/Type.hs
=====================================
@@ -380,7 +380,7 @@ zonkTyVarBinderX (Bndr tv vis)
zonkTyVarOcc :: HasDebugCallStack => TcTyVar -> ZonkTcM Type
zonkTyVarOcc tv
- = do { ZonkEnv { ze_tv_env = tv_env } <- getZonkEnv
+ = do { ZonkEnv { ze_tv_env = tv_env, ze_flexi = zonk_flexi } <- getZonkEnv
; let lookup_in_tv_env -- Look up in the env just as we do for Ids
= case lookupVarEnv tv_env tv of
@@ -394,7 +394,7 @@ zonkTyVarOcc tv
zonk_meta ref Flexi
= do { kind <- zonkTcTypeToTypeX (tyVarKind tv)
- ; ty <- commitFlexi tv kind
+ ; ty <- lift $ commitFlexi zonk_flexi tv kind
; lift $ liftZonkM $ writeMetaTyVarRef tv ref ty -- Belt and braces
; finish_meta ty }
@@ -442,50 +442,47 @@ lookupTyVarX tv
Nothing -> pprPanic "lookupTyVarOcc" (ppr tv $$ ppr tv_env)
; return res }
-commitFlexi :: TcTyVar -> Kind -> ZonkTcM Type
-commitFlexi tv zonked_kind
- = do { flexi <- ze_flexi <$> getZonkEnv
- ; lift $ case flexi of
- SkolemiseFlexi -> return (mkTyVarTy (mkTyVar name zonked_kind))
-
- DefaultFlexi
- -- Normally, RuntimeRep variables are defaulted in GHC.Tc.Utils.TcMType.defaultTyVar
- -- But that sees only type variables that appear in, say, an inferred type.
- -- Defaulting here, in the zonker, is needed to catch e.g.
- -- y :: Bool
- -- y = (\x -> True) undefined
- -- We need *some* known RuntimeRep for the x and undefined, but no one
- -- will choose it until we get here, in the zonker.
- | isRuntimeRepTy zonked_kind
- -> do { traceTc "Defaulting flexi tyvar to LiftedRep:" (pprTyVar tv)
- ; return liftedRepTy }
- | isLevityTy zonked_kind
- -> do { traceTc "Defaulting flexi tyvar to Lifted:" (pprTyVar tv)
- ; return liftedDataConTy }
- | isMultiplicityTy zonked_kind
- -> do { traceTc "Defaulting flexi tyvar to Many:" (pprTyVar tv)
- ; return manyDataConTy }
- | Just (ConcreteFRR origin) <- isConcreteTyVar_maybe tv
- -> do { addErr $ TcRnZonkerMessage (ZonkerCannotDefaultConcrete origin)
- ; return (anyTypeOfKind zonked_kind) }
- | otherwise
- -> do { traceTc "Defaulting flexi tyvar to ZonkAny:" (pprTyVar tv)
- -- See Note [Any types] in GHC.Builtin.Types, esp wrinkle (Any4)
- ; newZonkAnyType zonked_kind }
-
- RuntimeUnkFlexi
- -> do { traceTc "Defaulting flexi tyvar to RuntimeUnk:" (pprTyVar tv)
- ; return (mkTyVarTy (mkTcTyVar name zonked_kind RuntimeUnk)) }
- -- This is where RuntimeUnks are born:
- -- 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
-
+commitFlexi :: ZonkFlexi -> TcTyVar -> Kind -> TcM Type
+commitFlexi NoFlexi tv zonked_kind
+ = pprPanic "NoFlexi" (ppr tv <+> dcolon <+> ppr zonked_kind)
+
+commitFlexi (SkolemiseFlexi tvs_ref) tv zonked_kind
+ = do { let skol_tv = mkTyVar (tyVarName tv) zonked_kind
+ ; updTcRef tvs_ref (skol_tv :)
+ ; return (mkTyVarTy skol_tv) }
+
+commitFlexi RuntimeUnkFlexi tv zonked_kind
+ = do { traceTc "Defaulting flexi tyvar to RuntimeUnk:" (pprTyVar tv)
+ ; return (mkTyVarTy (mkTcTyVar (tyVarName tv) zonked_kind RuntimeUnk)) }
+ -- This is where RuntimeUnks are born:
+ -- otherwise-unconstrained unification variables are
+ -- turned into RuntimeUnks as they leave the
+ -- typechecker's monad
+
+commitFlexi DefaultFlexi tv zonked_kind
+ -- Normally, RuntimeRep variables are defaulted in GHC.Tc.Utils.TcMType.defaultTyVar
+ -- But that sees only type variables that appear in, say, an inferred type.
+ -- Defaulting here, in the zonker, is needed to catch e.g.
+ -- y :: Bool
+ -- y = (\x -> True) undefined
+ -- We need *some* known RuntimeRep for the x and undefined, but no one
+ -- will choose it until we get here, in the zonker.
+ | isRuntimeRepTy zonked_kind
+ = do { traceTc "Defaulting flexi tyvar to LiftedRep:" (pprTyVar tv)
+ ; return liftedRepTy }
+ | isLevityTy zonked_kind
+ = do { traceTc "Defaulting flexi tyvar to Lifted:" (pprTyVar tv)
+ ; return liftedDataConTy }
+ | isMultiplicityTy zonked_kind
+ = do { traceTc "Defaulting flexi tyvar to Many:" (pprTyVar tv)
+ ; return manyDataConTy }
+ | Just (ConcreteFRR origin) <- isConcreteTyVar_maybe tv
+ = do { addErr $ TcRnZonkerMessage (ZonkerCannotDefaultConcrete origin)
+ ; return (anyTypeOfKind zonked_kind) }
+ | otherwise
+ = do { traceTc "Defaulting flexi tyvar to ZonkAny:" (pprTyVar tv)
+ -- See Note [Any types] in GHC.Builtin.Types, esp wrinkle (Any4)
+ ; newZonkAnyType zonked_kind }
zonkCoVarOcc :: CoVar -> ZonkTcM Coercion
zonkCoVarOcc cv
@@ -858,22 +855,25 @@ zonkLTcSpecPrags ps
; id' <- zonkIdOcc id
; return (L loc (SpecPrag id' co_fn' inl)) }
zonk_prag (L loc (SpecPragE { spe_poly_id = poly_id
- , spe_tv_bndrs = tv_bndrs, spe_id_bndrs = id_bndrs
+ , spe_tv_bndrs = tv_bndrs
+ , spe_id_bndrs = id_bndrs
, spe_ev_bndrs = lhs_evs
, spe_call = spec_e
, spe_inl = inl }))
- = setZonkType SkolemiseFlexi $
- runZonkBndrT (zonkCoreBndrsX tv_bndrs) $ \tv_bndrs' ->
- runZonkBndrT (zonkCoreBndrsX id_bndrs) $ \id_bndrs' ->
- runZonkBndrT (zonkCoreBndrsX lhs_evs) $ \lhs_evs' ->
- do { poly_id' <- zonkIdOcc poly_id -- Does not need to be under all these binders, but no harm
- ; spec_e' <- zonkLExpr spec_e
- ; return (L loc (SpecPragE { spe_poly_id = poly_id'
- , spe_tv_bndrs = tv_bndrs'
- , spe_id_bndrs = id_bndrs'
- , spe_ev_bndrs = lhs_evs'
- , spe_call = spec_e'
- , spe_inl = inl })) }
+ = do { skol_tvs_ref <- lift $ newTcRef []
+ ; setZonkType (SkolemiseFlexi skol_tvs_ref) $
+ runZonkBndrT (zonkCoreBndrsX tv_bndrs) $ \tv_bndrs' ->
+ runZonkBndrT (zonkCoreBndrsX id_bndrs) $ \id_bndrs' ->
+ runZonkBndrT (zonkCoreBndrsX lhs_evs) $ \lhs_evs' ->
+ do { poly_id' <- zonkIdOcc poly_id -- Does not need to be under all these binders, but no harm
+ ; spec_e' <- zonkLExpr spec_e
+ ; skol_tvs <- lift $ readTcRef skol_tvs_ref
+ ; return (L loc (SpecPragE { spe_poly_id = poly_id'
+ , spe_tv_bndrs = skol_tvs ++ tv_bndrs'
+ , spe_id_bndrs = id_bndrs'
+ , spe_ev_bndrs = lhs_evs'
+ , spe_call = spec_e'
+ , spe_inl = inl })) } }
{-
************************************************************************
@@ -1690,13 +1690,20 @@ zonkRule :: RuleDecl GhcTc -> ZonkTcM (RuleDecl GhcTc)
zonkRule rule@(HsRule { rd_bndrs = bndrs
, rd_lhs = lhs
, rd_rhs = rhs })
- = zonkRuleBndrs bndrs $ \ new_bndrs ->
- do { -- See Note [Zonking the LHS of a RULE]
- ; new_lhs <- setZonkType SkolemiseFlexi $ zonkLExpr lhs
- ; new_rhs <- zonkLExpr rhs
- ; return $ rule { rd_bndrs = new_bndrs
- , rd_lhs = new_lhs
- , rd_rhs = new_rhs } }
+ = do { skol_tvs_ref <- lift $ newTcRef []
+ ; setZonkType (SkolemiseFlexi skol_tvs_ref) $
+ zonkRuleBndrs bndrs $ \ new_bndrs ->
+ do { -- See Note [Zonking the LHS of a RULE]
+ ; new_lhs <- zonkLExpr lhs
+ ; skol_tvs <- lift $ readTcRef skol_tvs_ref
+ ; new_rhs <- setZonkType DefaultFlexi $ zonkLExpr rhs
+ ; return $ rule { rd_bndrs = add_tvs skol_tvs new_bndrs
+ , rd_lhs = new_lhs
+ , rd_rhs = new_rhs } } }
+ where
+ add_tvs :: [TyVar] -> RuleBndrs GhcTc -> RuleBndrs GhcTc
+ add_tvs tvs rbs@(RuleBndrs { rb_tmvs = bndrs })
+ = rbs { rb_tmvs = map (noLocA . RuleBndr noAnn . noLocA) tvs ++ bndrs }
zonkRuleBndrs :: RuleBndrs GhcTc -> (RuleBndrs GhcTc -> ZonkTcM a) -> ZonkTcM a
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/17c7320d8479bdff67051ce27a46957dfa2c1824
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/17c7320d8479bdff67051ce27a46957dfa2c1824
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20241127/8a5e9b0a/attachment-0001.html>
More information about the ghc-commits
mailing list