No proper error message for linearity-violating RULES

Summary

RULES violating linearity aren't reported in a timely manner.

Steps to reproduce

{-# language LinearTypes #-}
{-# language TypeApplications #-}
{-# language DataKinds #-}
{-# language ScopedTypeVariables #-}

import Unsafe.Coerce
import GHC.Exts

toLinear :: forall m a b. (a %m -> b) %1-> (a %1-> b)
toLinear f = case unsafeEqualityProof @'One @m of
  UnsafeRefl -> f
{-# NOINLINE [1]  toLinear #-}

{-# RULES
"toLinear" forall a b. forall (f :: a -> b) (x :: a). toLinear f x = f x
 #-}

I was trying to see if I could pull one over on the type checker using rewrite rules. Surprisingly (to me), the above didn't produce an error message. However, compiling the above with -dcore-lint produces a core lint error.

Expected behavior

I expect the above to either produce a type error (at least if linearity is reflected in Core), or not to produce a core lint error (perhaps, if linearity is in the surface language only).

Environment

• GHC version used: 9.6

Optional:

• Operating System:
• System Architecture: