Does reflection risk incoherence?

Question

The reflection package offers a class

class Reifies s a | s -> a where
  reflect :: proxy s -> a

and a function

reify :: a -> (forall s . Reifies s a => Proxy s -> r) -> r

Given only these, one could mess things up rather badly by giving, for example, the instance

instance Reifies s Int where
  reflect _ = 0

This would be bad because, for instance,

reify (1 :: Int) $ \p -> reflect p

could legitimately produce either 1 (via the usual reflection process) or 0 (by specializing the passed function before applying reify).

In reality, this particular exploit seems to be blocked by the inclusion of a few Reifies instances in Data.Reflection. The evil instance I described will be rejected as overlapping. If overlapping instances are enabled, I believe the specialization may be blocked by the uncertainty overlapping brings.

Still, I'm wondering if there's some way to expose this with a shady instance, perhaps with the help of GADTs or some such.

Answer 1

I tentatively say it doesn't risk incoherence. After some tinkering, the best way I could come up with to hijack reflect used INCOHERENT, which is unsurprisingly sufficient to yield incoherence:

{-# LANGUAGE
  TypeFamilies, FlexibleInstances, MultiParamTypeClasses,
  ScopedTypeVariables #-}

import Data.Constraint
import Data.Proxy
import Data.Reflection

instance {-# INCOHERENT #-} Reifies (s :: *) Int where
  reflect _ = 0

reflectThis :: forall (s :: *). Dict (Reifies s Int)
reflectThis = Dict

-- prints 0
main = print $
  reify (1 :: Int) $ \(p :: Proxy s) ->
   case reflectThis :: Dict (Reifies s Int) of
     Dict -> reflect p