如何将CRT提升至类型层面以实现多项式商的逆元定义

我有如下函数：

crt :: Integer -> [(Integer, Integer)]

该函数用于计算输入的中国剩余定理（CRT）结果。我希望将其提升至类型层面，因为我有一个以Nat为参数的数据类型，为了实现其逆元，需要通过CRT拆分模数。我一直在尝试理解这一过程，但网上相关资源有限且难以理解，希望能得到帮助。

补充细节 #

上述内容是对实际问题的简化，我定义了以下两个核心数据类型：

data Polynomial (n :: Nat) = Poly {coef :: [Mod n]}
data PolynomialQuotient (n :: Nat) (m :: Nat) = PolyQ {value:: (Polynomial n)}

PolynomialQuotient中的m是一个自然数，转换为整数再转为多项式后将成为多项式环的商。我正尝试为PolynomialQuotient定义recip函数，但当系数模数n为合数时，除法算法无法终止。

我希望将一个PolynomialQuotient映射为通过CRT得到的等价多项式商列表，例如将3x² + 1 (mod p(x)) (mod 4)映射为[1x² +1 (mod p(x)) (mod 2), x² (mod p(x)) (mod 2)]，对每个元素求逆后再合并得到原逆元。但我无法直接实现该函数，因为Haskell无法推导模数因子的KnownNat约束。

内容的提问来源于stack exchange，提问作者Pookibrine