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: