Thank you for suggestions (not exactly sure how I would reify a modulus value into a constructor of this kind, but that's perhaps for another project) and, well, I'll try to keep in mind that IncoherentInstances
is a big hammer.
EDIT: Ok this seems to be the way.
I see so I should be using IncoherentInstances
all along. I was happily using code similar to this and it only broke after using it from Template Haskell. It'd be a nice enhancement if this incoherence would be detected and warn about.
I still don't understand the reflection well, I thought I can do whatever I want in my representation of a dictionary as long as I provide instances for the lifted type.
This code uses Template Haskell, reflection and the numeric-prelude library so it's quite big. I dynamically create an instance of Additive
from numeric-prelude and use it in a simple equation operationTest
which tells whether a compilation should fail or not guardTH
. Here's a stack project in this gist.
stack build
failsstack build --ghc-options -fno-solve-constant-dicts
or stack build --ghc-options -O0
worksReificator.hs
{-# LANGUAGE Rank2Types, FlexibleContexts, TypeFamilies #-}
{-# LANGUAGE ConstraintKinds, PolyKinds, TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Reificator where
import Data.Proxy
import Data.Reflection
import Data.Constraint
import Data.Constraint.Unsafe
import Data.Kind
import qualified Algebra.Additive as AG
import NumericPrelude.Numeric
import NumericPrelude.Base
import Debug.Trace (trace)
import Language.Haskell.TH.Syntax (TExp(..))
import Control.Monad.Fail
newtype Lift (p :: Type -> Constraint) (a :: Type) (s :: Type) = Lift { lower :: a }
class ReifiableConstraint p where
data Def (p :: Type -> Constraint) (a :: Type) :: Type
reifiedIns :: Reifies s (Def p a) :- p (Lift p a s)
using :: forall p a. ReifiableConstraint p => Def p a -> (p a => a) -> a
using d m = reify d $ \(_ :: Proxy s) ->
let replaceProof :: Reifies s (Def p a) :- p a
replaceProof = trans proof reifiedIns
where proof = unsafeCoerceConstraint :: p (Lift p a s) :- p a
in m \\ replaceProof
instance ReifiableConstraint AG.C where
data Def AG.C a = ReifiedAdditive {
zero' :: a,
plus' :: a -> a -> a,
negate' :: a -> a }
reifiedIns = Sub Dict
instance Reifies s (Def AG.C a) => AG.C (Lift AG.C a s) where
zero = a where a = Lift $ zero' (reflect a)
a + b = Lift $ plus' (reflect a) (lower a) (lower b)
negate a = Lift $ negate' (reflect a) (lower a)
reifiedAdditive :: Integer -> Def AG.C Integer
reifiedAdditive prime =
ReifiedAdditive
0
(fmap (`mod` prime) . (+))
((`mod` prime) . negate)
debug = flip trace
operationTest modulus x y = result `debug` (
"modulus: " ++ show modulus ++
"\nx: " ++ show x ++
"\ny: " ++ show y ++
"\nsum: " ++ show left ++
"\nresult: " ++ show result
)
where inField = using $ reifiedAdditive modulus
left = inField $ x + y
result = (left == inField zero)
guardTH cond val = if cond then val else fmap TExp (fail "Nope")
Main.hs
{-# LANGUAGE TemplateHaskell #-}
module Main where
import Reificator
main :: IO ()
main = pure $$(guardTH (operationTest 11 7 4) [|| () ||])
Optimization levels shouldn't break compilation.
Optional: