[Git][ghc/ghc][wip/T24359] More progress
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Feb 9 00:14:24 UTC 2024
Simon Peyton Jones pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
2a909abd by Simon Peyton Jones at 2024-02-09T00:13:24+00:00
More progress
(Still does not compile.)
- - - - -
10 changed files:
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Rename/Bind.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/Gen/Rule.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/Language/Haskell/Syntax/Binds.hs
- compiler/Language/Haskell/Syntax/Decls.hs
- compiler/ghc.cabal.in
Changes:
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -1105,7 +1105,7 @@ Consider #22471
We get two dicts on the LHS, one from `1` and one from `+`.
For reasons described in Note [The SimplifyRule Plan] in
-GHC.Tc.Gen.Rule, we quantify separately over those dictionaries:
+GHC.Tc.Gen.Sig, we quantify separately over those dictionaries:
forall f (d1::Num Int) (d2 :: Num Int).
foo (\xs. (+) d1 (fromInteger d2 1) xs) = ...
=====================================
compiler/GHC/Rename/Bind.hs
=====================================
@@ -1091,10 +1091,11 @@ renameSig ctxt sig@(SpecSig _ v tys inl)
= do { (new_ty, fvs_ty) <- rnHsSigType ty_ctxt TypeLevel ty
; return ( new_ty:tys, fvs_ty `plusFV` fvs) }
-renameSig ctxt sig@(SpecSigE _ spec_e inl)
- = do { (spec_e', fvs) <- rnLExpr spec_e
+renameSig ctxt sig@(SpecSigE _ bndrs spec_e inl)
+ = bindrRuleBndrs bndrs $ \_ bndrs' ->
+ do { (spec_e', fvs) <- rnLExpr spec_e
; fn <- checkSpecSig spec_e'
- ; return (SpecSigE fn spec_e' inl, fvs) }
+ ; return (SpecSigE fn bndrs' spec_e' inl, fvs) }
renameSig ctxt sig@(InlineSig _ v s)
= do { new_v <- lookupSigOccRnN ctxt sig v
@@ -1259,6 +1260,55 @@ checkDupMinimalSigs sigs
sig1 : sig2 : otherSigs -> dupMinimalSigErr sig1 sig2 otherSigs
_ -> return ()
+bindRuleBndrs :: RuleName -> RuleBndrs GhcPs
+ -> ([Name] -> RuleBndrs GhcRn -> RnM (a,FreeVars))
+ -> RnM (a,FreeVars)
+bindRuleBndrs rule_name (RuleBndrs { rb_tyvs = tyvs, rb_tmvs = tmvs }) thing_inside
+ = do { let rdr_names_w_loc = map (get_var . unLoc) tmvs
+ doc = RuleCtx rule_name
+ ; checkDupRdrNames rdr_names_w_loc
+ ; checkShadowedRdrNames rdr_names_w_loc
+ ; names <- newLocalBndrsRn rdr_names_w_loc
+ ; bindRuleTyVars doc tyvs $ \ tyvs' ->
+ bindRuleTmVars doc tyvs' tmvs names $ \ tmvs' ->
+ thing_inside (RuleBndrs { rb_tyvs = tyvs', rb_tmvs = tmvs' }) }
+ where
+ get_var :: RuleBndr GhcPs -> LocatedN RdrName
+ get_var (RuleBndrSig _ v _) = v
+ get_var (RuleBndr _ v) = v
+
+
+bindRuleTmVars :: HsDocContext -> Maybe ty_bndrs
+ -> [LRuleBndr GhcPs] -> [Name]
+ -> ([LRuleBndr GhcRn] -> RnM (a, FreeVars))
+ -> RnM (a, FreeVars)
+bindRuleTmVars doc tyvs vars names thing_inside
+ = go vars names $ \ vars' ->
+ bindLocalNamesFV names (thing_inside vars')
+ where
+ go ((L l (RuleBndr _ (L loc _))) : vars) (n : ns) thing_inside
+ = go vars ns $ \ vars' ->
+ thing_inside (L l (RuleBndr noAnn (L loc n)) : vars')
+
+ go ((L l (RuleBndrSig _ (L loc _) bsig)) : vars)
+ (n : ns) thing_inside
+ = rnHsPatSigType bind_free_tvs doc bsig $ \ bsig' ->
+ go vars ns $ \ vars' ->
+ thing_inside (L l (RuleBndrSig noAnn (L loc n) bsig') : vars')
+
+ go [] [] thing_inside = thing_inside []
+ go vars names _ = pprPanic "bindRuleVars" (ppr vars $$ ppr names)
+
+ bind_free_tvs = case tyvs of Nothing -> AlwaysBind
+ Just _ -> NeverBind
+
+bindRuleTyVars :: HsDocContext -> Maybe [LHsTyVarBndr () GhcPs]
+ -> (Maybe [LHsTyVarBndr () GhcRn] -> RnM (b, FreeVars))
+ -> RnM (b, FreeVars)
+bindRuleTyVars doc (Just bndrs) thing_inside
+ = bindLHsTyVarBndrs doc WarnUnusedForalls Nothing bndrs (thing_inside . Just)
+bindRuleTyVars _ _ thing_inside = thing_inside Nothing
+
{-
************************************************************************
* *
=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -25,7 +25,7 @@ import GHC.Hs
import GHC.Types.FieldLabel
import GHC.Types.Name.Reader
import GHC.Rename.HsType
-import GHC.Rename.Bind
+import GHC.Rename.Bind( bindRuleBndrs )
import GHC.Rename.Doc
import GHC.Rename.Env
import GHC.Rename.Utils ( mapFvRn, bindLocalNames
@@ -1150,22 +1150,15 @@ rnHsRuleDecls (HsRules { rds_ext = (_, src)
rnHsRuleDecl :: RuleDecl GhcPs -> RnM (RuleDecl GhcRn, FreeVars)
rnHsRuleDecl (HsRule { rd_ext = (_, st)
- , rd_name = rule_name
+ , rd_name = L _ rule_name
, rd_act = act
- , rd_tyvs = tyvs
- , rd_tmvs = tmvs
+ , rd_bndr = bndrs
, rd_lhs = lhs
, rd_rhs = rhs })
- = do { let rdr_names_w_loc = map (get_var . unLoc) tmvs
- ; checkDupRdrNames rdr_names_w_loc
- ; checkShadowedRdrNames rdr_names_w_loc
- ; names <- newLocalBndrsRn rdr_names_w_loc
- ; let doc = RuleCtx (unLoc rule_name)
- ; bindRuleTyVars doc tyvs $ \ tyvs' ->
- bindRuleTmVars doc tyvs' tmvs names $ \ tmvs' ->
+ = bindRuleBndrs rule_name bndrs $ \tm_names bndrs' ->
do { (lhs', fv_lhs') <- rnLExpr lhs
; (rhs', fv_rhs') <- rnLExpr rhs
- ; checkValidRule (unLoc rule_name) names lhs' fv_lhs'
+ ; checkValidRule rule_name tm_names lhs' fv_lhs'
; return (HsRule { rd_ext = (HsRuleRn fv_lhs' fv_rhs', st)
, rd_name = rule_name
, rd_act = act
@@ -1173,41 +1166,6 @@ rnHsRuleDecl (HsRule { rd_ext = (_, st)
, rd_tmvs = tmvs'
, rd_lhs = lhs'
, rd_rhs = rhs' }, fv_lhs' `plusFV` fv_rhs') } }
- where
- get_var :: RuleBndr GhcPs -> LocatedN RdrName
- get_var (RuleBndrSig _ v _) = v
- get_var (RuleBndr _ v) = v
-
-bindRuleTmVars :: HsDocContext -> Maybe ty_bndrs
- -> [LRuleBndr GhcPs] -> [Name]
- -> ([LRuleBndr GhcRn] -> RnM (a, FreeVars))
- -> RnM (a, FreeVars)
-bindRuleTmVars doc tyvs vars names thing_inside
- = go vars names $ \ vars' ->
- bindLocalNamesFV names (thing_inside vars')
- where
- go ((L l (RuleBndr _ (L loc _))) : vars) (n : ns) thing_inside
- = go vars ns $ \ vars' ->
- thing_inside (L l (RuleBndr noAnn (L loc n)) : vars')
-
- go ((L l (RuleBndrSig _ (L loc _) bsig)) : vars)
- (n : ns) thing_inside
- = rnHsPatSigType bind_free_tvs doc bsig $ \ bsig' ->
- go vars ns $ \ vars' ->
- thing_inside (L l (RuleBndrSig noAnn (L loc n) bsig') : vars')
-
- go [] [] thing_inside = thing_inside []
- go vars names _ = pprPanic "bindRuleVars" (ppr vars $$ ppr names)
-
- bind_free_tvs = case tyvs of Nothing -> AlwaysBind
- Just _ -> NeverBind
-
-bindRuleTyVars :: HsDocContext -> Maybe [LHsTyVarBndr () GhcPs]
- -> (Maybe [LHsTyVarBndr () GhcRn] -> RnM (b, FreeVars))
- -> RnM (b, FreeVars)
-bindRuleTyVars doc (Just bndrs) thing_inside
- = bindLHsTyVarBndrs doc WarnUnusedForalls Nothing bndrs (thing_inside . Just)
-bindRuleTyVars _ _ thing_inside = thing_inside Nothing
{-
Note [Rule LHS validity checking]
=====================================
compiler/GHC/Tc/Gen/Rule.hs
=====================================
@@ -7,7 +7,11 @@
-}
-- | Typechecking rewrite rules
-module GHC.Tc.Gen.Rule ( tcRules ) where
+module GHC.Tc.Gen.Rule (
+ tcRules,
+ tcRuleBndrs,
+ mkTcRuleBndrs
+ ) where
import GHC.Prelude
@@ -21,6 +25,7 @@ import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.TcType
import GHC.Tc.Gen.HsType
+import GHC.Tc.Gen.Sig( tcRuleBndrs )
import GHC.Tc.Gen.Expr
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.Unify( buildImplicationFor )
@@ -41,477 +46,3 @@ import GHC.Utils.Panic
import GHC.Data.FastString
import GHC.Data.Bag
-{-
-Note [Typechecking rules]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-We *infer* the typ of the LHS, and use that type to *check* the type of
-the RHS. That means that higher-rank rules work reasonably well. Here's
-an example (test simplCore/should_compile/rule2.hs) produced by Roman:
-
- foo :: (forall m. m a -> m b) -> m a -> m b
- foo f = ...
-
- bar :: (forall m. m a -> m a) -> m a -> m a
- bar f = ...
-
- {-# RULES "foo/bar" foo = bar #-}
-
-He wanted the rule to typecheck.
-
-Note [TcLevel in type checking rules]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Bringing type variables into scope naturally bumps the TcLevel. Thus, we type
-check the term-level binders in a bumped level, and we must accordingly bump
-the level whenever these binders are in scope.
-
-Note [Re-quantify type variables in rules]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this example from #17710:
-
- foo :: forall k (a :: k) (b :: k). Proxy a -> Proxy b
- foo x = Proxy
- {-# RULES "foo" forall (x :: Proxy (a :: k)). foo x = Proxy #-}
-
-Written out in more detail, the "foo" rewrite rule looks like this:
-
- forall k (a :: k). forall (x :: Proxy (a :: k)). foo @k @a @b0 x = Proxy @k @b0
-
-Where b0 is a unification variable. Where should b0 be quantified? We have to
-quantify it after k, since (b0 :: k). But generalization usually puts inferred
-type variables (such as b0) at the /front/ of the telescope! This creates a
-conflict.
-
-One option is to simply throw an error, per the principles of
-Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType. This is what would happen
-if we were generalising over a normal type signature. On the other hand, the
-types in a rewrite rule aren't quite "normal", since the notions of specified
-and inferred type variables aren't applicable.
-
-A more permissive design (and the design that GHC uses) is to simply requantify
-all of the type variables. That is, we would end up with this:
-
- forall k (a :: k) (b :: k). forall (x :: Proxy (a :: k)). foo @k @a @b x = Proxy @k @b
-
-It's a bit strange putting the generalized variable `b` after the user-written
-variables `k` and `a`. But again, the notion of specificity is not relevant to
-rewrite rules, since one cannot "visibly apply" a rewrite rule. This design not
-only makes "foo" typecheck, but it also makes the implementation simpler.
-
-See also Note [Generalising in tcTyFamInstEqnGuts] in GHC.Tc.TyCl, which
-explains a very similar design when generalising over a type family instance
-equation.
--}
-
-tcRules :: [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTc]
-tcRules decls = mapM (wrapLocMA tcRuleDecls) decls
-
-tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
-tcRuleDecls (HsRules { rds_ext = src
- , rds_rules = decls })
- = do { tc_decls <- mapM (wrapLocMA tcRule) decls
- ; return $ HsRules { rds_ext = src
- , rds_rules = tc_decls } }
-
-tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
-tcRule (HsRule { rd_ext = ext
- , rd_name = rname@(L _ name)
- , rd_act = act
- , rd_tyvs = ty_bndrs
- , rd_tmvs = tm_bndrs
- , rd_lhs = lhs
- , rd_rhs = rhs })
- = addErrCtxt (ruleCtxt name) $
- do { traceTc "---- Rule ------" (pprFullRuleName (snd ext) rname)
- ; skol_info <- mkSkolemInfo (RuleSkol name)
- -- Note [Typechecking rules]
- ; (tc_lvl, stuff) <- pushTcLevelM $
- generateRuleConstraints name ty_bndrs tm_bndrs lhs rhs
-
- ; let (id_bndrs, lhs', lhs_wanted
- , rhs', rhs_wanted, rule_ty) = stuff
-
- ; traceTc "tcRule 1" (vcat [ pprFullRuleName (snd ext) rname
- , ppr lhs_wanted
- , ppr rhs_wanted ])
-
- ; (lhs_evs, residual_lhs_wanted, dont_default)
- <- simplifyRule name tc_lvl lhs_wanted rhs_wanted
-
- -- SimplifyRule Plan, step 4
- -- Now figure out what to quantify over
- -- c.f. GHC.Tc.Solver.simplifyInfer
- -- We quantify over any tyvars free in *either* the rule
- -- *or* the bound variables. The latter is important. Consider
- -- ss (x,(y,z)) = (x,z)
- -- RULE: forall v. fst (ss v) = fst v
- -- The type of the rhs of the rule is just a, but v::(a,(b,c))
- --
- -- We also need to get the completely-unconstrained tyvars of
- -- the LHS, lest they otherwise get defaulted to Any; but we do that
- -- during zonking (see GHC.Tc.Zonk.Type.zonkRule)
-
- ; let tpl_ids = lhs_evs ++ id_bndrs
-
- -- See Note [Re-quantify type variables in rules]
- ; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids)
- ; let weed_out = (`dVarSetMinusVarSet` dont_default)
- quant_cands = forall_tkvs { dv_kvs = weed_out (dv_kvs forall_tkvs)
- , dv_tvs = weed_out (dv_tvs forall_tkvs) }
- ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars quant_cands
- ; traceTc "tcRule" (vcat [ pprFullRuleName (snd ext) rname
- , text "forall_tkvs:" <+> ppr forall_tkvs
- , text "quant_cands:" <+> ppr quant_cands
- , text "dont_default:" <+> ppr dont_default
- , text "residual_lhs_wanted:" <+> ppr residual_lhs_wanted
- , text "qtkvs:" <+> ppr qtkvs
- , text "rule_ty:" <+> ppr rule_ty
- , text "ty_bndrs:" <+> ppr ty_bndrs
- , text "qtkvs ++ tpl_ids:" <+> ppr (qtkvs ++ tpl_ids)
- , text "tpl_id info:" <+>
- vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
- ])
-
- -- SimplfyRule Plan, step 5
- -- Simplify the LHS and RHS constraints:
- -- For the LHS constraints we must solve the remaining constraints
- -- (a) so that we report insoluble ones
- -- (b) so that we bind any soluble ones
- ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
- lhs_evs residual_lhs_wanted
- ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
- lhs_evs rhs_wanted
- ; emitImplications (lhs_implic `unionBags` rhs_implic)
- ; return $ HsRule { rd_ext = ext
- , rd_name = rname
- , rd_act = act
- , rd_tyvs = ty_bndrs -- preserved for ppr-ing
- , rd_tmvs = map (noLocA . RuleBndr noAnn . noLocA)
- (qtkvs ++ tpl_ids)
- , rd_lhs = mkHsDictLet lhs_binds lhs'
- , rd_rhs = mkHsDictLet rhs_binds rhs' } }
-
-generateRuleConstraints :: FastString
- -> Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
- -> LHsExpr GhcRn -> LHsExpr GhcRn
- -> TcM ( [TcId]
- , LHsExpr GhcTc, WantedConstraints
- , LHsExpr GhcTc, WantedConstraints
- , TcType )
-generateRuleConstraints rule_name ty_bndrs tm_bndrs lhs rhs
- = do { ((tv_bndrs, id_bndrs), bndr_wanted) <- captureConstraints $
- tcRuleBndrs rule_name ty_bndrs tm_bndrs
- -- bndr_wanted constraints can include wildcard hole
- -- constraints, which we should not forget about.
- -- It may mention the skolem type variables bound by
- -- the RULE. c.f. #10072
- ; tcExtendNameTyVarEnv [(tyVarName tv, tv) | tv <- tv_bndrs] $
- tcExtendIdEnv id_bndrs $
- do { -- See Note [Solve order for RULES]
- ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
- ; (rhs', rhs_wanted) <- captureConstraints $
- tcCheckMonoExpr rhs rule_ty
- ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
- ; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
-
--- See Note [TcLevel in type checking rules]
-tcRuleBndrs :: FastString -> Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
- -> TcM ([TcTyVar], [Id])
-tcRuleBndrs rule_name (Just bndrs) xs
- = do { skol_info <- mkSkolemInfo (RuleSkol rule_name)
- ; (tybndrs1,(tys2,tms)) <- bindExplicitTKBndrs_Skol skol_info bndrs $
- tcRuleTmBndrs rule_name xs
- ; let tys1 = binderVars tybndrs1
- ; return (tys1 ++ tys2, tms) }
-
-tcRuleBndrs rule_name Nothing xs
- = tcRuleTmBndrs rule_name xs
-
--- See Note [TcLevel in type checking rules]
-tcRuleTmBndrs :: FastString -> [LRuleBndr GhcRn] -> TcM ([TcTyVar],[Id])
-tcRuleTmBndrs _ [] = return ([],[])
-tcRuleTmBndrs rule_name (L _ (RuleBndr _ (L _ name)) : rule_bndrs)
- = do { ty <- newOpenFlexiTyVarTy
- ; (tyvars, tmvars) <- tcRuleTmBndrs rule_name rule_bndrs
- ; return (tyvars, mkLocalId name ManyTy ty : tmvars) }
-tcRuleTmBndrs rule_name (L _ (RuleBndrSig _ (L _ name) rn_ty) : rule_bndrs)
--- e.g x :: a->a
--- The tyvar 'a' is brought into scope first, just as if you'd written
--- a::*, x :: a->a
--- If there's an explicit forall, the renamer would have already reported an
--- error for each out-of-scope type variable used
- = do { let ctxt = RuleSigCtxt rule_name name
- ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt HM_Sig rn_ty OpenKind
- ; let id = mkLocalId name ManyTy id_ty
- -- See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType
-
- -- The type variables scope over subsequent bindings; yuk
- ; (tyvars, tmvars) <- tcExtendNameTyVarEnv tvs $
- tcRuleTmBndrs rule_name rule_bndrs
- ; return (map snd tvs ++ tyvars, id : tmvars) }
-
-ruleCtxt :: FastString -> SDoc
-ruleCtxt name = text "When checking the rewrite rule" <+>
- doubleQuotes (ftext name)
-
-
-{-
-*********************************************************************************
-* *
- Constraint simplification for rules
-* *
-***********************************************************************************
-
-Note [The SimplifyRule Plan]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Example. Consider the following left-hand side of a rule
- f (x == y) (y > z) = ...
-If we typecheck this expression we get constraints
- d1 :: Ord a, d2 :: Eq a
-We do NOT want to "simplify" to the LHS
- forall x::a, y::a, z::a, d1::Ord a.
- f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
-Instead we want
- forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
- f ((==) d2 x y) ((>) d1 y z) = ...
-
-Here is another example:
- fromIntegral :: (Integral a, Num b) => a -> b
- {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
-In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
-we *dont* want to get
- forall dIntegralInt.
- fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
-because the scsel will mess up RULE matching. Instead we want
- forall dIntegralInt, dNumInt.
- fromIntegral Int Int dIntegralInt dNumInt = id Int
-
-Even if we have
- g (x == y) (y == z) = ..
-where the two dictionaries are *identical*, we do NOT WANT
- forall x::a, y::a, z::a, d1::Eq a
- f ((==) d1 x y) ((>) d1 y z) = ...
-because that will only match if the dict args are (visibly) equal.
-Instead we want to quantify over the dictionaries separately.
-
-In short, simplifyRuleLhs must *only* squash equalities, leaving
-all dicts unchanged, with absolutely no sharing.
-
-Also note that we can't solve the LHS constraints in isolation:
-Example foo :: Ord a => a -> a
- foo_spec :: Int -> Int
- {-# RULE "foo" foo = foo_spec #-}
-Here, it's the RHS that fixes the type variable
-
-HOWEVER, under a nested implication things are different
-Consider
- f :: (forall a. Eq a => a->a) -> Bool -> ...
- {-# RULES "foo" forall (v::forall b. Eq b => b->b).
- f b True = ...
- #-}
-Here we *must* solve the wanted (Eq a) from the given (Eq a)
-resulting from skolemising the argument type of g. So we
-revert to SimplCheck when going under an implication.
-
-
---------- So the SimplifyRule Plan is this -----------------------
-
-* Step 0: typecheck the LHS and RHS to get constraints from each
-
-* Step 1: Simplify the LHS and RHS constraints all together in one bag,
- but /discarding/ the simplified constraints. We do this only
- to discover all unification equalities.
-
-* Step 2: Zonk the ORIGINAL (unsimplified) LHS constraints, to take
- advantage of those unifications
-
-* Setp 3: Partition the LHS constraints into the ones we will
- quantify over, and the others.
- See Note [RULE quantification over equalities]
-
-* Step 4: Decide on the type variables to quantify over
-
-* Step 5: Simplify the LHS and RHS constraints separately, using the
- quantified constraints as givens
-
-Note [Solve order for RULES]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In step 1 above, we need to be a bit careful about solve order.
-Consider
- f :: Int -> T Int
- type instance T Int = Bool
-
- RULE f 3 = True
-
-From the RULE we get
- lhs-constraints: T Int ~ alpha
- rhs-constraints: Bool ~ alpha
-where 'alpha' is the type that connects the two. If we glom them
-all together, and solve the RHS constraint first, we might solve
-with alpha := Bool. But then we'd end up with a RULE like
-
- RULE: f 3 |> (co :: T Int ~ Bool) = True
-
-which is terrible. We want
-
- RULE: f 3 = True |> (sym co :: Bool ~ T Int)
-
-So we are careful to solve the LHS constraints first, and *then* the
-RHS constraints. Actually much of this is done by the on-the-fly
-constraint solving, so the same order must be observed in
-tcRule.
-
-
-Note [RULE quantification over equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Deciding which equalities to quantify over is tricky:
- * We do not want to quantify over insoluble equalities (Int ~ Bool)
- (a) because we prefer to report a LHS type error
- (b) because if such things end up in 'givens' we get a bogus
- "inaccessible code" error
-
- * But we do want to quantify over things like (a ~ F b), where
- F is a type function.
-
-The difficulty is that it's hard to tell what is insoluble!
-So we see whether the simplification step yielded any type errors,
-and if so refrain from quantifying over *any* equalities.
-
-Note [Quantifying over coercion holes]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Equality constraints from the LHS will emit coercion hole Wanteds.
-These don't have a name, so we can't quantify over them directly.
-Instead, because we really do want to quantify here, invent a new
-EvVar for the coercion, fill the hole with the invented EvVar, and
-then quantify over the EvVar. Not too tricky -- just some
-impedance matching, really.
-
-Note [Simplify cloned constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-At this stage, we're simplifying constraints only for insolubility
-and for unification. Note that all the evidence is quickly discarded.
-We use a clone of the real constraint. If we don't do this,
-then RHS coercion-hole constraints get filled in, only to get filled
-in *again* when solving the implications emitted from tcRule. That's
-terrible, so we avoid the problem by cloning the constraints.
-
--}
-
-simplifyRule :: RuleName
- -> TcLevel -- Level at which to solve the constraints
- -> WantedConstraints -- Constraints from LHS
- -> WantedConstraints -- Constraints from RHS
- -> TcM ( [EvVar] -- Quantify over these LHS vars
- , WantedConstraints -- Residual un-quantified LHS constraints
- , TcTyVarSet ) -- Don't default these
--- See Note [The SimplifyRule Plan]
--- NB: This consumes all simple constraints on the LHS, but not
--- any LHS implication constraints.
-simplifyRule name tc_lvl lhs_wanted rhs_wanted
- = do {
- -- Note [The SimplifyRule Plan] step 1
- -- First solve the LHS and *then* solve the RHS
- -- Crucially, this performs unifications
- -- Why clone? See Note [Simplify cloned constraints]
- ; lhs_clone <- cloneWC lhs_wanted
- ; rhs_clone <- cloneWC rhs_wanted
- ; (dont_default, _)
- <- setTcLevel tc_lvl $
- runTcS $
- do { lhs_wc <- solveWanteds lhs_clone
- ; _rhs_wc <- solveWanteds rhs_clone
- -- Why do them separately?
- -- See Note [Solve order for RULES]
-
- ; let dont_default = nonDefaultableTyVarsOfWC lhs_wc
- -- If lhs_wanteds has
- -- (a[sk] :: TYPE rr[sk]) ~ (b0[tau] :: TYPE r0[conc])
- -- we want r0 to be non-defaultable;
- -- see nonDefaultableTyVarsOfWC. Simplest way to get
- -- this is to look at the post-simplified lhs_wc, which
- -- will contain (rr[sk] ~ r0[conc)]. An example is in
- -- test rep-poly/RepPolyRule1
- ; return dont_default }
-
- -- Note [The SimplifyRule Plan] step 2
- ; lhs_wanted <- liftZonkM $ zonkWC lhs_wanted
- ; let (quant_cts, residual_lhs_wanted) = getRuleQuantCts lhs_wanted
-
- -- Note [The SimplifyRule Plan] step 3
- ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
-
- ; traceTc "simplifyRule" $
- vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
- , text "lhs_wanted" <+> ppr lhs_wanted
- , text "rhs_wanted" <+> ppr rhs_wanted
- , text "quant_cts" <+> ppr quant_cts
- , text "residual_lhs_wanted" <+> ppr residual_lhs_wanted
- , text "dont_default" <+> ppr dont_default
- ]
-
- ; return (quant_evs, residual_lhs_wanted, dont_default) }
-
- where
- mk_quant_ev :: Ct -> TcM EvVar
- mk_quant_ev ct
- | CtWanted { ctev_dest = dest, ctev_pred = pred } <- ctEvidence ct
- = case dest of
- EvVarDest ev_id -> return ev_id
- HoleDest hole -> -- See Note [Quantifying over coercion holes]
- do { ev_id <- newEvVar pred
- ; fillCoercionHole hole (mkCoVarCo ev_id)
- ; return ev_id }
- mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct)
-
-
-getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
--- Extract all the constraints we can quantify over,
--- also returning the depleted WantedConstraints
---
--- NB: we must look inside implications, because with
--- -fdefer-type-errors we generate implications rather eagerly;
--- see GHC.Tc.Utils.Unify.implicationNeeded. Not doing so caused #14732.
---
--- Unlike simplifyInfer, we don't leave the WantedConstraints unchanged,
--- and attempt to solve them from the quantified constraints. That
--- nearly works, but fails for a constraint like (d :: Eq Int).
--- We /do/ want to quantify over it, but the short-cut solver
--- (see GHC.Tc.Solver.Dict Note [Shortcut solving]) ignores the quantified
--- and instead solves from the top level.
---
--- So we must partition the WantedConstraints ourselves
--- Not hard, but tiresome.
-
-getRuleQuantCts wc
- = float_wc emptyVarSet wc
- where
- float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
- float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics, wc_errors = errs })
- = ( simple_yes `andCts` implic_yes
- , emptyWC { wc_simple = simple_no, wc_impl = implics_no, wc_errors = errs })
- where
- (simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples
- (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs)
- emptyBag implics
-
- float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
- float_implic skol_tvs yes1 imp
- = (yes1 `andCts` yes2, imp { ic_wanted = no })
- where
- (yes2, no) = float_wc new_skol_tvs (ic_wanted imp)
- new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp
-
- rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
- rule_quant_ct skol_tvs ct = case classifyPredType (ctPred ct) of
- EqPred _ t1 t2
- | not (ok_eq t1 t2)
- -> False -- Note [RULE quantification over equalities]
- _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs
-
- ok_eq t1 t2
- | t1 `tcEqType` t2 = False
- | otherwise = is_fun_app t1 || is_fun_app t2
-
- is_fun_app ty -- ty is of form (F tys) where F is a type function
- = case tyConAppTyCon_maybe ty of
- Just tc -> isTypeFamilyTyCon tc
- Nothing -> False
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -22,7 +22,9 @@ module GHC.Tc.Gen.Sig(
TcPragEnv, emptyPragEnv, lookupPragEnv, extendPragEnv,
mkPragEnv, tcSpecPrags, tcSpecWrapper, tcImpPrags,
- addInlinePrags, addInlinePragArity
+ addInlinePrags, addInlinePragArity,
+
+ tcRules
) where
import GHC.Prelude
@@ -33,14 +35,13 @@ import GHC.Driver.Backend
import GHC.Hs
-
import GHC.Tc.Errors.Types ( FixedRuntimeRepProvenance(..), TcRnMessage(..) )
import GHC.Tc.Gen.HsType
-import GHC.Tc.Types
import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.TcMType ( checkTypeHasFixedRuntimeRep )
import GHC.Tc.Zonk.Type
+import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType
import GHC.Tc.Validity ( checkValidType )
@@ -825,16 +826,37 @@ tcSpecPrag poly_id prag@(SpecSig _ fun_name hs_tys inl)
; wrap <- tcSpecWrapper (FunSigCtxt name (lhsSigTypeContextSpan hs_ty)) poly_ty spec_ty
; return (SpecPrag poly_id wrap inl) }
--- Example: {-# SPECIALISE f True #-}
--- We typecheck, and generate (SpecPragE (f ())
+-- Example: f :: forall a. Ord a => a -> Bool -> blah
+-- {-# SPECIALISE forall x. f (x::Int) True #-}
+-- We typecheck, and generate (SpecPragE [x] (f @Int dOrdInt x True))
-- Then when desugaring we generate
--- $sf = (\f. f True) <f-rhs>
--- RULE f True =
-
-tcSpecPrag poly_id prag@(SpecSigE nm spec_e inl)
- = do { (spec_e', _rho) <- tcInferRhow spec_e
- ; return (SpecPragE spec_e' inl) }
-
+-- $sf x = <f-rhs> @Int dOrdInt x True
+-- RULE forall d x. f @Int d x True = $sf x
+-- The thing in the SpecPragE is very very like the LHS of a RULE
+
+tcSpecPrag poly_id prag@(SpecSigE nm bndrs spec_e inl)
+ = do { (tc_lvl, wanted, (id_bndrs, spec_e', rho))
+ <- pushLevelAndCaptureConstraints $
+ do { (tv_bndrs, id_bndrs) <- tcRuleBndrs rule_name bndrs
+ ; tcExtendNameTyVarEnv [(tyVarName tv, tv) | tv <- tv_bndrs] $
+ tcExtendIdEnv id_bndrs $
+ do { (spec_e', rho) <- tcInferRho spec_e
+ ; return (id_bndrs, spec_e', rho) } }
+
+ ; _ <- setTcLevel tc_lvl $ runTcS $ solveWanteds wanteds
+ ; wanted <- liftZonkM $ zonkWC wanted
+
+ ; let (quant_cts, residual_wanted) = getRuleQuantCts wanted
+ ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
+ ; let tpl_ids = quant_evs ++ id_bndrs
+ ; forall_tkvs <- candidateQTyVarsOfTypes (rho : map idType tpl_ids)
+ ; skol_info <- mkSkolemInfo (RuleSkol nm)
+ ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars forall_tkvs
+ ; (implic, ev_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
+ quant_evs residual_wanted
+ ; emitImplication implic
+ ; return (SpecPragE (mkTcRuleBndrs bndrs (qtkvs ++ tpl_ids)
+ spec_e' inl)) }
tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
@@ -904,3 +926,487 @@ longer has an unfolding in the future. But then you'll get a helpful
error message suggesting an INLINABLE pragma, which you can follow.
That seems enough for now.
-}
+
+
+{- *********************************************************************
+* *
+ Rules
+* *
+************************************************************************
+
+Note [Typechecking rules]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+We *infer* the typ of the LHS, and use that type to *check* the type of
+the RHS. That means that higher-rank rules work reasonably well. Here's
+an example (test simplCore/should_compile/rule2.hs) produced by Roman:
+
+ foo :: (forall m. m a -> m b) -> m a -> m b
+ foo f = ...
+
+ bar :: (forall m. m a -> m a) -> m a -> m a
+ bar f = ...
+
+ {-# RULES "foo/bar" foo = bar #-}
+
+He wanted the rule to typecheck.
+
+Note [TcLevel in type checking rules]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Bringing type variables into scope naturally bumps the TcLevel. Thus, we type
+check the term-level binders in a bumped level, and we must accordingly bump
+the level whenever these binders are in scope.
+
+Note [Re-quantify type variables in rules]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this example from #17710:
+
+ foo :: forall k (a :: k) (b :: k). Proxy a -> Proxy b
+ foo x = Proxy
+ {-# RULES "foo" forall (x :: Proxy (a :: k)). foo x = Proxy #-}
+
+Written out in more detail, the "foo" rewrite rule looks like this:
+
+ forall k (a :: k). forall (x :: Proxy (a :: k)). foo @k @a @b0 x = Proxy @k @b0
+
+Where b0 is a unification variable. Where should b0 be quantified? We have to
+quantify it after k, since (b0 :: k). But generalization usually puts inferred
+type variables (such as b0) at the /front/ of the telescope! This creates a
+conflict.
+
+One option is to simply throw an error, per the principles of
+Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType. This is what would happen
+if we were generalising over a normal type signature. On the other hand, the
+types in a rewrite rule aren't quite "normal", since the notions of specified
+and inferred type variables aren't applicable.
+
+A more permissive design (and the design that GHC uses) is to simply requantify
+all of the type variables. That is, we would end up with this:
+
+ forall k (a :: k) (b :: k). forall (x :: Proxy (a :: k)). foo @k @a @b x = Proxy @k @b
+
+It's a bit strange putting the generalized variable `b` after the user-written
+variables `k` and `a`. But again, the notion of specificity is not relevant to
+rewrite rules, since one cannot "visibly apply" a rewrite rule. This design not
+only makes "foo" typecheck, but it also makes the implementation simpler.
+
+See also Note [Generalising in tcTyFamInstEqnGuts] in GHC.Tc.TyCl, which
+explains a very similar design when generalising over a type family instance
+equation.
+-}
+
+tcRules :: [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTc]
+tcRules decls = mapM (wrapLocMA tcRuleDecls) decls
+
+tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
+tcRuleDecls (HsRules { rds_ext = src
+ , rds_rules = decls })
+ = do { tc_decls <- mapM (wrapLocMA tcRule) decls
+ ; return $ HsRules { rds_ext = src
+ , rds_rules = tc_decls } }
+
+tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
+tcRule (HsRule { rd_ext = ext
+ , rd_name = rname@(L _ name)
+ , rd_act = act
+ , rd_bndrs = bndrs
+ , rd_lhs = lhs
+ , rd_rhs = rhs })
+ = addErrCtxt (ruleCtxt name) $
+ do { traceTc "---- Rule ------" (pprFullRuleName (snd ext) rname)
+ ; skol_info <- mkSkolemInfo (RuleSkol name)
+ -- Note [Typechecking rules]
+ ; (tc_lvl, stuff) <- pushTcLevelM $
+ generateRuleConstraints name bndrs lhs rhs
+
+ ; let (id_bndrs, lhs', lhs_wanted
+ , rhs', rhs_wanted, rule_ty) = stuff
+
+ ; traceTc "tcRule 1" (vcat [ pprFullRuleName (snd ext) rname
+ , ppr lhs_wanted
+ , ppr rhs_wanted ])
+
+ ; (lhs_evs, residual_lhs_wanted, dont_default)
+ <- simplifyRule name tc_lvl lhs_wanted rhs_wanted
+
+ -- SimplifyRule Plan, step 4
+ -- Now figure out what to quantify over
+ -- c.f. GHC.Tc.Solver.simplifyInfer
+ -- We quantify over any tyvars free in *either* the rule
+ -- *or* the bound variables. The latter is important. Consider
+ -- ss (x,(y,z)) = (x,z)
+ -- RULE: forall v. fst (ss v) = fst v
+ -- The type of the rhs of the rule is just a, but v::(a,(b,c))
+ --
+ -- We also need to get the completely-unconstrained tyvars of
+ -- the LHS, lest they otherwise get defaulted to Any; but we do that
+ -- during zonking (see GHC.Tc.Zonk.Type.zonkRule)
+
+ ; let tpl_ids = lhs_evs ++ id_bndrs
+
+ -- See Note [Re-quantify type variables in rules]
+ ; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids)
+ ; let weed_out = (`dVarSetMinusVarSet` dont_default)
+ quant_cands = forall_tkvs { dv_kvs = weed_out (dv_kvs forall_tkvs)
+ , dv_tvs = weed_out (dv_tvs forall_tkvs) }
+ ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars quant_cands
+ ; traceTc "tcRule" (vcat [ pprFullRuleName (snd ext) rname
+ , text "forall_tkvs:" <+> ppr forall_tkvs
+ , text "quant_cands:" <+> ppr quant_cands
+ , text "dont_default:" <+> ppr dont_default
+ , text "residual_lhs_wanted:" <+> ppr residual_lhs_wanted
+ , text "qtkvs:" <+> ppr qtkvs
+ , text "rule_ty:" <+> ppr rule_ty
+ , text "ty_bndrs:" <+> ppr ty_bndrs
+ , text "qtkvs ++ tpl_ids:" <+> ppr (qtkvs ++ tpl_ids)
+ , text "tpl_id info:" <+>
+ vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
+ ])
+
+ -- SimplfyRule Plan, step 5
+ -- Simplify the LHS and RHS constraints:
+ -- For the LHS constraints we must solve the remaining constraints
+ -- (a) so that we report insoluble ones
+ -- (b) so that we bind any soluble ones
+ ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
+ lhs_evs residual_lhs_wanted
+ ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
+ lhs_evs rhs_wanted
+ ; emitImplications (lhs_implic `unionBags` rhs_implic)
+ ; return $ HsRule { rd_ext = ext
+ , rd_name = rname
+ , rd_act = act
+ , rd_bnrs = mkTcRuleBndrs bndrs (qtkvs ++ tpl_ids)
+ , rd_lhs = mkHsDictLet lhs_binds lhs'
+ , rd_rhs = mkHsDictLet rhs_binds rhs' } }
+
+mkTcRuleBndrs :: RuleBndrs GhcRn -> [Var] -> RuleBndrs GHCTc
+mkTcRuleBndrs (RuleBndrs { rb_tyvs = tyvs }) vars
+ = RuleBndrs { rb_tyvs = tyvs -- preserved for ppr-ing
+ , rb_tmvs = map (noLocA . RuleBndr noAnn . noLocA) vars }
+
+generateRuleConstraints :: FastString
+ -> RuleBndrs GhcRn
+ -> LHsExpr GhcRn -> LHsExpr GhcRn
+ -> TcM ( [TcId]
+ , LHsExpr GhcTc, WantedConstraints
+ , LHsExpr GhcTc, WantedConstraints
+ , TcType )
+generateRuleConstraints rule_namebndrs lhs rhs
+ = do { ((tv_bndrs, id_bndrs), bndr_wanted) <- captureConstraints $
+ tcRuleBndrs rule_name bndrs
+ -- bndr_wanted constraints can include wildcard hole
+ -- constraints, which we should not forget about.
+ -- It may mention the skolem type variables bound by
+ -- the RULE. c.f. #10072
+ ; tcExtendNameTyVarEnv [(tyVarName tv, tv) | tv <- tv_bndrs] $
+ tcExtendIdEnv id_bndrs $
+ do { -- See Note [Solve order for RULES]
+ ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
+ ; (rhs', rhs_wanted) <- captureConstraints $
+ tcCheckMonoExpr rhs rule_ty
+ ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
+ ; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
+
+
+ruleCtxt :: FastString -> SDoc
+ruleCtxt name = text "When checking the rewrite rule" <+>
+ doubleQuotes (ftext name)
+
+
+-- See Note [TcLevel in type checking rules]
+tcRuleBndrs :: RuleName -> RuleBndrs GhcRn
+ -> TcM ([TcTyVar], [Id])
+tcRuleBndrs rule_name (RuleBndrs { rb_tyvs = mb_tv_bndrs, rb_tmvs = tmvs })) xs
+ | Just tv_bndrs <- mb_tv_bndrs
+ = do { skol_info <- mkSkolemInfo (RuleSkol rule_name)
+ ; (tybndrs1,(tys2,tms)) <- bindExplicitTKBndrs_Skol skol_info tv_bndrs $
+ tcRuleTmBndrs rule_name tmvs
+ ; let tys1 = binderVars tybndrs1
+ ; return (tys1 ++ tys2, tms) }
+
+ | otherwise
+ = tcRuleTmBndrs rule_name xs
+
+-- See Note [TcLevel in type checking rules]
+tcRuleTmBndrs :: FastString -> [LRuleBndr GhcRn] -> TcM ([TcTyVar],[Id])
+tcRuleTmBndrs _ [] = return ([],[])
+tcRuleTmBndrs rule_name (L _ (RuleBndr _ (L _ name)) : rule_bndrs)
+ = do { ty <- newOpenFlexiTyVarTy
+ ; (tyvars, tmvars) <- tcRuleTmBndrs rule_name rule_bndrs
+ ; return (tyvars, mkLocalId name ManyTy ty : tmvars) }
+tcRuleTmBndrs rule_name (L _ (RuleBndrSig _ (L _ name) rn_ty) : rule_bndrs)
+-- e.g x :: a->a
+-- The tyvar 'a' is brought into scope first, just as if you'd written
+-- a::*, x :: a->a
+-- If there's an explicit forall, the renamer would have already reported an
+-- error for each out-of-scope type variable used
+ = do { let ctxt = RuleSigCtxt rule_name name
+ ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt HM_Sig rn_ty OpenKind
+ ; let id = mkLocalId name ManyTy id_ty
+ -- See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType
+
+ -- The type variables scope over subsequent bindings; yuk
+ ; (tyvars, tmvars) <- tcExtendNameTyVarEnv tvs $
+ tcRuleTmBndrs rule_name rule_bndrs
+ ; return (map snd tvs ++ tyvars, id : tmvars) }
+
+{-
+*********************************************************************************
+* *
+ Constraint simplification for rules
+* *
+***********************************************************************************
+
+Note [The SimplifyRule Plan]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Example. Consider the following left-hand side of a rule
+ f (x == y) (y > z) = ...
+If we typecheck this expression we get constraints
+ d1 :: Ord a, d2 :: Eq a
+We do NOT want to "simplify" to the LHS
+ forall x::a, y::a, z::a, d1::Ord a.
+ f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
+Instead we want
+ forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
+ f ((==) d2 x y) ((>) d1 y z) = ...
+
+Here is another example:
+ fromIntegral :: (Integral a, Num b) => a -> b
+ {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
+In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
+we *dont* want to get
+ forall dIntegralInt.
+ fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
+because the scsel will mess up RULE matching. Instead we want
+ forall dIntegralInt, dNumInt.
+ fromIntegral Int Int dIntegralInt dNumInt = id Int
+
+Even if we have
+ g (x == y) (y == z) = ..
+where the two dictionaries are *identical*, we do NOT WANT
+ forall x::a, y::a, z::a, d1::Eq a
+ f ((==) d1 x y) ((>) d1 y z) = ...
+because that will only match if the dict args are (visibly) equal.
+Instead we want to quantify over the dictionaries separately.
+
+In short, simplifyRuleLhs must *only* squash equalities, leaving
+all dicts unchanged, with absolutely no sharing.
+
+Also note that we can't solve the LHS constraints in isolation:
+Example foo :: Ord a => a -> a
+ foo_spec :: Int -> Int
+ {-# RULE "foo" foo = foo_spec #-}
+Here, it's the RHS that fixes the type variable
+
+HOWEVER, under a nested implication things are different
+Consider
+ f :: (forall a. Eq a => a->a) -> Bool -> ...
+ {-# RULES "foo" forall (v::forall b. Eq b => b->b).
+ f b True = ...
+ #-}
+Here we *must* solve the wanted (Eq a) from the given (Eq a)
+resulting from skolemising the argument type of g. So we
+revert to SimplCheck when going under an implication.
+
+
+--------- So the SimplifyRule Plan is this -----------------------
+
+* Step 0: typecheck the LHS and RHS to get constraints from each
+
+* Step 1: Simplify the LHS and RHS constraints all together in one bag,
+ but /discarding/ the simplified constraints. We do this only
+ to discover all unification equalities.
+
+* Step 2: Zonk the ORIGINAL (unsimplified) LHS constraints, to take
+ advantage of those unifications
+
+* Setp 3: Partition the LHS constraints into the ones we will
+ quantify over, and the others.
+ See Note [RULE quantification over equalities]
+
+* Step 4: Decide on the type variables to quantify over
+
+* Step 5: Simplify the LHS and RHS constraints separately, using the
+ quantified constraints as givens
+
+Note [Solve order for RULES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In step 1 above, we need to be a bit careful about solve order.
+Consider
+ f :: Int -> T Int
+ type instance T Int = Bool
+
+ RULE f 3 = True
+
+From the RULE we get
+ lhs-constraints: T Int ~ alpha
+ rhs-constraints: Bool ~ alpha
+where 'alpha' is the type that connects the two. If we glom them
+all together, and solve the RHS constraint first, we might solve
+with alpha := Bool. But then we'd end up with a RULE like
+
+ RULE: f 3 |> (co :: T Int ~ Bool) = True
+
+which is terrible. We want
+
+ RULE: f 3 = True |> (sym co :: Bool ~ T Int)
+
+So we are careful to solve the LHS constraints first, and *then* the
+RHS constraints. Actually much of this is done by the on-the-fly
+constraint solving, so the same order must be observed in
+tcRule.
+
+
+Note [RULE quantification over equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Deciding which equalities to quantify over is tricky:
+ * We do not want to quantify over insoluble equalities (Int ~ Bool)
+ (a) because we prefer to report a LHS type error
+ (b) because if such things end up in 'givens' we get a bogus
+ "inaccessible code" error
+
+ * But we do want to quantify over things like (a ~ F b), where
+ F is a type function.
+
+The difficulty is that it's hard to tell what is insoluble!
+So we see whether the simplification step yielded any type errors,
+and if so refrain from quantifying over *any* equalities.
+
+Note [Quantifying over coercion holes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Equality constraints from the LHS will emit coercion hole Wanteds.
+These don't have a name, so we can't quantify over them directly.
+Instead, because we really do want to quantify here, invent a new
+EvVar for the coercion, fill the hole with the invented EvVar, and
+then quantify over the EvVar. Not too tricky -- just some
+impedance matching, really.
+
+Note [Simplify cloned constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+At this stage, we're simplifying constraints only for insolubility
+and for unification. Note that all the evidence is quickly discarded.
+We use a clone of the real constraint. If we don't do this,
+then RHS coercion-hole constraints get filled in, only to get filled
+in *again* when solving the implications emitted from tcRule. That's
+terrible, so we avoid the problem by cloning the constraints.
+
+-}
+
+simplifyRule :: RuleName
+ -> TcLevel -- Level at which to solve the constraints
+ -> WantedConstraints -- Constraints from LHS
+ -> WantedConstraints -- Constraints from RHS
+ -> TcM ( [EvVar] -- Quantify over these LHS vars
+ , WantedConstraints -- Residual un-quantified LHS constraints
+ , TcTyVarSet ) -- Don't default these
+-- See Note [The SimplifyRule Plan]
+-- NB: This consumes all simple constraints on the LHS, but not
+-- any LHS implication constraints.
+simplifyRule name tc_lvl lhs_wanted rhs_wanted
+ = do {
+ -- Note [The SimplifyRule Plan] step 1
+ -- First solve the LHS and *then* solve the RHS
+ -- Crucially, this performs unifications
+ -- Why clone? See Note [Simplify cloned constraints]
+ ; lhs_clone <- cloneWC lhs_wanted
+ ; rhs_clone <- cloneWC rhs_wanted
+ ; (dont_default, _)
+ <- setTcLevel tc_lvl $
+ runTcS $
+ do { lhs_wc <- solveWanteds lhs_clone
+ ; _rhs_wc <- solveWanteds rhs_clone
+ -- Why do them separately?
+ -- See Note [Solve order for RULES]
+
+ ; let dont_default = nonDefaultableTyVarsOfWC lhs_wc
+ -- If lhs_wanteds has
+ -- (a[sk] :: TYPE rr[sk]) ~ (b0[tau] :: TYPE r0[conc])
+ -- we want r0 to be non-defaultable;
+ -- see nonDefaultableTyVarsOfWC. Simplest way to get
+ -- this is to look at the post-simplified lhs_wc, which
+ -- will contain (rr[sk] ~ r0[conc)]. An example is in
+ -- test rep-poly/RepPolyRule1
+ ; return dont_default }
+
+ -- Note [The SimplifyRule Plan] step 2
+ ; lhs_wanted <- liftZonkM $ zonkWC lhs_wanted
+ ; let (quant_cts, residual_lhs_wanted) = getRuleQuantCts lhs_wanted
+
+ -- Note [The SimplifyRule Plan] step 3
+ ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
+
+ ; traceTc "simplifyRule" $
+ vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
+ , text "lhs_wanted" <+> ppr lhs_wanted
+ , text "rhs_wanted" <+> ppr rhs_wanted
+ , text "quant_cts" <+> ppr quant_cts
+ , text "residual_lhs_wanted" <+> ppr residual_lhs_wanted
+ , text "dont_default" <+> ppr dont_default
+ ]
+
+ ; return (quant_evs, residual_lhs_wanted, dont_default) }
+
+mk_quant_ev :: Ct -> TcM EvVar
+mk_quant_ev ct
+ | CtWanted { ctev_dest = dest, ctev_pred = pred } <- ctEvidence ct
+ = case dest of
+ EvVarDest ev_id -> return ev_id
+ HoleDest hole -> -- See Note [Quantifying over coercion holes]
+ do { ev_id <- newEvVar pred
+ ; fillCoercionHole hole (mkCoVarCo ev_id)
+ ; return ev_id }
+mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct)
+
+
+getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
+-- Extract all the constraints we can quantify over,
+-- also returning the depleted WantedConstraints
+--
+-- NB: we must look inside implications, because with
+-- -fdefer-type-errors we generate implications rather eagerly;
+-- see GHC.Tc.Utils.Unify.implicationNeeded. Not doing so caused #14732.
+--
+-- Unlike simplifyInfer, we don't leave the WantedConstraints unchanged,
+-- and attempt to solve them from the quantified constraints. That
+-- nearly works, but fails for a constraint like (d :: Eq Int).
+-- We /do/ want to quantify over it, but the short-cut solver
+-- (see GHC.Tc.Solver.Dict Note [Shortcut solving]) ignores the quantified
+-- and instead solves from the top level.
+--
+-- So we must partition the WantedConstraints ourselves
+-- Not hard, but tiresome.
+
+getRuleQuantCts wc
+ = float_wc emptyVarSet wc
+ where
+ float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
+ float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics, wc_errors = errs })
+ = ( simple_yes `andCts` implic_yes
+ , emptyWC { wc_simple = simple_no, wc_impl = implics_no, wc_errors = errs })
+ where
+ (simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples
+ (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs)
+ emptyBag implics
+
+ float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
+ float_implic skol_tvs yes1 imp
+ = (yes1 `andCts` yes2, imp { ic_wanted = no })
+ where
+ (yes2, no) = float_wc new_skol_tvs (ic_wanted imp)
+ new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp
+
+ rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
+ rule_quant_ct skol_tvs ct = case classifyPredType (ctPred ct) of
+ EqPred _ t1 t2
+ | not (ok_eq t1 t2)
+ -> False -- Note [RULE quantification over equalities]
+ _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+
+ ok_eq t1 t2
+ | t1 `tcEqType` t2 = False
+ | otherwise = is_fun_app t1 || is_fun_app t2
+
+ is_fun_app ty -- ty is of form (F tys) where F is a type function
+ = case tyConAppTyCon_maybe ty of
+ Just tc -> isTypeFamilyTyCon tc
+ Nothing -> False
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -71,7 +71,7 @@ import GHC.Tc.Gen.Annotation
import GHC.Tc.Gen.Bind
import GHC.Tc.Gen.Default
import GHC.Tc.Utils.Env
-import GHC.Tc.Gen.Rule
+import GHC.Tc.Gen.Sig( tcRules )
import GHC.Tc.Gen.Foreign
import GHC.Tc.TyCl.Instance
import GHC.Tc.Utils.TcMType
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -3319,7 +3319,7 @@ without treating the explicitly-quantified ones specially. Wrinkles:
no role.
See also Note [Re-quantify type variables in rules] in
-GHC.Tc.Gen.Rule, which explains a /very/ similar design when
+GHC.Tc.Gen.Sig, which explains a /very/ similar design when
generalising over the type of a rewrite rule.
-}
=====================================
compiler/Language/Haskell/Syntax/Binds.hs
=====================================
@@ -445,6 +445,7 @@ data Sig pass
-- SPECIALISE, not SPECIALISE_INLINE
| SpecSigE (XSpecSigE pass)
+ (RuleBndrs pass)
(LHsExpr pass) -- Expression to specialise
InlinePragma
-- The expression should be of form
=====================================
compiler/Language/Haskell/Syntax/Decls.hs
=====================================
@@ -1635,14 +1635,10 @@ data RuleDecl pass
-- ^ After renamer, free-vars from the LHS and RHS
, rd_name :: XRec pass RuleName
-- ^ Note [Pragma source text] in "GHC.Types.SourceText"
- , rd_act :: Activation
- , rd_tyvs :: Maybe [LHsTyVarBndr () (NoGhcTc pass)]
- -- ^ Forall'd type vars
- , rd_tmvs :: [LRuleBndr pass]
- -- ^ Forall'd term vars, before typechecking; after typechecking
- -- this includes all forall'd vars
- , rd_lhs :: XRec pass (HsExpr pass)
- , rd_rhs :: XRec pass (HsExpr pass)
+ , rd_bndrs :: RuleBndrs pass
+ , rd_act :: Activation
+ , rd_lhs :: XRec pass (HsExpr pass)
+ , rd_rhs :: XRec pass (HsExpr pass)
}
-- ^
-- - 'GHC.Parser.Annotation.AnnKeywordId' :
@@ -1653,12 +1649,20 @@ data RuleDecl pass
-- 'GHC.Parser.Annotation.AnnEqual',
| XRuleDecl !(XXRuleDecl pass)
+data RuleBndrs pass = RuleBndrs
+ { rb_tyvs :: Maybe [LHsTyVarBndr () (NoGhcTc pass)]
+ -- ^ Forall'd type vars
+ , rb_tmvs :: [LRuleBndr pass]
+ -- ^ Forall'd term vars, before typechecking;
+ -- after typechecking this includes all forall'd vars
+ }
+
-- | Located Rule Binder
type LRuleBndr pass = XRec pass (RuleBndr pass)
-- | Rule Binder
data RuleBndr pass
- = RuleBndr (XCRuleBndr pass) (LIdP pass)
+ = RuleBndr (XCRuleBndr pass) (LIdP pass)
| RuleBndrSig (XRuleBndrSig pass) (LIdP pass) (HsPatSigType pass)
| XRuleBndr !(XXRuleBndr pass)
-- ^
=====================================
compiler/ghc.cabal.in
=====================================
@@ -768,7 +768,6 @@ Library
GHC.Tc.Gen.HsType
GHC.Tc.Gen.Match
GHC.Tc.Gen.Pat
- GHC.Tc.Gen.Rule
GHC.Tc.Gen.Sig
GHC.Tc.Gen.Splice
GHC.Tc.Instance.Class
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2a909abd65d094d2448b0c5ab74ea0e25d5cff31
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2a909abd65d094d2448b0c5ab74ea0e25d5cff31
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/20240208/e4970f32/attachment-0001.html>
More information about the ghc-commits
mailing list