Data.Reflectionのトリックは、基底クラスの代わりにタイプファミリーを使用して実装できますか？

Question

パッケージからのData.ReflectionのGHC実装では、GHCが辞書パスを使用してタイプメーターをコンパイルする方法を利用するunsafeCoerceというトリックを使用します。実装は短いですので、私はここにその全体でそれを再現することができます

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

newtype Magic a r = Magic (forall (s :: *). Reifies s a => Proxy s -> r) 

reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r 
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy 

これは、それをバックに反映、タイプレベルの値を具体化することを可能にする：

ghci> reify (42 :: Integer) (\p -> reflect p) :: Integer 
42 

私は興味がありましたこのテクニックを使用する際には、私の目的上、機能的な依存関係ではなくReifiesの型ファミリを使用するのが便利だと思ったので、通常の変換を使用して実装を書き直そうとしました。

しかし、残念ながら、これはもう機能しません！私はGHCの理由を理解するためにどのように動作するかを十分に慣れていないよ、しかし

ghci> reify (42 :: Integer) (\p -> reflect p) :: Integer 
2199023255808 

：これはunsafeCoerceトリックを破るために十分有意にコンパイルを変更します。関数従属の代わりに関連型を使用してData.Reflectionを実装することは可能ですか？もしそうなら、何を変える必要がありますか？そうでない場合は、どうしてですか？

Answer 1

unsafeCoerceトリックは

Reifies s a => Proxy s -> r 

が(Reifies s a, a ~ Reflects s)に制約を拡大し

a -> Proxy s -> r 

として、あなたはこの重要な違反、実行時に、まったく同じ表現を持っているという事実を利用します仮定。これを解決するにはいくつかの方法があります。ここでは1です：

{-# language MultiParamTypeClasses, TypeFamilies, PolyKinds, KindSignatures, 
     RankNTypes, ScopedTypeVariables, TypeOperators #-} 
module TFReifies where 
import Data.Proxy 
import Unsafe.Coerce 
import Data.Type.Equality 

class Reifies s a where 
    type Reflects s :: * 
    reflect' :: proxy s -> a 

reflect :: (Reifies s a, a ~ Reflects s) => proxy s -> a 
reflect = reflect' 


newtype Magic a r = Magic (forall (s :: *). (Reifies s a) => Proxy s -> r) 

reify' :: forall a r. a -> (forall (s :: *). (Reifies s a) => Proxy s -> r) -> r 
reify' a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy 

reify :: forall a r. a -> (forall (s :: *). (Reifies s a, a ~ Reflects s) => Proxy s -> r) -> r 
reify a f = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> f p) 

---

ここであなたに近いバージョンです：私はこの質問を書いた、私はコアで覗くと発見し、私の驚きに、そのタイプの等式は、実行時の証人を持っていた後

class Reifies s where 
    type Reflects s :: * 
    reflect :: proxy s -> Reflects s 

newtype Magic a r = Magic (forall (s :: *). (Reifies s) => Proxy s -> r) 

reify :: forall a r. a -> (forall (s :: *). (Reifies s, a ~ Reflects s) => Proxy s -> r) -> r 
reify a f = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> f p) 
    where 
    -- This function is totally bogus in other contexts, so we hide it. 
    reify' :: forall a r. a -> (forall (s :: *). (Reifies s) => Proxy s -> r) -> r 
    reify' a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy