Add a `NOINLINE` pragma on `someNatVal` (#16586)
authorIavor Diatchki <>
Tue, 7 May 2019 20:02:27 +0000 (13:02 -0700)
committerMarge Bot <>
Fri, 24 May 2019 02:39:35 +0000 (22:39 -0400)
This fixes #16586, see `Note [NOINLINE someNatVal]` for details.

testsuite/tests/lib/base/T16586.hs [new file with mode: 0644]
testsuite/tests/lib/base/T16586.stdout [new file with mode: 0644]
testsuite/tests/lib/base/all.T [new file with mode: 0644]

index 7e3e514..449fc20 100644 (file)
@@ -105,6 +105,9 @@ someNatVal n
 -- @since
 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
 instance Eq SomeSymbol where
index b78608a..48428cb 100644 (file)
@@ -78,6 +78,65 @@ data SomeNat    = forall n. KnownNat n    => SomeNat    (Proxy n)
 -- @since
 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
 instance Eq SomeNat where
diff --git a/testsuite/tests/lib/base/T16586.hs b/testsuite/tests/lib/base/T16586.hs
new file mode 100644 (file)
index 0000000..37169e6
--- /dev/null
@@ -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 (file)
index 0000000..d00491f
--- /dev/null
@@ -0,0 +1 @@
diff --git a/testsuite/tests/lib/base/all.T b/testsuite/tests/lib/base/all.T
new file mode 100644 (file)
index 0000000..ff0c9f9
--- /dev/null
@@ -0,0 +1 @@
+test('T16586', normal, compile_and_run, ['-O2'])