haskell - 反射是否有不连贯的风险？

Question

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 或类似的帮助下。

Answer 1

我试探性地说，它不会冒不连贯的风险。经过一番修补，我能想出劫持 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