I'm tyring to understand the use of phantom types in the package arithmoi (https://hackage.haskell.org/package/arithmoi-0.8.0.0). It helps to check if I'm working with the right residue class (Z/nZ).
The phantom type in question is data Mod (n :: Nat) = Mod Natural, and as I understand the constructor is not exported. But the constructor of SomeMod is exported, so I figure I must use it to construct ::Mod n variable.
Moreover, one can read in the documentation, but I can't use it.
case modulo n m of
SomeMod k -> process k -- Here k has type Mod m
InfMod{} -> error "impossible"
So I tried:
foo :: KnownNat m => Nat -> Nat -> Mod m
foo n m = case modulo n m of
(SomeMod k) -> k
otherwise -> error "some error"
I got an error about a variable m, m1 which is escaping its scope. I'm a bit puzzled.
Like IO, existentials cannot be escaped. Once in an existential, always in an existential. But that's okay -- if you're willing to admit KnownNat m, which your type signature claims you are willing to do, then you can just lift directly to that type.
foo :: KnownNat m => Natural -> Mod m
foo = fromIntegral