Besteht bei der Reflexion Inkohärenz?

Question

Das reflection Paket bietet eine Klasse

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

und eine Funktion

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

Da nur diese, man könnte Chaos Dinge eher schlecht zum Beispiel, indem sie, bis die Instanz

instance Reifies s Int where 
    reflect _ = 0 

Dies wäre schlecht, weil zum Beispiel

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

könnte legitim entweder 1 (über den üblichen Reflexionsprozess) oder 0 (durch Spezialisierung der übergebenen Funktion vor der Anwendung reify) produzieren.

In Wirklichkeit scheint dieser besondere Exploit durch die Aufnahme von einigen Reifies Instanzen in Data.Reflection blockiert zu sein. Die böse Instanz, die ich beschrieben habe, wird als überlappend zurückgewiesen. Wenn überlappende Instanzen aktiviert sind, glaube ich, dass die Spezialisierung möglicherweise durch die Unsicherheitsüberlappung blockiert wird.

Dennoch frage ich mich, ob es eine Möglichkeit gibt, dies mit einer zwielichtigen Instanz zu offenbaren, vielleicht mit Hilfe von GADTs oder ähnlichem.

Answer 1

Ich versuchsweise sagen, dass es keine Inkohärenz riskiert. Nach einigem Tüfteln, könnte der beste Weg, ich komme mit reflectINCOHERENT verwendet kapern, die Inkohärenz zu erhalten unsurprisingly ausreichend ist:

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