Skip to content

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information