RULES involving newtypes don't fire
In the following program, the RULE involving the newtype constructor MkN
does not fire:
{-# NOINLINE f #-}
f :: a -> a
f x = x
newtype N = MkN { runN :: Int }
{-# RULES
"f/N" forall i. f (MkN i) = MkN (1000 * i)
#-}
main = print $ runN (f (MkN 17))
We get a result of 17
, instead of the expected 17000
.
This is because of the logic in GHC.Core.Rules.match_co
which only allows coercions which are reflexive or coercion variables, whereas in this example the coercion is Sym (N:N[0])
.
Note that this observation does not jeopardise the map/coerce
rule, which does function as intended. That is, map MkN
is indeed simplified away to a cast, and this happens AFTER the compulsory unfolding of MkN
into \ x -> x |> Sym N[0]
is inlined, as explained in Note [Getting the map/coerce RULE to work] in GHC.Core.SimpleOpt
.
One concern I have about these RULES involving newtypes is that firing the rule whenever we see x |> Sym N[0]
(or any coercion relating the same types as Sym N[0]
, to account for proof irrelevance) seems dodgy: the typechecker can insert coercions at will, in places which might not correspond to user-written applications of the newtype constructor MkN
. So we would end up firing the RULE in unexpected circumstances.