Add GCD and LCM type families to GHC.TypeNats
Motivation
Several libraries define a type family for the greatest common divisor on Nat:
-
constraintsdefinesGcdand provides a magic hack to derive(KnownNat n, KnownNat m) :- KnownNat (Gcd n m). -
ghc-typelits-extradefinesGCDand provides a type checker plugin to evaluate this type family. -
o-clockdefinesGcd, which can be evaluated only for statically knownNats. -
typenumsdefinesGCD, also only for statically known indices.
This is a suboptimal situation, causing significant duplication and (more importantly) complicating APIs of respective packages and interoperation between them.
(The main application of type-level gcd is defining type-level rational numbers, but it is also important for safe modular arithmetic)
Proposal
Provide a type family GCD (and, probably, LCM) immediately from GHC.TypeNats with built-in evaluation support.