Opened 4 years ago

Last modified 4 years ago

#10418 new bug

Incorrect RULE warning on constructor, and inablilty to {-# INLINE [0] #-} constrcutor

Reported by: duncan Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #10417, #7398 Differential Rev(s):
Wiki Page:

Description

This is mentioned in passing in ticket #10417, but pulling it out here to track it.

Given a type

data Decoder s s' where
  Done     :: Decoder s s
  Sequence :: Decoder a b -> Decoder b c -> Decoder a c

and rules:

{-# RULES "Sequence/Done"
    forall sa. Sequence Done sa = sa
  #-}

{-# RULES "Sequence/Sequence"
    forall a b c. Sequence (Sequence a b) c
                = Sequence a (Sequence b c)
  #-}

GHC gives us warnings like:

    Rule "Sequence/Done" may never fire
      because ‘RulesExample.Sequence’ might inline first
    Probable fix: add an INLINE[n] or NOINLINE[n] pragma on ‘RulesExample.Sequence’

but it's currently syntactically invalid to write such a pragma:

{-# INLINE [0] Done #-}
{-# INLINE [0] Sequence #-}

Now there's two problems here:

  1. This warning is wrong most of the time
  2. The warning is actually right sometimes, but there's nothing you can do about it.

For 1, most of the time constructors remain as themselves in core, with no wrappers to get in the way of rule matching. In these cases the warning is just wrong.

For 2, for some constructors ghc does rewrite them. In this case the rewrite rule really will fail to match. But we cannot tell GHC to delay the rewriting of them because we cannot write INLINE pragmas for them. So for this case it would be useful to allow us to write INLINE pragmas.

In the above example, GHC will rewrite Done during optimisation, e.g. an excerpt from ticket #10417:

$WDone = \ @ s_anC -> Done @~ <s_anC>_N

working_example2 =
  \ @ b_aw2 -> AlterStack (working_example3) ($WDone)

This can and will interfere with rule matching. In this case it would be desirable to be able to write

{-# INLINE [0] Done #-}

Currently that's a syntax error.

For the case of nullary constructors, a workaround is to consistently use a smart constructor with an INLINE [0] pragma, and do all the rule matching on that.

Change History (3)

comment:1 Changed 4 years ago by duncan

comment:2 Changed 4 years ago by duncan

comment:3 Changed 4 years ago by thomie

Type of failure: None/UnknownIncorrect warning at compile-time
Note: See TracTickets for help on using tickets.