Type safe modular arthmetic no annotation

Question

There's a number of Haskell modular arithmetic modules that implement type safe modular arithmetic with type annotations. Is it possible to pass in a variable in the type annotation?

For example in the mod module the following works

let x = 4 :: Mod 7
let y = 5 :: Mod 7
print x + y

Is there any way to achieve something similar to the following

let base = 7
let x = 4 :: Mod base
let y = 5 :: Mod base
print x + y

My problem here is that base is not a type. I'm unsure of the correct way to approach this problem or whether I'm thinking about this in the wrong way for functional languages. Thanks.

Update

In practice base will be the result of some computation I do not know in advance.

Answer 1

A value parameterized by the base is a polymorphic value:

import Data.Mod
import GHC.TypeNats (Nat)

nine :: KnownNat base => Mod base
nine =
  let x = 4
      y = 5
  in x + y   -- Let type inference do the work of deducing that x, y :: Mod base

To explicitly annotate these expressions, use ScopedTypeVariables to be able to refer to the base type variable. This also requires base to be explicitly quantified:

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Mod
import GHC.TypeNats (Nat)

nine :: forall base. KnownNat base => Mod base
nine =
  let x = 4 :: Mod base
      y = 5 :: Mod base
  in x + y

Answer 2

A value parameterized by the base is a polymorphic value:

import Data.Mod
import GHC.TypeNats (Nat)

nine :: KnownNat base => Mod base
nine =
  let x = 4
      y = 5
  in x + y   -- Let type inference do the work of deducing that x, y :: Mod base

To explicitly annotate these expressions, use ScopedTypeVariables to be able to refer to the base type variable. This also requires base to be explicitly quantified:

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Mod
import GHC.TypeNats (Nat)

nine :: forall base. KnownNat base => Mod base
nine =
  let x = 4 :: Mod base
      y = 5 :: Mod base
  in x + y

Answer 3

I found a similar question

Can I have an unknown KnownNat?

this can be applied in the given example as

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
module Main where

import GHC.TypeLits
import Data.Proxy
import Data.Mod as M

f x = x + 2

main :: IO ()
main = do
    let y = f 5
    let Just someNat = someNatVal y
    case someNat of
        SomeNat (_ :: Proxy n) -> do
            let x = 4 :: M.Mod n
            let y = 5 :: M.Mod n
            print $ x + y