Add a `NOINLINE` pragma on `someNatVal` (#16586)

This fixes #16586, see `Note [NOINLINE someNatVal]` for details.

5 files changed, 91 insertions, 0 deletions

diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 7e3e514be9..449fc20425 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -105,6 +105,9 @@ someNatVal n
 -- @since 4.7.0.0
 someSymbolVal :: String -> SomeSymbol
 someSymbolVal n   = withSSymbol SomeSymbol (SSymbol n) Proxy
+{-# NOINLINE someSymbolVal #-}
+-- For details see Note [NOINLINE someNatVal] in "GHC.TypeNats"
+-- The issue described there applies to `someSymbolVal` as well.
 
 -- | @since 4.7.0.0
 instance Eq SomeSymbol where
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index b78608af89..48428cb903 100644
--- a/libraries/base/GHC/TypeNats.hs
+++ b/libraries/base/GHC/TypeNats.hs
@@ -78,6 +78,65 @@ data SomeNat    = forall n. KnownNat n    => SomeNat    (Proxy n)
 -- @since 4.10.0.0
 someNatVal :: Natural -> SomeNat
 someNatVal n = withSNat SomeNat (SNat n) Proxy
+{-# NOINLINE someNatVal #-} -- See Note [NOINLINE someNatVal]
+
+{- Note [NOINLINE someNatVal]
+
+`someNatVal` converts a natural number to an existentially quantified
+dictionary for `KnowNat` (aka `SomeNat`).  The existential quantification
+is very important, as it captures the fact that we don't know the type
+statically, although we do know that it exists.   Because this type is
+fully opaque, we should never be able to prove that it matches anything else.
+This is why coherence should still hold:  we can manufacture a `KnownNat k`
+dictionary, but it can never be confused with a `KnownNat 33` dictionary,
+because we should never be able to prove that `k ~ 33`.
+
+But how to implement `someNatVal`?  We can't quite implement it "honestly"
+because `SomeNat` needs to "hide" the type of the newly created dictionary,
+but we don't know what the actual type is!  If `someNatVal` was built into
+the language, then we could manufacture a new skolem constant,
+which should behave correctly.
+
+Since extra language constructors have additional maintenance costs,
+we use a trick to implement `someNatVal` in the library.  The idea is that
+instead of generating a "fresh" type for each use of `someNatVal`, we simply
+use GHC's placeholder type `Any` (of kind `Nat`). So, the elaborated
+version of the code is:
+
+  someNatVal n = withSNat @T (SomeNat @T) (SNat @T n) (Proxy @T)
+    where type T = Any Nat
+
+After inlining and simplification, this ends up looking something like this:
+
+  someNatVal n = SomeNat @T (KnownNat @T (SNat @T n)) (Proxy @T)
+    where type T = Any Nat
+
+`KnownNat` is the constructor for dictionaries for the class `KnownNat`.
+See Note [magicDictId magic] in "basicType/MkId.hs" for details on how
+we actually construct the dictionry.
+
+Note that using `Any Nat` is not really correct, as multilple calls to
+`someNatVal` would violate coherence:
+
+  type T = Any Nat
+
+  x = SomeNat @T (KnownNat @T (SNat @T 1)) (Proxy @T)
+  y = SomeNat @T (KnownNat @T (SNat @T 2)) (Proxy @T)
+
+Note that now the code has two dictionaries with the same type, `KnownNat Any`,
+but they have different implementations, namely `SNat 1` and `SNat 2`.  This
+is not good, as GHC assumes coherence, and it is free to interchange
+dictionaries of the same type, but in this case this would produce an incorrect
+result.   See #16586 for examples of this happening.
+
+We can avoid this problem by making the definition of `someNatVal` opaque
+and we do this by using a `NOINLINE` pragma.  This restores coherence, because
+GHC can only inspect the result of `someNatVal` by pattern matching on the
+existential, which would generate a new type.  This restores correctness,
+at the cost of having a little more allocation for the `SomeNat` constructors.
+-}
+
+
 
 -- | @since 4.7.0.0
 instance Eq SomeNat where
diff --git a/testsuite/tests/lib/base/T16586.hs b/testsuite/tests/lib/base/T16586.hs
new file mode 100644
index 0000000000..37169e650a
--- /dev/null
+++ b/testsuite/tests/lib/base/T16586.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE DataKinds, PolyKinds, RankNTypes, ScopedTypeVariables #-}
+
+module Main where
+
+import Data.Proxy
+import GHC.TypeNats
+import Numeric.Natural
+
+newtype Foo (m :: Nat) = Foo { getVal :: Word }
+
+mul :: KnownNat m => Foo m -> Foo m -> Foo m
+mul mx@(Foo x) (Foo y) =
+  Foo $ x * y `rem` fromIntegral (natVal mx)
+
+pow :: KnownNat m => Foo m -> Int -> Foo m
+pow x k = iterate (`mul` x) (Foo 1) !! k
+
+modl :: (forall m. KnownNat m => Foo m) -> Natural -> Word
+modl x m = case someNatVal m of
+  SomeNat (_ :: Proxy m) -> getVal (x :: Foo m)
+
+-- Should print 1
+main :: IO ()
+main = print $ (Foo 127 `pow` 31336) `modl` 31337
+
+dummyValue :: Word
+dummyValue = (Foo 33 `pow` 44) `modl` 456
diff --git a/testsuite/tests/lib/base/T16586.stdout b/testsuite/tests/lib/base/T16586.stdout
new file mode 100644
index 0000000000..d00491fd7e
--- /dev/null
+++ b/testsuite/tests/lib/base/T16586.stdout
@@ -0,0 +1 @@
+1
diff --git a/testsuite/tests/lib/base/all.T b/testsuite/tests/lib/base/all.T
new file mode 100644
index 0000000000..ff0c9f963f
--- /dev/null
+++ b/testsuite/tests/lib/base/all.T
@@ -0,0 +1 @@
+test('T16586', normal, compile_and_run, ['-O2'])