-fsolve-constant-dicts is too eager

Summary

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.

Steps to reproduce

1. Download the stack project
2. stack build fails
3. stack build --ghc-options -fno-solve-constant-dicts or stack build --ghc-options -O0 works

Reificator.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) [|| () ||])

Expected behavior

Optimization levels shouldn't break compilation.

Environment

• GHC version used: 8.10.4

Optional:

• Operating System: 20.04.2-Ubuntu
• System Architecture: x86_64