content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  
  module GH55Spec (main, spec) where
  
  import Data.Constraint
  import Data.Constraint.Nat
  import GHC.TypeLits
  import Test.Hspec
  
  newtype GF (n :: Nat) = GF Integer deriving (Eq, Show)
  
  instance KnownNat n => Num (GF n) where
    xf@(GF a) + GF b = GF $ (a+b) `mod` (natVal xf)
    xf@(GF a) - GF b = GF $ (a-b) `mod` (natVal xf)
    xf@(GF a) * GF b = GF $ (a*b) `mod` (natVal xf)
    abs = id
    signum xf@(GF a) | a==0 = xf
                     | otherwise = GF 1
    fromInteger = GF
  
  x :: GF 5
  x = GF 3
  
  y :: GF 5
  y = GF 4
  
  foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
  foo m@(GF a) n@(GF b) = GF $ (a*b) `mod` (lcm (natVal m) (natVal n))
  
  bar :: (KnownNat m) => GF m -> GF m -> GF m
  bar (a :: GF m) b = foo a b - foo b a \\ Sub @() (lcmIsIdempotent @m) \\ lcmNat @m @m
  
  z :: GF 5
  z = bar x y
  
  spec :: Spec
  spec = describe "GH #53" $
           it "should normalize Lcm m m" $
             z `shouldBe` (GF 0 :: GF (Lcm 5 5))
  
  main :: IO ()
  main = hspec spec
  