"Unbound RULE binders" conditions too restrictive?
While debugging a client project a colleague encountered Core Lint error after simplification:
*** Core Lint errors : in result of Simplifier ***
<no location info>: error: [-Werror]
Rule "SC:$j0": unbound [sg_svBxD]
In the RHS of $w$ctoSQL_svxsI :: ByteArray#
-> Int#
-> Int#
-> TableName
-> SetExp
-> Maybe FromExp
-> Maybe WhereFrag
-> Maybe RetExp
-> (# ArrayWriter, Int#, Int# #)
In the body of lambda with binder ww_svxsv :: ByteArray#
In the body of lambda with binder ww_svxsw :: Int#
In the body of lambda with binder ww_svxsx :: Int#
In the body of lambda with binder ww_svxsz :: TableName
In the body of lambda with binder ww_svxsB :: SetExp
In the body of lambda with binder ww_svxsC :: Maybe FromExp
In the body of lambda with binder ww_svxsD :: Maybe WhereFrag
In the body of lambda with binder ww_svxsE :: Maybe RetExp
In a case alternative: (TextBuilder ww_av2BQ :: ArrayWriter,
ww1_av2BR :: Int#,
ww2_av2BS :: Int#)
In a case alternative: ((#,,#) ww5_iv2AG :: ArrayWriter,
ww6_iv2AH :: Int#,
ww7_iv2AI :: Int#)
In a case alternative: ((#,,#) ww_svy6c :: ArrayWriter,
ww_svy6d :: Int#,
ww_svy6e :: Int#)
In the body of lambda with binder sc_svBxy :: Int#
In the body of lambda with binder sc_svBxx :: Int#
In the body of lambda with binder sg_svBxw :: (forall {s}.
MArray s
-> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter
In the body of letrec with binders $s$j_svBxQ :: Int#
-> Int#
-> ((forall {s}.
MArray s
-> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter) =>
(# ArrayWriter, Int#, Int# #)
In the body of lambda with binder ww_XoV :: ArrayWriter
In the body of lambda with binder ww1_XoW :: Int#
In the body of lambda with binder ww2_XoX :: Int#
In the body of letrec with binders $s$j_svBxJ :: Int#
-> Int#
-> ((forall {s}.
MArray s
-> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter) =>
(# ArrayWriter, Int#, Int# #)
In a rule attached to $j_sv2DD :: ArrayWriter
-> Int# -> Int# -> (# ArrayWriter, Int#, Int# #)
Substitution: <InScope = {sg_svBxw sg_svBxD}
IdSubst = []
TvSubst = []
CvSubst = [svBxw :-> sg_svBxw, svBxD :-> sg_svBxD]
As seen in the relevant Core (see below), the problem is the occurrence of an coercion variable in the RHS of a spec-constr rule which is not bound in the rule's LHS. This coercion witnesses the equality of the ArrayWriter
newtype and its representation:
newtype ArrayWriter
= ArrayWriter (forall s. TextArray.MArray s -> Int -> ST s Int)
The coercion variable appears to have arisen from the (N:ArrayWriter[0] :: ArrayWriter ~R# (forall s. MArray s -> Int -> ST s Int))
coercion appearing in the unspecialised binding's RHS (perhaps introduced by SpecConstr itself? we are currently checking this). If SpecConstr is indeed the source of the coercion variable then this seems like a bug; afterall, there should be no need to abstract over closed coercions.
However, this also seems quite similar to the issue observed in Note [Unbound RULE binders]
. Specifically, that Note specifies that we allow certain (namely, reflexive) coercion variables to occur in a rule's RHS despite being not bound by the LHS. The Note says that, while such occurrences are a bit strange, they are hard to avoid as the result of simplification.
The Core Lint offense suggests to me that the reflexivity restriction of Note [Unbound RULE binders]
may be too strict: Newtype coercions seem just as benign as reflexive coercions. Sadly, I don't have a minimal reproducer to demonstrate the issue.
Binding and questionable rule
...
join {
$j_sv2DD
:: ArrayWriter -> Int# -> Int# -> (# ArrayWriter, Int#, Int# #)
[LclId[JoinId(3)(Nothing)],
Arity=3,
Str=<SC(L,C(1,C(1,L)))><L><L>,
Unf=Unf{Src=<vanilla>, TopLvl=False,
Value=True, ConLike=True, WorkFree=True, Expandable=True,
Guidance=IF_ARGS [20 0 0] 432 10},
RULES: "SC:$j0"
forall (sc_svBxF :: Int#)
(sc_svBxE :: Int#)
(sg_svBxD
:: (forall {s}.
MArray s -> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter).
$j_sv2DD ($fMonoidBuilder3
`cast` (sg_svBxw
:: (forall {s}.
MArray s
-> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter))
sc_svBxE
sc_svBxF
= jump $s$j_svBxJ
sc_svBxF
sc_svBxE
@~(sg_svBxD
:: (forall {s}.
MArray s -> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter)]
$j_sv2DD (ww3_av2BZ [Dmd=SC(L,C(1,C(1,L))), OS=OneShot]
:: ArrayWriter)
(ww4_av2C0 [OS=OneShot] :: Int#)
(ww5_av2C1 [OS=OneShot] :: Int#)
= case ww3_av2BZ
`cast` (N:ArrayWriter[0]
:: ArrayWriter ~R# (forall s. MArray s -> Int -> ST s Int))
of nt_sv85q [Dmd=LC(S,C(S,C(S,L)))]
...