gistfile1.txt

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}

import Data.Proxy
import Data.Int
import GHC.Exts
import Unsafe.Coerce
import GHC.TypeLits

newtype Tagged s a = Tagged { unTagged :: a }

unproxy :: (Proxy s -> a) -> Tagged s a
unproxy f = Tagged (f Proxy)

class Reifies s a | s -> a where
  reflect' :: Tagged s a

-- For convenience
reflect :: forall s a proxy . Reifies s a => proxy s -> a
reflect _ = unTagged (reflect' :: Tagged s a)

newtype M s = M {getM :: Int} deriving Show

mkM :: Reifies s Int => Int -> M s
mkM = normalize . M
{-# INLINE mkM #-}

instance Reifies s Int => Num (M s) where
  M x + M y = normalize (M (x + y))
  M x - M y = normalize (M (x - y))
  M x * M y = normalize (M (x * y))
  abs x = x
  signum x = 1
  fromInteger = mkM . fromIntegral
  {-# INLINE (+) #-}

normalize :: Reifies s Int => M s -> M s
normalize m@(M x) = M $ x `mod` reflect m
{-# INLINE normalize #-}

unInt :: Int -> Int#
unInt (I# x) = x
{-# INLINE unInt #-}

test1 :: Int -> Int -> Int -> Int
test1 m x y = reify m $ \(_ :: Proxy s) -> getM (mkM x + mkM y :: M s)

newtype Magic a r = Magic (forall (s :: *). Reifies s a => Proxy s -> r)

-- | Reify a value at the type level, to be recovered with 'reflect'.
reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy

instance KnownNat n => Reifies n Int where
  reflect' = Tagged (fromIntegral $ natVal (Proxy @n))