Rule with KnownNat constraint does not fire
Summary
{-# RULES "foo -> bar" forall (x :: KnownNat m => Proxy m). foo x = bar x #-}
does not fire.
Steps to reproduce
{-# LANGUAGE DataKinds, PolyKinds, KindSignatures #-}
{-# OPTIONS_GHC -O2 -Wall -ddump-rule-firings #-}
module Main where
import Data.Proxy
import GHC.TypeNats
foo :: Proxy m -> Int
foo _ = 42
{-# NOINLINE foo #-}
bar :: KnownNat m => Proxy m -> Int
bar _ = 24
{-# RULES "foo -> bar" forall (x :: KnownNat m => Proxy m). foo x = bar x #-}
main :: IO ()
main = print $ foo (Proxy :: Proxy 1)
$ ghc-9.2 Modd.hs && ./Modd
[1 of 1] Compiling Main ( Modd.hs, Modd.o )
Rule fired: Class op show (BUILTIN)
Linking Modd ...
42
Expected behavior
I'd expect to see rule foo -> bar
fired and the program to return 24
.
This example has been distilled from https://github.com/Bodigrim/mod/issues/14
Environment
- GHC version used: 9.2.1