diff options
| -rw-r--r-- | compiler/typecheck/TcRules.hs | 62 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 3 | ||||
| -rw-r--r-- | testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr | 10 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T17710.hs | 15 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
5 files changed, 67 insertions, 24 deletions
diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs index e63e670e03..76b1c651ad 100644 --- a/compiler/typecheck/TcRules.hs +++ b/compiler/typecheck/TcRules.hs @@ -60,6 +60,43 @@ 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 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 TcTyClsDecls, which +explains a very similar design when generalising over a type family instance +equation. -} tcRules :: [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTcId] @@ -89,8 +126,8 @@ tcRule (HsRule { rd_ext = ext ; (tc_lvl, stuff) <- pushTcLevelM $ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs - ; let (tv_bndrs, id_bndrs, lhs', lhs_wanted - , rhs', rhs_wanted, rule_ty) = stuff + ; let (id_bndrs, lhs', lhs_wanted + , rhs', rhs_wanted, rule_ty) = stuff ; traceTc "tcRule 1" (vcat [ pprFullRuleName rname , ppr lhs_wanted @@ -113,14 +150,13 @@ tcRule (HsRule { rd_ext = ext -- during zonking (see TcHsSyn.zonkRule) ; let tpl_ids = lhs_evs ++ id_bndrs - ; forall_tkvs <- candidateQTyVarsOfTypes $ - map (mkSpecForAllTys tv_bndrs) $ -- don't quantify over lexical tyvars - rule_ty : map idType tpl_ids + + -- See Note [Re-quantify type variables in rules] + ; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids) ; qtkvs <- quantifyTyVars forall_tkvs ; traceTc "tcRule" (vcat [ pprFullRuleName rname , ppr forall_tkvs , ppr qtkvs - , ppr tv_bndrs , ppr rule_ty , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ] ]) @@ -130,11 +166,10 @@ tcRule (HsRule { rd_ext = ext -- 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 - ; let all_qtkvs = qtkvs ++ tv_bndrs - skol_info = RuleSkol name - ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info all_qtkvs + ; let skol_info = RuleSkol name + ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs lhs_evs residual_lhs_wanted - ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info all_qtkvs + ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs lhs_evs rhs_wanted ; emitImplications (lhs_implic `unionBags` rhs_implic) @@ -143,15 +178,14 @@ tcRule (HsRule { rd_ext = ext , rd_act = act , rd_tyvs = ty_bndrs -- preserved for ppr-ing , rd_tmvs = map (noLoc . RuleBndr noExtField . noLoc) - (all_qtkvs ++ tpl_ids) + (qtkvs ++ tpl_ids) , rd_lhs = mkHsDictLet lhs_binds lhs' , rd_rhs = mkHsDictLet rhs_binds rhs' } } tcRule (XRuleDecl nec) = noExtCon nec generateRuleConstraints :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn] -> LHsExpr GhcRn -> LHsExpr GhcRn - -> TcM ( [TyVar] - , [TcId] + -> TcM ( [TcId] , LHsExpr GhcTc, WantedConstraints , LHsExpr GhcTc, WantedConstraints , TcType ) @@ -170,7 +204,7 @@ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs ; (rhs', rhs_wanted) <- captureConstraints $ tcMonoExpr rhs (mkCheckExpType rule_ty) ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted - ; return (tv_bndrs, id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } } + ; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } } -- See Note [TcLevel in type checking rules] tcRuleBndrs :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn] diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index e712f79e1d..fff1376807 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -2669,6 +2669,9 @@ Hence the slightly mysterious call: candidateQTyVarsOfTypes (pats ++ mkTyVarTys scoped_tvs) Simple, neat, but a little non-obvious! + +See also Note [Re-quantify type variables in rules] in TcRules, which explains +a very similar design when generalising over the type of a rewrite rule. -} -------------------------- diff --git a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr index a233fb4f50..0a575c9bb3 100644 --- a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr +++ b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr @@ -1,14 +1,4 @@ -ExplicitForAllRules1.hs:49:11: warning: - Forall'd type variable ‘k’ is not bound in RULE lhs - Orig bndrs: [k, a, b, x] - Orig lhs: id' @a x - optimised lhs: id' @a x - Forall'd type variable ‘b’ is not bound in RULE lhs - Orig bndrs: [k, a, b, x] - Orig lhs: id' @a x - optimised lhs: id' @a x - ExplicitForAllRules1.hs:49:31: warning: [-Wunused-foralls (in -Wextra)] Unused quantified type variable ‘b’ in the rule "example7" diff --git a/testsuite/tests/typecheck/should_compile/T17710.hs b/testsuite/tests/typecheck/should_compile/T17710.hs new file mode 100644 index 0000000000..f30370c201 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T17710.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module T17710 where + +import Data.Proxy + +foo :: forall k (a :: k) (b :: k). Proxy a -> Proxy b +foo x = Proxy +{-# INLINABLE [1] foo #-} +{-# RULES "foo" forall (x :: Proxy (a :: k)). foo x = Proxy #-} + +bar :: forall k (b :: k). (forall (a :: k). Proxy a -> Proxy a) -> Proxy b +bar g = g Proxy +{-# INLINABLE [1] bar #-} +{-# RULES "bar" forall (g :: forall (a :: k). Proxy a -> Proxy a). bar g = g Proxy #-} diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index c1cd076a6d..5ca578a7ba 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -697,4 +697,5 @@ test('T17566', [extra_files(['T17566a.hs'])], makefile_test, []) test('T12760', unless(compiler_debugged(), skip), compile, ['-O']) test('T13142', normal, compile, ['-O2']) test('T12926', reqlib('vector'), compile, ['-O2']) +test('T17710', normal, compile, ['']) test('T17792', normal, compile, ['']) |