Add a `NOINLINE` pragma on `someNatVal` (#16586)
[ghc.git] / testsuite / tests / lib / base / T16586.hs
1 {-# LANGUAGE DataKinds, PolyKinds, RankNTypes, ScopedTypeVariables #-}
2
3 module Main where
4
5 import Data.Proxy
6 import GHC.TypeNats
7 import Numeric.Natural
8
9 newtype Foo (m :: Nat) = Foo { getVal :: Word }
10
11 mul :: KnownNat m => Foo m -> Foo m -> Foo m
12 mul mx@(Foo x) (Foo y) =
13 Foo $ x * y `rem` fromIntegral (natVal mx)
14
15 pow :: KnownNat m => Foo m -> Int -> Foo m
16 pow x k = iterate (`mul` x) (Foo 1) !! k
17
18 modl :: (forall m. KnownNat m => Foo m) -> Natural -> Word
19 modl x m = case someNatVal m of
20 SomeNat (_ :: Proxy m) -> getVal (x :: Foo m)
21
22 -- Should print 1
23 main :: IO ()
24 main = print $ (Foo 127 `pow` 31336) `modl` 31337
25
26 dummyValue :: Word
27 dummyValue = (Foo 33 `pow` 44) `modl` 456