haskell - 反射会带来不一致的风险吗？

reflection包提供了一个类

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

和一个功能

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

仅给出这些，就可以通过给出实例来使事情变得很糟

instance Reifies s Int where
  reflect _ = 0

这将是不好的，因为例如

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

可以合法地产生1(通过通常的反射过程)或0(通过在应用reify之前专用于传递的函数)。

实际上，这种特殊的利用似乎被Reifies中包含一些Data.Reflection实例所阻止。我描述的邪恶实例将被视为重叠。如果启用重叠的实例，我相信专业化可能会因重叠带来的不确定性而受到阻碍。

不过，我想知道是否有某种方法可以通过一个阴暗的实例来公开它，也许是借助GADT或类似的方法。

最佳答案

我暂时说这不会带来不连贯的风险。经过一番修补后，我想出的劫持reflect的最佳方法是使用INCOHERENT，这不足为奇，足以产生不连贯性:

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