KnownNat: result changes depending on optimizations
Summary
The following program changes output from 1
(without optimizations) to 331
(with -O1
).
Steps to reproduce
{-# 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)
main :: IO ()
main = print $ (Foo 127 `pow` 31336) `modl` 31337
dummyValue :: Word
dummyValue = (Foo 33 `pow` 44) `modl` 456
$ ghc -fforce-recomp Mod.hs && ./Mod
1
$ ghc -fforce-recomp -O Mod.hs && ./Mod
313
Expected behavior
The expected output is 1
.
While dummyValue
is absolutely unused and should not have any impact, compilation with -O
somehow replaces 31337
in main
with 456
, producing 313. This can be also verified by dumping Core: it does not even contain 31337
anywhere, but surprisingly includes 456
.
Any of the following restores the behaviour of -O1
program to expected:
- Remove
module Main where
line. - Switch from
GHC.TypeNats
toGHC.TypeLits
. - Change
(`mul` x)
to(mul x)
.
Environment
- GHC version used: 8.6.4
- Operating System: macOS 10.14.4
- System Architecture: x64