Deal with phantom type variables in rules
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 29 Jul 2015 15:06:29 +0000 (16:06 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 30 Jul 2015 10:03:06 +0000 (11:03 +0100)
See Note [Unbound template type variables] in Rules.hs
This fixes Trac #10689.

The problem was a rule LHS that mentioned a type variable
in a phantom argument to a type synonym.  Then matching the
LHS didn't bind the type variable, and the rule matcher
complained.

This patch fixes the problem, as described by the Note.

I also went back to not-cloning the template varaibles during
rule matching.  I'm convinced that it's not necessary now
(if it ever was), and cloning makes the fix for #10689 much more
fiddly.

compiler/specialise/Rules.hs
testsuite/tests/simplCore/should_compile/T10689.hs [new file with mode: 0644]
testsuite/tests/simplCore/should_compile/T10689a.hs [new file with mode: 0644]
testsuite/tests/simplCore/should_compile/all.T

index 65c3058..dd48832 100644 (file)
@@ -37,19 +37,21 @@ import CoreFVs          ( exprFreeVars, exprsFreeVars, bindFreeVars
 import CoreUtils        ( exprType, eqExpr, mkTick, mkTicks,
                           stripTicksTopT, stripTicksTopE )
 import PprCore          ( pprRules )
-import Type             ( Type )
+import Type             ( Type, substTy, mkTvSubst )
 import TcType           ( tcSplitTyConApp_maybe )
+import TysPrim          ( anyTypeOfKind )
 import Coercion
 import CoreTidy         ( tidyRules )
 import Id
 import IdInfo           ( SpecInfo( SpecInfo ) )
+import Var
 import VarEnv
 import VarSet
 import Name             ( Name, NamedThing(..), nameIsLocalOrFrom )
 import NameSet
 import NameEnv
 import Unify            ( ruleMatchTyX, MatchEnv(..) )
-import BasicTypes       ( Activation, CompilerPhase, isActive )
+import BasicTypes       ( Activation, CompilerPhase, isActive, pprRuleName )
 import StaticFlags      ( opt_PprStyle_Debug )
 import DynFlags         ( DynFlags )
 import Outputable
@@ -442,8 +444,8 @@ isMoreSpecific :: CoreRule -> CoreRule -> Bool
 isMoreSpecific (BuiltinRule {}) _                = False
 isMoreSpecific (Rule {})        (BuiltinRule {}) = True
 isMoreSpecific (Rule { ru_bndrs = bndrs1, ru_args = args1 })
-               (Rule { ru_bndrs = bndrs2, ru_args = args2 })
-  = isJust (matchN (in_scope, id_unfolding_fun) bndrs2 args2 args1)
+               (Rule { ru_bndrs = bndrs2, ru_args = args2, ru_name = rule_name2 })
+  = isJust (matchN (in_scope, id_unfolding_fun) rule_name2 bndrs2 args2 args1)
   where
    id_unfolding_fun _ = NoUnfolding     -- Don't expand in templates
    in_scope = mkInScopeSet (mkVarSet bndrs1)
@@ -507,13 +509,12 @@ matchRule dflags rule_env _is_active fn args _rough_args
         -- We could do this when putting things into the rulebase, I guess
 
 matchRule _ in_scope is_active _ args rough_args
-          (Rule { ru_act = act, ru_rough = tpl_tops
-                , ru_bndrs = tpl_vars, ru_args = tpl_args
-                , ru_rhs = rhs })
+          (Rule { ru_name = rule_name, ru_act = act, ru_rough = tpl_tops
+                , ru_bndrs = tpl_vars, ru_args = tpl_args, ru_rhs = rhs })
   | not (is_active act)               = Nothing
   | ruleCantMatch tpl_tops rough_args = Nothing
   | otherwise
-  = case matchN in_scope tpl_vars tpl_args args of
+  = case matchN in_scope rule_name tpl_vars tpl_args args of
         Nothing                        -> Nothing
         Just (bind_wrapper, tpl_vals) -> Just (bind_wrapper $
                                                rule_fn `mkApps` tpl_vals)
@@ -523,8 +524,7 @@ matchRule _ in_scope is_active _ args rough_args
 
 ---------------------------------------
 matchN  :: InScopeEnv
-        -> [Var]                -- ^ Match template type variables
-        -> [CoreExpr]           -- ^ Match template
+        -> RuleName -> [Var] -> [CoreExpr]
         -> [CoreExpr]           -- ^ Target; can have more elements than the template
         -> Maybe (BindWrapper,  -- Floated bindings; see Note [Matching lets]
                   [CoreExpr])
@@ -532,15 +532,15 @@ matchN  :: InScopeEnv
 -- the entire result and what should be substituted for each template variable.
 -- Fail if there are two few actual arguments from the target to match the template
 
-matchN (in_scope, id_unf) tmpl_vars tmpl_es target_es
+matchN (in_scope, id_unf) rule_name tmpl_vars tmpl_es target_es
   = do  { subst <- go init_menv emptyRuleSubst tmpl_es target_es
-        ; return (rs_binds subst,
-                  map (lookup_tmpl subst) tmpl_vars') }
+        ; let (_, matched_es) = mapAccumL lookup_tmpl subst tmpl_vars
+        ; return (rs_binds subst, matched_es) }
   where
-    (init_rn_env, tmpl_vars') = mapAccumL rnBndrL (mkRnEnv2 in_scope) tmpl_vars
-        -- See Note [Template binders]
+    init_rn_env = mkRnEnv2 (extendInScopeSetList in_scope tmpl_vars)
+                  -- See Note [Template binders]
 
-    init_menv = RV { rv_tmpls = mkVarSet tmpl_vars', rv_lcl = init_rn_env
+    init_menv = RV { rv_tmpls = mkVarSet tmpl_vars, rv_lcl = init_rn_env
                    , rv_fltR = mkEmptySubst (rnInScopeSet init_rn_env)
                    , rv_unf = id_unf }
 
@@ -549,46 +549,82 @@ matchN (in_scope, id_unf) tmpl_vars tmpl_es target_es
     go menv subst (t:ts) (e:es) = do { subst1 <- match menv subst t e
                                      ; go menv subst1 ts es }
 
-    lookup_tmpl :: RuleSubst -> Var -> CoreExpr
-    lookup_tmpl (RS { rs_tv_subst = tv_subst, rs_id_subst = id_subst }) tmpl_var'
-        | isId tmpl_var' = case lookupVarEnv id_subst tmpl_var' of
-                             Just e -> e
-                             _      -> unbound tmpl_var'
-        | otherwise      = case lookupVarEnv tv_subst tmpl_var' of
-                             Just ty -> Type ty
-                             Nothing -> unbound tmpl_var'
+    lookup_tmpl :: RuleSubst -> Var -> (RuleSubst, CoreExpr)
+    lookup_tmpl rs@(RS { rs_tv_subst = tv_subst, rs_id_subst = id_subst }) tmpl_var
+        | isId tmpl_var
+        = case lookupVarEnv id_subst tmpl_var of
+             Just e -> (rs, e)
+             _      -> unbound tmpl_var
+        | otherwise
+        = case lookupVarEnv tv_subst tmpl_var of
+             Just ty -> (rs, Type ty)
+             Nothing -> (rs { rs_tv_subst = extendVarEnv tv_subst tmpl_var fake_ty }, Type fake_ty)
+             -- See Note [Unbound template type variables]
+        where
+          fake_ty = anyTypeOfKind kind
+          kind = Type.substTy (mkTvSubst in_scope tv_subst) (tyVarKind tmpl_var)
 
-    unbound var = pprPanic "Template variable unbound in rewrite rule"
-                        (ppr var $$ ppr tmpl_vars $$ ppr tmpl_vars' $$ ppr tmpl_es $$ ppr target_es)
+    unbound var = pprPanic "Template variable unbound in rewrite rule" $
+                  vcat [ ptext (sLit "Variable:") <+> ppr var
+                       , ptext (sLit "Rule") <+> pprRuleName rule_name
+                       , ptext (sLit "Rule bndrs:") <+> ppr tmpl_vars
+                       , ptext (sLit "LHS args:") <+> ppr tmpl_es
+                       , ptext (sLit "Actual args:") <+> ppr target_es ]
+
+{- Note [Unbound template type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type synonyms with phantom args can give rise to unbound template type
+variables.  Consider this (Trac #10689, simplCore/should_compile/T10689):
+
+    type Foo a b = b
+
+    f :: Eq a => a -> Bool
+    f x = x==x
+
+    {-# RULES "foo" forall (x :: Foo a Char). f x = True #-}
+    finkle = f 'c'
+
+The rule looks like
+   foall (a::*) (d::Eq Char) (x :: Foo a Char).
+         f (Foo a Char) d x = True
+
+Matching the rule won't bind 'a', and legitimately so.  We fudge by
+pretending that 'a' is bound to (Any :: *).
 
-{-
 Note [Template binders]
 ~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following match:
+Consider the following match (example 1):
         Template:  forall x.  f x
-        Target:     f (x+1)
-This should succeed, because the template variable 'x' has
-nothing to do with the 'x' in the target.
+        Target:               f (x+1)
+This should succeed, because the template variable 'x' has nothing to
+do with the 'x' in the target.
 
-On reflection, this case probably does just work, but this might not
+Likewise this one (example 2):
         Template:  forall x. f (\x.x)
-        Target:    f (\y.y)
-Here we want to clone when we find the \x, but to know that x must be in scope
+        Target:              f (\y.y)
 
-To achive this, we use rnBndrL to rename the template variables if
-necessary; the renamed ones are the tmpl_vars'
+We achieve this simply by:
+  * Adding forall'd template binders to the in-scope set
+
+This works even if the template binder are already in scope
+(in the target) because
+
+  * The RuleSubst rs_tv_subst, rs_id_subst maps LHS template vars to
+    the target world.  It is not applied recursively.
+
+  * Having the template vars in the in-scope set ensures that in
+    example 2 above, the (\x.x) is cloned to (\x'. x').
+
+In the past we used rnBndrL to clone the template variables if
+they were already in scope.  But (a) that's not necessary and (b)
+it complicate the fancy footwork for Note [Unbound template type variables]
 
 
 ************************************************************************
 *                                                                      *
                    The main matcher
 *                                                                      *
-************************************************************************
-
-        ---------------------------------------------
-                The inner workings of matching
-        ---------------------------------------------
--}
+********************************************************************* -}
 
 -- * The domain of the TvSubstEnv and IdSubstEnv are the template
 --   variables passed into the match.
diff --git a/testsuite/tests/simplCore/should_compile/T10689.hs b/testsuite/tests/simplCore/should_compile/T10689.hs
new file mode 100644 (file)
index 0000000..d0ee706
--- /dev/null
@@ -0,0 +1,11 @@
+module T10694 where
+
+f :: Eq a => a -> Bool
+{-# NOINLINE f #-}
+f x = x==x
+
+type Foo a b = b
+
+{-# RULES "foo" forall (x :: Foo a Char). f x = True #-}
+
+finkle = f 'c'
diff --git a/testsuite/tests/simplCore/should_compile/T10689a.hs b/testsuite/tests/simplCore/should_compile/T10689a.hs
new file mode 100644 (file)
index 0000000..5b21b42
--- /dev/null
@@ -0,0 +1,114 @@
+{-# LANGUAGE TypeOperators
+           , DataKinds
+           , PolyKinds
+           , TypeFamilies
+           , GADTs
+           , UndecidableInstances
+           , RankNTypes
+           , ScopedTypeVariables
+  #-}
+
+{-# OPTIONS_GHC -Wall #-}
+{-# OPTIONS_GHC -Werror #-}
+{-# OPTIONS_GHC -O1 -fspec-constr #-}
+
+{-
+ghc-stage2: panic! (the 'impossible' happened)
+  (GHC version 7.11.20150723 for x86_64-unknown-linux):
+        Template variable unbound in rewrite rule
+-}
+
+module List (sFoldr1) where
+
+data Proxy t
+
+data family Sing (a :: k)
+
+data TyFun (a :: *) (b :: *)
+
+type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
+
+data instance Sing (f :: TyFun k1 k2 -> *) =
+  SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
+
+type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
+
+type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
+singFun2 :: Proxy f -> SingFunction2 f -> Sing f
+singFun2 _ f = SLambda (\x -> SLambda (f x))
+
+data (:$$) (j :: a) (i :: TyFun [a] [a])
+type instance Apply ((:$$) j) i = (:) j i
+
+data (:$) (l :: TyFun a (TyFun [a] [a] -> *))
+type instance Apply (:$) l = (:$$) l
+data instance Sing (z :: [a])
+  = z ~ '[] =>
+    SNil
+  | forall (m :: a)
+           (n :: [a]). z ~ (:) m n =>
+    SCons (Sing m) (Sing n)
+
+data ErrorSym0 (t1 :: TyFun k1 k2)
+
+type Let1627448493XsSym4 t_afee t_afef t_afeg t_afeh = Let1627448493Xs t_afee t_afef t_afeg t_afeh
+
+type Let1627448493Xs f_afe9
+                     x_afea
+                     wild_1627448474_afeb
+                     wild_1627448476_afec =
+    Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec
+type Foldr1Sym2 (t_afdY :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
+                           -> *)
+                (t_afdZ :: [a_afdP]) =
+    Foldr1 t_afdY t_afdZ
+data Foldr1Sym1 (l_afe3 :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
+                           -> *)
+                (l_afe2 :: TyFun [a_afdP] a_afdP)
+type instance Apply (Foldr1Sym1 l_afe3) l_afe2 = Foldr1Sym2 l_afe3 l_afe2
+
+data Foldr1Sym0 (l_afe0 :: TyFun (TyFun a_afdP (TyFun a_afdP a_afdP
+                                                -> *)
+                                  -> *) (TyFun [a_afdP] a_afdP -> *))
+type instance Apply Foldr1Sym0 l = Foldr1Sym1 l
+
+type family Foldr1 (a_afe5 :: TyFun a_afdP (TyFun a_afdP a_afdP
+                                            -> *)
+                              -> *)
+                   (a_afe6 :: [a_afdP]) :: a_afdP where
+  Foldr1 z_afe7 '[x_afe8] = x_afe8
+  Foldr1 f_afe9 ((:) x_afea ((:) wild_1627448474_afeb wild_1627448476_afec)) = Apply (Apply f_afe9 x_afea) (Apply (Apply Foldr1Sym0 f_afe9) (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec))
+  Foldr1 z_afew '[] = Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list"
+
+sFoldr1 ::
+  forall (x :: TyFun a_afdP (TyFun a_afdP a_afdP -> *) -> *)
+         (y :: [a_afdP]).
+  Sing x
+  -> Sing y -> Sing (Apply (Apply Foldr1Sym0 x) y)
+sFoldr1 _ (SCons _sX SNil) = undefined
+sFoldr1 sF (SCons sX (SCons sWild_1627448474 sWild_1627448476))
+  = let
+      lambda_afeC ::
+        forall f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec.
+        Sing f_afe9
+        -> Sing x_afea
+           -> Sing wild_1627448474_afeb
+              -> Sing wild_1627448476_afec
+                 -> Sing (Apply (Apply Foldr1Sym0 f_afe9) (Apply (Apply (:$) x_afea) (Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec)))
+      lambda_afeC f_afeD x_afeE wild_1627448474_afeF wild_1627448476_afeG
+        = let
+            sXs ::
+              Sing (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec)
+            sXs
+              = applySing
+                  (applySing
+                     (singFun2 (undefined :: Proxy (:$)) SCons) wild_1627448474_afeF)
+                  wild_1627448476_afeG
+          in
+            applySing
+              (applySing f_afeD x_afeE)
+              (applySing
+                 (applySing (singFun2 (undefined :: Proxy Foldr1Sym0) sFoldr1) f_afeD)
+                 sXs)
+    in lambda_afeC sF sX sWild_1627448474 sWild_1627448476
+sFoldr1 _ SNil = undefined
index b675077..b337c9c 100644 (file)
@@ -223,3 +223,5 @@ test('T10083',
      expect_broken(10083),
      run_command,
      ['$MAKE -s --no-print-directory T10083'])
+test('T10689', normal, compile, [''])
+test('T10689a', normal, compile, [''])