[Git][ghc/ghc][master] Add a `NOINLINE` pragma on `someNatVal` (#16586)

[Marge Bot]

 Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
59f4cb6f by Iavor Diatchki at 2019-05-24T02:39:35Z
Add a `NOINLINE` pragma on `someNatVal` (#16586)

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

- - - - -


5 changed files:

- libraries/base/GHC/TypeLits.hs
- libraries/base/GHC/TypeNats.hs
- + testsuite/tests/lib/base/T16586.hs
- + testsuite/tests/lib/base/T16586.stdout
- + testsuite/tests/lib/base/all.T


Changes:

=====================================
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


=====================================
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


=====================================
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


=====================================
testsuite/tests/lib/base/T16586.stdout
=====================================
@@ -0,0 +1 @@
+1


=====================================
testsuite/tests/lib/base/all.T
=====================================
@@ -0,0 +1 @@
+test('T16586', normal, compile_and_run, ['-O2'])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/59f4cb6fb73ade6f9b0bdc85380dfddba93bf14b

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/59f4cb6fb73ade6f9b0bdc85380dfddba93bf14b
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20190523/2b428d91/attachment-0001.html>