Linear types and RULES

RULES can be used to rewrite a linear function to an unrestricted one, violating invariants.

For example, this program fails with -O -dlinear-core-lint.

{-# LANGUAGE LinearTypes, EmptyCase #-}

module Main where

{-# NOINLINE silly #-}
silly :: Bool %1 -> Bool
silly True = False
silly False = True

{-# RULES "silly" forall x. silly x = not x #-}

{-# NOINLINE g #-}
g :: Bool %1 -> Bool
g x = silly x

main :: IO ()
main = print (silly True)

The only solution I see is computing the usage environment of both sides and refusing to perform the rule if the usage environment or the RHS of the rule is disallowed in that context.

Originally reported by Richard at https://github.com/tweag/ghc/issues/413.