From: simonpj@microsoft.com <unknown>
Date: Sat, 29 Sep 2007 10:44:06 +0000 (+0000)
Subject: Fix Trac #1746: make rule-matching work properly with Cast expressions
X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=27ebdb91ed6df61dbf680a87ccda40337bc811af

Fix Trac #1746: make rule-matching work properly with Cast expressions

The Cast case of the rule-matcher was simply wrong.

This patch fixes it; see Trac #1746.

I also fixed the rule generation in SpecConstr to generate a wild-card
for the cast expression, which we don't want to match on.  This makes
the rule more widely applicable; it wasn't the cause of the bug.
---

diff --git a/compiler/specialise/Rules.lhs b/compiler/specialise/Rules.lhs
index c1d2006..24c4004 100644
--- a/compiler/specialise/Rules.lhs
+++ b/compiler/specialise/Rules.lhs
@@ -595,11 +595,8 @@ match menv subst (Type ty1) (Type ty2)
   = match_ty menv subst ty1 ty2
 
 match menv subst (Cast e1 co1) (Cast e2 co2)
-  | (from1, to1) <- coercionKind co1
-  , (from2, to2) <- coercionKind co2
-  = do	{ subst1 <- match_ty menv subst  to1   to2
-	; subst2 <- match_ty menv subst1 from1 from2
-	; match menv subst2 e1 e2 }
+  = do	{ subst1 <- match_ty menv subst co1 co2
+	; match menv subst1 e1 e2 }
 
 {-	REMOVING OLD CODE: I think that the above handling for let is 
 			   better than the stuff here, which looks 
@@ -646,6 +643,8 @@ match_var menv subst@(tv_subst, id_subst, binds) v1 e2
 
 		| otherwise	-- No renaming to do on e2, because no free var
 				-- of e2 is in the rnEnvR of the envt
+		-- Note [Matching variable types]
+		-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 		-- However, we must match the *types*; e.g.
 		--   forall (c::Char->Int) (x::Char). 
 		--	f (c x) = "RULE FIRED"
diff --git a/compiler/specialise/SpecConstr.lhs b/compiler/specialise/SpecConstr.lhs
index 256674b..0478d2e 100644
--- a/compiler/specialise/SpecConstr.lhs
+++ b/compiler/specialise/SpecConstr.lhs
@@ -27,11 +27,11 @@ import CoreTidy		( tidyRules )
 import PprCore		( pprRules )
 import WwLib		( mkWorkerArgs )
 import DataCon		( dataConRepArity, dataConUnivTyVars )
-import Type		( Type, tyConAppArgs )
-import Coercion		( coercionKind )
+import Coercion	
+import Type		hiding( substTy )
 import Id		( Id, idName, idType, isDataConWorkId_maybe, idArity,
 			  mkUserLocal, mkSysLocal, idUnfolding, isLocalId )
-import Var		( Var )
+import Var
 import VarEnv
 import VarSet
 import Name
@@ -1107,10 +1107,15 @@ argToPat in_scope val_env (Let _ arg) arg_occ
 
 argToPat in_scope val_env (Cast arg co) arg_occ
   = do	{ (interesting, arg') <- argToPat in_scope val_env arg arg_occ
-	; if interesting then 
-		return (interesting, Cast arg' co)
-	  else 
-		wildCardPat (snd (coercionKind co)) }
+	; let (ty1,ty2) = coercionKind co
+	; if not interesting then 
+		wildCardPat ty2
+	  else do
+	{ -- Make a wild-card pattern for the coercion
+	  uniq <- getUniqueUs
+	; let co_name = mkSysTvName uniq FSLIT("sg")
+	      co_var = mkCoVar co_name (mkCoKind ty1 ty2)
+	; return (interesting, Cast arg' (mkTyVarTy co_var)) } }
 
 {-	Disabling lambda specialisation for now
 	It's fragile, and the spec_loop can be infinite
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index edec800..8ffee89 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -26,6 +26,7 @@ import Var
 import VarEnv
 import VarSet
 import Type
+import Coercion
 import TyCon
 import DataCon
 import TypeRep
@@ -149,7 +150,7 @@ match :: MatchEnv	-- For the most part this is pushed downwards
 -- it respects NewTypes and PredType
 
 match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2
-			  | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
+			 | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
 
 match menv subst (TyVarTy tv1) ty2
   | tv1' `elemVarSet` me_tmpls menv
@@ -157,10 +158,9 @@ match menv subst (TyVarTy tv1) ty2
 	Nothing 	-- No existing binding
 	    | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
 	    -> Nothing	-- Occurs check
-	    | not (typeKind ty2 `isSubKind` tyVarKind tv1)
-	    -> Nothing	-- Kind mis-match
-	    | otherwise
-	    -> Just (extendVarEnv subst tv1' ty2)
+	    | otherwise	
+	    -> do { subst1 <- match_kind menv subst tv1 ty2
+		  ; return (extendVarEnv subst tv1' ty2) }
 
 	Just ty1' 	-- There is an existing binding; check whether ty2 matches it
 	    | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
@@ -200,6 +200,33 @@ match menv subst ty1 ty2
   = Nothing
 
 --------------
+match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
+-- Match the kind of the template tyvar with the kind of Type
+-- Note [Matching kinds]
+match_kind menv subst tv ty
+  | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
+			  (ty3,ty4) = coercionKind ty
+		    ; subst1 <- match menv subst ty1 ty3
+		    ; match menv subst1 ty2 ty4 }
+  | otherwise  = if typeKind ty `isSubKind` tyVarKind tv
+		 then Just subst
+		 else Nothing
+
+-- Note [Matching kinds]
+-- ~~~~~~~~~~~~~~~~~~~~~
+-- For ordinary type variables, we don't want (m a) to match (n b) 
+-- if say (a::*) and (b::*->*).  This is just a yes/no issue. 
+--
+-- For coercion kinds matters are more complicated.  If we have a 
+-- coercion template variable co::a~[b], where a,b are presumably also
+-- template type variables, then we must match co's kind against the 
+-- kind of the actual argument, so as to give bindings to a,b.  
+--
+-- In fact I have no example in mind that *requires* this kind-matching
+-- to instantiate template type variables, but it seems like the right
+-- thing to do.  C.f. Note [Matching variable types] in Rules.lhs
+
+--------------
 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
 
 --------------