Getting GHC to accept type signature with KnownNat arithmetic
I am trying to implement the Chinese halting theorem , for the specific case of only two equations, using Data.Modular . The idea is that I can specify each equation with only one modular number ( x = a (mod m)
using a number a (mod m)
). Here is my implementation.
{-# LANGUAGE DataKinds, ScopedTypeVariables, TypeOperators #-}
import GHC.TypeLits
import Data.Proxy (Proxy (..))
import Data.Modular
crt :: forall k1 k2 i. (KnownNat k1, KnownNat k2, Integral i) => i `Mod` k1 -> i `Mod` k2 -> i `Mod` (k1 * k2)
crt a1 a2 = toMod $ (unMod a1)*n2*(unMod n2') + (unMod a2)*n1*(unMod n1')
where n1 = getModulus a1 :: i
n2 = getModulus a2 :: i
n2' = inv $ (toMod n2 :: i `Mod` k1)
n1' = inv $ (toMod n1 :: i `Mod` k2)
getModulus :: forall n i j. (Integral i, Integral j, KnownNat n) => i `Mod` n -> j
getModulus x = fromInteger $ natVal (Proxy :: Proxy n)
I get the following error: Could not deduce (KnownNat (k1 * k2)) arising from a use of ‘toMod’
. However, shouldn't the GHC do arithmetic for KnownNat (k1 * k2)
? Also, for some strange reason, it looks like if I had a type constructor Mod
instead of a function toMod
, everything would work. I don't understand how this should change ...
I'm looking for any fixes to help compile, including any extensions. However, I wish it weren't possible to make my own version of Data.Modular if possible. (I think I could make this work frantically and awkwardly by using the constructor Mod
directly).
source to share
A cheap, crappy way to make this compiler is to add FlexibleContexts
and then add KnownNat (k1 * k2)
to context crt
. Once I did that, I could successfully call it in ghci:
> crt (3 :: Mod Integer 5) (5 :: Mod Integer 7)
33
Have fun thinking about how to express Coprime k1 k2
as limitation ...; -)
source to share