RULE quantification over equalities is fragile
We quantify over some equality constraints arising from the LHS of rules, as explained in Note [RULE quantification over equalities]
. We do so by inspecting the initial LHS Wanted constraints, before we have even attempted to canonicalise anything. This seems a bit fragile; for example, we are willing to quantify over equalities of the form A ~# F B
for a type family F
, but what if the constraint was of the form D A ~# D (F B)
for a datatype D
? We would now decide not to quantify over it because neither the LHS or RHS is headed by a type family, even though it is decomposable and decomposes to A ~# F B
, which we would quantify over.
Here's a contrived example I came up with that illustrates the problem:
type I :: k -> k
type family I a where
I a = a
f :: forall rr (a :: TYPE (I rr)). Proxy rr -> Proxy a -> Proxy a
f _ px = px
{-# NOINLINE f #-}
{-# RULES "f_id" forall (k :: Proxy LiftedRep) (x :: Proxy Int). f k x = x #-}
warning:
Forall'd constraint `LiftedRep ~ I LiftedRep'
is not bound in RULE lhs
Orig bndrs: [co_aBT, k, x]
Orig lhs: f @LiftedRep @Int k x
optimised lhs: f @LiftedRep @Int k x
|
16 | {-# RULES "f_id" forall (k :: Proxy LiftedRep) (x :: Proxy Int). f k x = x #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^