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 (file)
--- 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 (file)
--- 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 (file)
--- 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
 
 --------------