Commit 8674883c authored by Simon Peyton Jones's avatar Simon Peyton Jones

Allow unbound Refl binders in a RULE

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.
parent e07211f7
......@@ -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)
......
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -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
......
......@@ -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.
......
......@@ -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
......
{-# 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
......@@ -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'])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment