X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcRules.lhs;h=3925c6def3e535048aa4b0972a7c3d94a546c7b4;hp=28be06e05fd8beaced14bdb74d129e7df93cd0b7;hb=HEAD;hpb=2423c249f5ca7785d0ec89eb33e72662da7561c1

diff --git a/compiler/typecheck/TcRules.lhs b/compiler/typecheck/TcRules.lhs
index 28be06e..3925c6d 100644
--- a/compiler/typecheck/TcRules.lhs
+++ b/compiler/typecheck/TcRules.lhs
@@ -8,8 +8,6 @@ TcRules: Typechecking transformation rules
 \begin{code}
 module TcRules ( tcRules ) where
 
-#include "HsVersions.h"
-
 import HsSyn
 import TcRnMonad
 import TcSimplify
@@ -18,51 +16,65 @@ import TcType
 import TcHsType
 import TcExpr
 import TcEnv
-import Inst
 import Id
 import Name
+import VarSet
 import SrcLoc
 import Outputable
+import FastString
+import Data.List( partition )
 \end{code}
 
+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.
+
 \begin{code}
 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
-tcRules decls = mappM (wrapLocM tcRule) decls
+tcRules decls = mapM (wrapLocM tcRule) decls
 
 tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
-tcRule (HsRule name act vars lhs fv_lhs rhs fv_rhs)
-  = addErrCtxt (ruleCtxt name)			$
-    traceTc (ptext SLIT("---- Rule ------")
-		 <+> ppr name)			`thenM_` 
-    newFlexiTyVarTy openTypeKind		`thenM` \ rule_ty ->
-
-	-- Deal with the tyvars mentioned in signatures
-    tcRuleBndrs vars (\ ids ->
-		-- Now LHS and RHS
-	getLIE (tcMonoExpr lhs rule_ty)	`thenM` \ (lhs', lhs_lie) ->
-	getLIE (tcMonoExpr rhs rule_ty)	`thenM` \ (rhs', rhs_lie) ->
-	returnM (ids, lhs', rhs', lhs_lie, rhs_lie)
-    )				`thenM` \ (ids, lhs', rhs', lhs_lie, rhs_lie) ->
-
-		-- Check that LHS has no overloading at all
-    tcSimplifyRuleLhs lhs_lie	`thenM` \ (lhs_dicts, lhs_binds) ->
-
-	-- Gather the template variables and tyvars
-    let
-	tpl_ids = map instToId lhs_dicts ++ ids
+tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
+  = addErrCtxt (ruleCtxt name)	$
+    do { traceTc "---- Rule ------" (ppr name)
+
+    	-- Note [Typechecking rules]
+       ; vars <- tcRuleBndrs hs_bndrs
+       ; let (id_bndrs, tv_bndrs) = partition isId vars
+       ; (lhs', lhs_lie, rhs', rhs_lie, rule_ty)
+            <- tcExtendTyVarEnv tv_bndrs $
+               tcExtendIdEnv id_bndrs $
+               do { ((lhs', rule_ty), lhs_lie) <- captureConstraints (tcInferRho lhs)
+                  ; (rhs', rhs_lie) <- captureConstraints (tcMonoExpr rhs rule_ty)
+                  ; return (lhs', lhs_lie, rhs', rhs_lie, rule_ty) }
+
+       ; (lhs_dicts, lhs_ev_binds, rhs_ev_binds) 
+             <- simplifyRule name tv_bndrs lhs_lie rhs_lie
 
 	-- IMPORTANT!  We *quantify* over any dicts that appear in the LHS
 	-- Reason: 
-	--	a) The particular dictionary isn't important, because its value
+	--	(a) The particular dictionary isn't important, because its value
 	--	   depends only on the type
 	--		e.g	gcd Int $fIntegralInt
 	--         Here we'd like to match against (gcd Int any_d) for any 'any_d'
 	--
-	--	b) We'd like to make available the dictionaries bound 
-	--	   on the LHS in the RHS, so quantifying over them is good
-	--	   See the 'lhs_dicts' in tcSimplifyAndCheck for the RHS
+	--	(b) We'd like to make available the dictionaries bound 
+	--	    on the LHS in the RHS, so quantifying over them is good
+	--	    See the 'lhs_dicts' in tcSimplifyAndCheck for the RHS
 
-	-- We initially quantify over any tyvars free in *either* the rule
+	-- 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
@@ -70,47 +82,46 @@ tcRule (HsRule name act vars lhs fv_lhs rhs fv_rhs)
 	--
 	-- We also need to get the free tyvars of the LHS; but we do that
 	-- during zonking (see TcHsSyn.zonkRule)
-	--
-	forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
-    in
-	-- RHS can be a bit more lenient.  In particular,
-	-- we let constant dictionaries etc float outwards
-	--
-	-- NB: tcSimplifyInferCheck zonks the forall_tvs, and 
-	--     knocks out any that are constrained by the environment
-    getInstLoc (SigOrigin (RuleSkol name))	`thenM` \ loc -> 
-    tcSimplifyInferCheck loc
-			 forall_tvs
-			 lhs_dicts rhs_lie	`thenM` \ (forall_tvs1, rhs_binds) ->
-    zonkQuantifiedTyVars forall_tvs1 		`thenM` \ forall_tvs2 ->
-	-- This zonk is exactly the same as the one in TcBinds.generalise
-
-    returnM (HsRule name act
-		    (map (RuleBndr . noLoc) (forall_tvs2 ++ tpl_ids))	-- yuk
-		    (mkHsDictLet lhs_binds lhs') fv_lhs
-		    (mkHsDictLet rhs_binds rhs') fv_rhs)
-
-
-tcRuleBndrs [] thing_inside = thing_inside []
-tcRuleBndrs (RuleBndr var : vars) thing_inside
+
+       ; let tpl_ids    = lhs_dicts ++ id_bndrs
+             forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
+
+	     -- Now figure out what to quantify over
+	     -- c.f. TcSimplify.simplifyInfer
+       ; zonked_forall_tvs <- zonkTcTyVarsAndFV forall_tvs
+       ; gbl_tvs           <- tcGetGlobalTyVars	     -- Already zonked
+       ; qtvs <- zonkQuantifiedTyVars $
+                 varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs)
+
+       ; return (HsRule name act
+		    (map (RuleBndr . noLoc) (qtvs ++ tpl_ids))	-- yuk
+		    (mkHsDictLet lhs_ev_binds lhs') fv_lhs
+		    (mkHsDictLet rhs_ev_binds rhs') fv_rhs) }
+
+tcRuleBndrs :: [RuleBndr Name] -> TcM [Var]
+tcRuleBndrs [] 
+  = return []
+tcRuleBndrs (RuleBndr var : rule_bndrs)
   = do 	{ ty <- newFlexiTyVarTy openTypeKind
-	; let id = mkLocalId (unLoc var) ty
-	; tcExtendIdEnv [id] $
-	  tcRuleBndrs vars (\ids -> thing_inside (id:ids)) }
-tcRuleBndrs (RuleBndrSig var rn_ty : vars) thing_inside
+        ; vars <- tcRuleBndrs rule_bndrs
+	; return (mkLocalId (unLoc var) ty : vars) }
+tcRuleBndrs (RuleBndrSig var 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
   = do	{ let ctxt = FunSigCtxt (unLoc var)
 	; (tyvars, ty) <- tcHsPatSigType ctxt rn_ty
-	; let skol_tvs = tcSkolSigTyVars (SigSkol ctxt) tyvars
+        ; let skol_tvs = tcSuperSkolTyVars tyvars
 	      id_ty = substTyWith tyvars (mkTyVarTys skol_tvs) ty
 	      id = mkLocalId (unLoc var) id_ty
-	; tcExtendTyVarEnv skol_tvs $
-	  tcExtendIdEnv [id] $
-	  tcRuleBndrs vars (\ids -> thing_inside (id:ids)) }
 
-ruleCtxt name = ptext SLIT("When checking the transformation rule") <+> 
+	      -- The type variables scope over subsequent bindings; yuk
+        ; vars <- tcExtendTyVarEnv skol_tvs $ 
+                  tcRuleBndrs rule_bndrs 
+	; return (skol_tvs ++ id : vars) }
+
+ruleCtxt :: FastString -> SDoc
+ruleCtxt name = ptext (sLit "When checking the transformation rule") <+> 
 		doubleQuotes (ftext name)
 \end{code}