反射風險是否不一致？

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之前專門化傳遞的函數）。

實際上，這個特定的漏洞利用似乎被Data.Reflection中包含一些Reifies實例所阻塞。我描述的邪惡實例將被拒絕爲重疊。如果啓用重疊實例，我認爲專業化可能會因重疊帶來的不確定性而受阻。

不過，我想知道是否有某種方法可以揭示這個陰暗的實例，也許在GADTs或類似的幫助下。

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