Allow unbound Refl binders in a RULE
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 29 Mar 2017 08:00:02 +0000 (09:00 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 29 Mar 2017 08:02:53 +0000 (09:02 +0100)
Trac #13410 was failing because we had a RULE with a binder
   (c :: t~t)
and the /occurrences/ of c on the LHS were being optimised to Refl,
leaving a binder that would not be filled in by matching the LHS
of the rule.

I flirted with trying to ensure that occurrences (c :: t~t) are
not optimised to Relf, but that turned out to be fragile; it was
being done, for good reasons, in multiple places, including
  - TyCoRep.substCoVarBndr
  - Simplify.simplCast
  - Corecion.mkCoVarCo

So I fixed it in one place by making Rules.matchN deal happily
with an unbound binder (c :: t~t).  Quite easy.  See "Coercion
variables" in Note [Unbound RULE binders] in Rules.

In addition, I needed to make CoreLint be happy with an bound
RULE binder that is a Relf coercion variable

In debugging this, I was perplexed that occurrences of a variable
(c :: t~t) mysteriously turned into Refl.  I found out how it
was happening, and decided to move it:

* In TyCoRep.substCoVarBndr, do not substitute Refl for a
  binder (c :: t~t).

* In mkCoVarCo do not optimise (c :: t~t) to Refl.

Instead, we do this optimisation in optCoercion (specifically
opt_co4) where, surprisingly, the optimisation was /not/
being done.  This has no effect on what programs compile;
it just moves a relatively-expensive optimisation to optCoercion,
where it seems more properly to belong.  It's actually not clear
to me which is really "better", but this way round is less
surprising.

One small simplifying refactoring

* Eliminate TyCoRep.substCoVarBndrCallback, which was only
  called locally.

compiler/coreSyn/CoreLint.hs
compiler/specialise/Rules.hs
compiler/types/Coercion.hs
compiler/types/OptCoercion.hs
compiler/types/TyCoRep.hs
testsuite/tests/simplCore/should_compile/T13410.hs [new file with mode: 0644]
testsuite/tests/simplCore/should_compile/all.T

index 089a225..4c3da43 100644 (file)
@@ -1425,16 +1425,14 @@ lintCoreRule fun fun_ty rule@(Rule { ru_name = name, ru_bndrs = bndrs
        ; rhs_ty <- case isJoinId_maybe fun of
                      Just join_arity
                        -> do { checkL (args `lengthIs` join_arity) $
-                                 mkBadJoinPointRuleMsg fun join_arity rule
+                                mkBadJoinPointRuleMsg fun join_arity rule
                                -- See Note [Rules for join points]
                              ; lintCoreExpr rhs }
                      _ -> markAllJoinsBad $ lintCoreExpr rhs
        ; ensureEqTys lhs_ty rhs_ty $
          (rule_doc <+> vcat [ text "lhs type:" <+> ppr lhs_ty
                             , text "rhs type:" <+> ppr rhs_ty ])
-       ; let bad_bndrs = filterOut (`elemVarSet` exprsFreeVars args) $
-                         filter (`elemVarSet` exprFreeVars rhs) $
-                         bndrs
+       ; let bad_bndrs = filter is_bad_bndr bndrs
 
        ; checkL (null bad_bndrs)
                 (rule_doc <+> text "unbound" <+> ppr bad_bndrs)
@@ -1443,6 +1441,16 @@ lintCoreRule fun fun_ty rule@(Rule { ru_name = name, ru_bndrs = bndrs
   where
     rule_doc = text "Rule" <+> doubleQuotes (ftext name) <> colon
 
+    lhs_fvs = exprsFreeVars args
+    rhs_fvs = exprFreeVars rhs
+
+    is_bad_bndr :: Var -> Bool
+    -- See Note [Unbound RULE binders] in Rules
+    is_bad_bndr bndr = not (bndr `elemVarSet` lhs_fvs)
+                    && bndr `elemVarSet` rhs_fvs
+                    && isNothing (isReflCoVar_maybe bndr)
+
+
 {- Note [Linting rules]
 ~~~~~~~~~~~~~~~~~~~~~~~
 It's very bad if simplifying a rule means that one of the template
@@ -1462,7 +1470,7 @@ this check will nail it.
 NB (Trac #11643): it's possible that a variable listed in the
 binders becomes not-mentioned on both LHS and RHS.  Here's a silly
 example:
-   RULE forall x y. f (g x y) = g (x+1 (y-1)
+   RULE forall x y. f (g x y) = g (x+1) (y-1)
 And suppose worker/wrapper decides that 'x' is Absent.  Then
 we'll end up with
    RULE forall x y. f ($gw y) = $gw (x+1)
index 192b6bb..1dcff82 100644 (file)
@@ -555,12 +555,16 @@ matchN (in_scope, id_unf) rule_name tmpl_vars tmpl_es target_es
         | isId tmpl_var
         = case lookupVarEnv id_subst tmpl_var of
              Just e -> (rs, e)
-             _      -> unbound tmpl_var
+             Nothing | Just refl_co <- isReflCoVar_maybe tmpl_var
+                     , let co_expr = Coercion refl_co
+                     -> (rs { rs_id_subst = extendVarEnv id_subst tmpl_var co_expr }, co_expr)
+                     | otherwise
+                     -> 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]
+                        -- See Note [Unbound RULE binders]
         where
           fake_ty = anyTypeOfKind kind
           cv_subst = to_co_env id_subst
@@ -584,10 +588,14 @@ matchN (in_scope, id_unf) rule_name tmpl_vars tmpl_es target_es
                        , text "LHS args:" <+> ppr tmpl_es
                        , text "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):
+{- Note [Unbound RULE binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It can be the case that the binder in a rule is not actually
+bound on the LHS:
+
+* 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
 
@@ -597,12 +605,31 @@ variables.  Consider this (Trac #10689, simplCore/should_compile/T10689):
     {-# 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).
+  The rule looks like
+    forall (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 :: *).
+  Matching the rule won't bind 'a', and legitimately so.  We fudge by
+  pretending that 'a' is bound to (Any :: *).
+
+* Coercion variables.  On the LHS of a RULE for a local binder
+  we might have
+    RULE forall (c :: a~b). f (x |> c) = e
+  Now, if that binding is inlined, so that a=b=Int, we'd get
+    RULE forall (c :: Int~Int). f (x |> c) = e
+  and now when we simpilfy the LHS (Simplify.simplRule) we
+  optCoercion will turn that 'c' into Refl:
+    RULE forall (c :: Int~Int). f (x |> <Int>) = e
+  and then perhaps drop it altogether.  Now 'c' is unbound.
+
+  It's tricky to be sure this never happens, so instead I
+  say it's OK to have an unbound coercion binder in a RULE
+  provided its type is (c :: t~t).  Then, when the RULE
+  fires we can substitute <t> for c.
+
+  This actually happened (in a RULE for a local function)
+  in Trac #13410, and also in test T10602.
+
 
 Note [Template binders]
 ~~~~~~~~~~~~~~~~~~~~~~~
index 6b7a640..86f9d76 100644 (file)
@@ -59,6 +59,7 @@ module Coercion (
         pickLR,
 
         isReflCo, isReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
+        isReflCoVar_maybe,
 
         -- ** Coercion variables
         mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
@@ -372,10 +373,10 @@ splitForAllCo_maybe _                     = Nothing
 -------------------------------------------------------
 -- and some coercion kind stuff
 
-coVarTypes :: CoVar -> (Type,Type)
+coVarTypes :: CoVar -> Pair Type
 coVarTypes cv
   | (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
-  = (ty1, ty2)
+  = Pair ty1 ty2
 
 coVarKindsTypesRole :: CoVar -> (Kind,Kind,Type,Type,Role)
 coVarKindsTypesRole cv
@@ -432,6 +433,15 @@ mkRuntimeRepCo co
     kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2
                            -- (up to silliness with Constraint)
 
+isReflCoVar_maybe :: CoVar -> Maybe Coercion
+-- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
+isReflCoVar_maybe cv
+  | Pair ty1 ty2 <- coVarTypes cv
+  , ty1 `eqType` ty2
+  = Just (Refl (coVarRole cv) ty1)
+  | otherwise
+  = Nothing
+
 -- | Tests if this coercion is obviously reflexive. Guaranteed to work
 -- very quickly. Sometimes a coercion can be reflexive, but not obviously
 -- so. c.f. 'isReflexiveCo'
@@ -739,15 +749,20 @@ mkHomoForAllCos_NoRefl tvs orig_co = foldr go orig_co tvs
 
 mkCoVarCo :: CoVar -> Coercion
 -- cv :: s ~# t
-mkCoVarCo cv
-  | ty1 `eqType` ty2 = Refl (coVarRole cv) ty1
-  | otherwise        = CoVarCo cv
-  where
-    (ty1, ty2) = coVarTypes cv
+-- See Note [mkCoVarCo]
+mkCoVarCo cv = CoVarCo cv
 
 mkCoVarCos :: [CoVar] -> [Coercion]
 mkCoVarCos = map mkCoVarCo
 
+{- Note [mkCoVarCo]
+~~~~~~~~~~~~~~~~~~~
+In the past, mkCoVarCo optimised (c :: t~t) to (Refl t).  That is
+valid (although see Note [Unbound RULE binders] in Rules), but
+it's a relatively expensive test and perhaps better done in
+optCoercion.  Not a big deal either way.
+-}
+
 -- | Extract a covar, if possible. This check is dirty. Be ashamed
 -- of yourself. (It's dirty because it cares about the structure of
 -- a coercion, which is morally reprehensible.)
@@ -1800,7 +1815,7 @@ coercionKind co = go co
             -- need to, see #11735
         mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2'
     go (FunCo _ co1 co2)    = mkFunTy <$> go co1 <*> go co2
-    go (CoVarCo cv)         = toPair $ coVarTypes cv
+    go (CoVarCo cv)         = coVarTypes cv
     go (AxiomInstCo ax ind cos)
       | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
                    , cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
@@ -1882,7 +1897,7 @@ coercionKindRole = go
         (mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2', r)
     go (FunCo r co1 co2)
       = (mkFunTy <$> coercionKind co1 <*> coercionKind co2, r)
-    go (CoVarCo cv) = (toPair $ coVarTypes cv, coVarRole cv)
+    go (CoVarCo cv) = (coVarTypes cv, coVarRole cv)
     go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
     go (UnivCo _ r ty1 ty2)  = (Pair ty1 ty2, r)
     go (SymCo co) = first swap $ go co
index 5e4927f..7f96754 100644 (file)
@@ -220,13 +220,24 @@ opt_co4 env sym rep r (CoVarCo cv)
   | Just co <- lookupCoVar (lcTCvSubst env) cv
   = opt_co4_wrap (zapLiftingContext env) sym rep r co
 
-  | Just cv1 <- lookupInScope (lcInScopeSet env) cv
-  = ASSERT( isCoVar cv1 ) wrapRole rep r $ wrapSym sym (CoVarCo cv1)
-                -- cv1 might have a substituted kind!
+  | ty1 `eqType` ty2   -- See Note [Optimise CoVarCo to Refl]
+  = Refl (chooseRole rep r) ty1
+
+  | otherwise
+  = ASSERT( isCoVar cv1 )
+    wrapRole rep r $ wrapSym sym $
+    CoVarCo cv1
+
+  where
+    Pair ty1 ty2 = coVarTypes cv1
+
+    cv1 = case lookupInScope (lcInScopeSet env) cv of
+             Just cv1 -> cv1
+             Nothing  -> WARN( True, text "opt_co: not in scope:"
+                                     <+> ppr cv $$ ppr env)
+                         cv
+          -- cv1 might have a substituted kind!
 
-  | otherwise = WARN( True, text "opt_co: not in scope:" <+> ppr cv $$ ppr env)
-                ASSERT( isCoVar cv )
-                wrapRole rep r $ wrapSym sym (CoVarCo cv)
 
 opt_co4 env sym rep r (AxiomInstCo con ind cos)
     -- Do *not* push sym inside top-level axioms
@@ -335,6 +346,15 @@ opt_co4 env sym rep r (AxiomRuleCo co cs)
     wrapSym sym $
     AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
 
+{- Note [Optimise CoVarCo to Refl]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have (c :: t~t) we can optimise it to Refl. That increases the
+chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)
+
+We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
+in Coercion.
+-}
+
 -------------
 -- | Optimize a phantom coercion. The input coercion may not necessarily
 -- be a phantom, but the output sure will be.
index 8f9b1a5..52a0f1d 100644 (file)
@@ -112,7 +112,7 @@ module TyCoRep (
         substTyVar, substTyVars,
         substForAllCoBndr,
         substTyVarBndrCallback, substForAllCoBndrCallback,
-        substCoVarBndrCallback,
+        checkValidSubst, isValidTCvSubst,
 
         -- * Tidying type related things up for printing
         tidyType,      tidyTypes,
@@ -2367,21 +2367,13 @@ substTyVarBndrCallback subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
         -- The uniqAway part makes sure the new variable is not already in scope
 
 substCoVarBndr :: TCvSubst -> CoVar -> (TCvSubst, CoVar)
-substCoVarBndr = substCoVarBndrCallback False substTy
-
-substCoVarBndrCallback :: Bool -- apply "sym" to the covar?
-                       -> (TCvSubst -> Type -> Type)
-                       -> TCvSubst -> CoVar -> (TCvSubst, CoVar)
-substCoVarBndrCallback sym subst_fun subst@(TCvSubst in_scope tenv cenv) old_var
+substCoVarBndr subst@(TCvSubst in_scope tenv cenv) old_var
   = ASSERT( isCoVar old_var )
     (TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
   where
-    -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
-    -- In that case, mkCoVarCo will return a ReflCoercion, and
-    -- we want to substitute that (not new_var) for old_var
-    new_co    = (if sym then mkSymCo else id) $ mkCoVarCo new_var
+    new_co         = mkCoVarCo new_var
     no_kind_change = all noFreeVarsOfType [t1, t2]
-    no_change = new_var == old_var && not (isReflCo new_co) && no_kind_change
+    no_change      = new_var == old_var && no_kind_change
 
     new_cenv | no_change = delVarEnv cenv old_var
              | otherwise = extendVarEnv cenv old_var new_co
@@ -2390,9 +2382,9 @@ substCoVarBndrCallback sym subst_fun subst@(TCvSubst in_scope tenv cenv) old_var
     subst_old_var = mkCoVar (varName old_var) new_var_type
 
     (_, _, t1, t2, role) = coVarKindsTypesRole old_var
-    t1' = subst_fun subst t1
-    t2' = subst_fun subst t2
-    new_var_type = uncurry (mkCoercionType role) (if sym then (t2', t1') else (t1', t2'))
+    t1' = substTy subst t1
+    t2' = substTy subst t2
+    new_var_type = mkCoercionType role t1' t2'
                   -- It's important to do the substitution for coercions,
                   -- because they can have free type variables
 
diff --git a/testsuite/tests/simplCore/should_compile/T13410.hs b/testsuite/tests/simplCore/should_compile/T13410.hs
new file mode 100644 (file)
index 0000000..9db017d
--- /dev/null
@@ -0,0 +1,152 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Vector.Hybrid.Internal (Vector) where
+
+import Control.Monad (liftM2)
+import Data.Functor.Identity (Identity(..))
+import GHC.ST (ST, runST)
+import Text.Read (ReadPrec, readPrec)
+
+-----
+
+class Monad m => PrimMonad m where
+  type PrimState m
+
+instance PrimMonad (ST s) where
+  type PrimState (ST s) = s
+
+class GMVector v a where
+  gmbasicLength      :: v s a -> Int
+  gmbasicUnsafeSlice :: Int -> Int -> v s a -> v s a
+  gmbasicUnsafeNew   :: PrimMonad m => Int -> m (v (PrimState m) a)
+  gmbasicUnsafeWrite :: PrimMonad m => v (PrimState m) a -> Int -> a -> m ()
+
+type family GMutable (v :: * -> *) :: * -> * -> *
+
+class GMVector (GMutable v) a => GVector v a where
+  gbasicUnsafeFreeze :: PrimMonad m => GMutable v (PrimState m) a -> m (v a)
+
+data Step s a where
+  Yield :: a -> s -> Step s a
+
+instance Functor (Step s) where
+  {-# INLINE fmap #-}
+  fmap f (Yield x s) = Yield (f x) s
+
+data Stream m a = forall s. Stream (s -> m (Step s a)) s
+data Chunk v a = Chunk Int (forall m. (PrimMonad m, GVector v a) => GMutable v (PrimState m) a -> m ())
+data New v a = New { newrun :: forall s. ST s (GMutable v s a) }
+type MBundle m v a = Stream m (Chunk v a)
+type Bundle v a = MBundle Identity v a
+
+mbfromStream :: Monad m => Stream m a -> MBundle m v a
+{-# INLINE mbfromStream #-}
+mbfromStream (Stream step t) = Stream step' t
+  where
+    step' s = do r <- step s
+                 return $ fmap (\x -> Chunk 1 (\v -> gmbasicUnsafeWrite v 0 x)) r
+
+mbunsafeFromList :: Monad m => [a] -> MBundle m v a
+{-# INLINE [1] mbunsafeFromList #-}
+mbunsafeFromList xs = mbfromStream (sfromList xs)
+
+blift :: Monad m => Bundle v a -> MBundle m v a
+{-# INLINE [1] blift #-}
+blift (Stream vstep t) = Stream (return . runIdentity . vstep) t
+
+sfromList :: Monad m => [a] -> Stream m a
+{-# INLINE sfromList #-}
+sfromList zs = Stream step zs
+  where
+    step (x:xs) = return (Yield x xs)
+    step _ = undefined
+
+sfoldlM :: Monad m => (a -> b -> m a) -> a -> Stream m b -> m a
+{-# INLINE [1] sfoldlM #-}
+sfoldlM m w (Stream step t) = foldlM_loop w t
+  where
+    foldlM_loop z s
+      = do
+          r <- step s
+          case r of
+            Yield x s' -> do { z' <- m z x; foldlM_loop z' s' }
+
+gmvunstream :: (PrimMonad m, GVector v a)
+            => Bundle v a -> m (GMutable v (PrimState m) a)
+{-# INLINE [1] gmvunstream #-}
+gmvunstream s = gmvmunstreamUnknown (blift s)
+
+gmvmunstreamUnknown :: (PrimMonad m, GVector v a)
+                    => MBundle m v a -> m (GMutable v (PrimState m) a)
+{-# INLINE gmvmunstreamUnknown #-}
+gmvmunstreamUnknown s
+  = do
+      v <- gmbasicUnsafeNew 0
+      (_, _) <- sfoldlM copyChunk (v,0) s
+      return undefined
+  where
+    {-# INLINE [0] copyChunk #-}
+    copyChunk (v,i) (Chunk n f)
+      = do
+          let j = i+n
+          v' <- if gmbasicLength v < j
+                  then gmbasicUnsafeNew undefined
+                  else return v
+          f (gmbasicUnsafeSlice i n v')
+          return (v',j)
+
+newunstream :: GVector v a => Bundle v a -> New v a
+{-# INLINE [1] newunstream #-}
+newunstream s = s `seq` New (gmvunstream s)
+
+gnew :: GVector v a => New v a -> v a
+{-# INLINE [1] gnew #-}
+gnew m = m `seq` runST (gbasicUnsafeFreeze =<< newrun m)
+
+gunstream :: GVector v a => Bundle v a -> v a
+{-# INLINE gunstream #-}
+gunstream s = gnew (newunstream s)
+
+gfromList :: GVector v a => [a] -> v a
+{-# INLINE gfromList #-}
+gfromList = gunstream . mbunsafeFromList
+
+greadPrec :: (GVector v a, Read a) => ReadPrec (v a)
+{-# INLINE greadPrec #-}
+greadPrec = do
+  xs <- readPrec
+  return (gfromList xs)
+
+-----
+
+data MVector :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
+  MV :: !(u s a) -> !(v s b) -> MVector u v s (a, b)
+
+instance (GMVector u a, GMVector v b) => GMVector (MVector u v) (a, b) where
+  gmbasicLength (MV ks _) = gmbasicLength ks
+  gmbasicUnsafeSlice s e (MV ks vs) = MV (gmbasicUnsafeSlice s e ks) (gmbasicUnsafeSlice s e vs)
+
+  gmbasicUnsafeNew n = liftM2 MV (gmbasicUnsafeNew n) (gmbasicUnsafeNew n)
+  -- Removing this INLINE pragma makes it compile
+  {-# INLINE gmbasicUnsafeNew #-}
+
+  gmbasicUnsafeWrite (MV ks vs) n (k,v) = do
+    gmbasicUnsafeWrite ks n k
+    gmbasicUnsafeWrite vs n v
+
+data Vector :: (* -> *) -> (* -> *) -> * -> *
+
+type instance GMutable (Vector u v) = MVector (GMutable u) (GMutable v)
+
+instance (GVector u a, GVector v b) => GVector (Vector u v) (a, b) where
+  gbasicUnsafeFreeze = undefined
+
+instance (GVector u a, GVector v b, Read a, Read b, c ~ (a, b)) => Read (Vector u v c) where
+  readPrec = greadPrec
index 365aa44..2d87e24 100644 (file)
@@ -253,3 +253,4 @@ test('T13367', normal, run_command, ['$MAKE -s --no-print-directory T13367'])
 test('T13417', normal, compile, ['-O'])
 test('T13413', normal, compile, [''])
 test('T13429', normal, compile, [''])
+test('T13410', normal, compile, ['-O2'])