Rule with KnownNat constraint does not fire

added DataKinds needs triage rules labels

Thanks for the bug report. I remember trying something like this too and being surprised it didn't work.

Now, here the problem has to do with specifying an additional constraint for a rule. If we write

{-# RULES "foo -> bar" forall x. foo x = bar x #-}

we get the error:

    * No instance for (KnownNat m) arising from a use of `bar'
      Possible fix:
        add (KnownNat m) to the context of the RULE "foo -> bar"
    * In the expression: bar x
      When checking the rewrite rule "foo -> bar"
   |
16 | {-# RULES "foo -> bar" forall x. foo x = bar x #-}
   |                                          ^^^

The error is fair enough, but it's unclear how to go about adding KnownNat m to the context, given the special syntax of rewrite rules. You went with what seems to be the only option, which is to add it as a context to x, but I think that just gets GHC confused because now it expects x to take one value argument (the dictionary), and thus fails to match against Proxy @Nat @1 which is not of the right form (no value arguments).

I'm not too familiar with the syntax of rewrite rules myself, so perhaps someone else (e.g. @simonpj) can chime in and give a better explanation of the problem/possible solutions.

From my perspective it would be totally fine to prohibit such rules, no big deal. But silently ignoring them is problematic.

I don't think there is much hope writing rewriting an application of foo to an application of bar because the arguments of foo don't contain enough information (ie no KnownNat dictionary) to write to an application of bar.

OTOH, the rule as written doesn't seem to make much sense, in core I would expect the argument x to be represented by a function due to the type containing a => but somehow this is accepted as an argument to foo and bar.

added Pnormal Tbug labels

removed needs triage label

assigned to @mpickering

@mpickering will investigate why this rule is accepted at all.

You can see that the function theory is entirely correct.

==================== Tidy Core rules ====================
"foo -> bar"
    forall (@(m :: Nat))
           ($dKnownNat :: KnownNat m)
           (x :: KnownNat m => Proxy m).
      foo @Nat @m (x $dKnownNat)
      = I# 24#

and if you modify the program like so, you can get the rule to fire.

{-# 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

test_x :: KnownNat m => Proxy m
test_x = Proxy
{-# NOINLINE test_x #-}

{-# RULES "foo -> bar" forall (x :: KnownNat m => Proxy m). foo x = bar x #-}

main :: IO ()
main = do
  print $ foo (test_x @1)

This is not very obvious, I'm not done yet.

The reason the for the structure of the rule can be boiled down the inferred type of the following program:

check (x :: KnownNat m => Proxy m) = bar x

which gets inferred type

check :: KnownNat m => (KnownNat m => Proxy m) -> Int

but of course if you write

check (x :: forall m . KnownNat m => Proxy m) = bar x

then that gets rejected (correctly) with a type error

Test.hs:9:49: error:
    • No instance for (KnownNat m0) arising from a use of ‘bar’
    • In the expression: bar x
      In an equation for ‘check’:
          check (x :: forall m. KnownNat m => Proxy m) = bar x
  |
9 | check (x :: forall m . KnownNat m => Proxy m) = bar x
  |

@simonpj Any opinion about this issue?

From my perspective it would be totally fine to prohibit such rules, no big deal. But silently ignoring them is problematic.

The question is: what rules do you want to prohibit? Here the rule (making the dictionaries explicit) is

"foo -> bar"
    forall (@(m :: Nat)) ($dKnownNat :: KnownNat m)  (x :: KnownNat m => Proxy m).
      foo @Nat @m (x $dKnownNat) = I# 24#

So anytime it sees foo @Nat @<ty> (<expr1> <expr2>), where <expr1> :: KnownNat <ty> => Proxy <ty> and <expr2> :: KnownNat <ty>, it'll fire the rule.

But in the program you have no such expression. All we have is

main_s11S
  = case foo @Natural @1 (Data.Proxy.Proxy @Natural @1) of
    { GHC.Types.I# n_a11I ->
    GHC.Show.itos n_a11I (GHC.Types.[] @Char)
    }

So the rule doesn't fire. As Matthew says, it's not a useless rule -- there exist programs where it will fire. It's not silently ignored.

The difficulty is that I can't see grounds for rejecting it.

If we cannot reject such rules automatically, could someone knowledgeable please document the behaviour in the user's manual?

added documentation label

I think it's pretty much this:

A rule that has a forall binder with a polymorphic type, is likely to fail to fire. E.g.
```
{-# RULES forall (x :: forall a. Num a => a -> a).  f x = blah #-}  
```
Here x has a polymorphic type. The applies to a forall'd binder with a type class constraint, such as
```
{-# RULES forall @m (x :: KnownNat m => Proxy m).  g x = blah #-} 
```
See #21093 (closed) for discussion.

Would that help? If so could someone add that to the user manual? @mpickering @bgamari

mentioned in merge request !8035 (closed)

Thanks, @simonpj!

closed

@Bodigrim is that text positively helpful? Then we should add it to the user manual. Reopening.

That's precisely what @Bodigrim did in !8035 (closed).

reopened

Ha ok, thank you. That's what I had missed.

closed

added backport needed:9.4 label

Present in %9.4.1 as df77c085.

removed backport needed:9.4 label

mentioned in issue #22474

Rule with KnownNat constraint does not fire

Summary

Steps to reproduce

Expected behavior

Environment

Child items ...

Activity