reflection + template haskell issue

Main.hs

{-# LANGUAGE TemplateHaskell #-}
module Main where

import Reificator

main :: IO ()
main = pure $$(guardTH (operationTest 11 7 4) [|| () ||])

Reflection-TH.cabal

name:                Reflection-TH
version:             0.0.0
build-type:          Simple
cabal-version:       >=1.10

executable Reflection-TH
  main-is:             Main.hs
  other-modules:       Reificator
  other-extensions:    NoImplicitPrelude, Rank2Types, FlexibleContexts, UndecidableInstances, TypeFamilies, FlexibleInstances, ConstraintKinds, PolyKinds, TypeOperators, ScopedTypeVariables
  build-depends:       base >=4.7, arithmoi >=0.4, numeric-prelude >=0.4, reflection >=2.1, constraints >=0.8, template-haskell >= 2.16.0.0
  default-language:    Haskell2010

Reificator.hs

-- Doesn't build without this switch, uncomment for a successful build:
-- {-# OPTIONS_GHC -fno-solve-constant-dicts #-}

{-# 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")

stack.yaml

flags: {}
extra-package-dbs: []
packages:
- '.'
extra-deps: []
resolver: lts-18.5

stack.yaml.lock

# This file was autogenerated by Stack.
# You should not edit this file by hand.
# For more information, please see the documentation at:
#   https://docs.haskellstack.org/en/stable/lock_files

packages: []
snapshots:
- completed:
    size: 585817
    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/5.yaml
    sha256: 22d24d0dacad9c1450b9a174c28d203f9bb482a2a8da9710a2f2a9f4afee2887
  original: lts-18.5