種類の降格（種類プロモーションとは対照的に）

Question

DataKinds拡張子は「値」（つまりコンストラクタ）を型に昇格します。たとえば、TrueとFalseは、種類が異なるBoolの別の種類になります。

私がしたいのは反対です。すなわち、型を値に降格します。このシグネチャを持つ関数は、罰金のようになります。

demote :: Proxy (a :: t) -> t 

私は実際にBoolのために、たとえば、これを行うことができます。

class DemoteBool (a :: Bool) where 
    demoteBool :: Proxy (a :: Bool) -> Bool 

instance DemoteBool True where 
    demoteBool _ = True 

instance DemoteBool False where 
    demoteBool _ = False 

しかし、私は私がしたい任意の型のインスタンスを記述する必要があると思いますその価値に降格する。これほど多くの定型文が含まれていない、これを行うためのより良い方法がありますか？

Answer 1

fromSing特に、singletonsの用途の一つである：

ghci> :m +Data.Singletons.Prelude 
ghci> :set -XDataKinds 
ghci> fromSing (sing :: Sing 'True) 
True 

それはまだ定型の多くを含むが、パッケージは、それの多くは、すでに定義されていると私はそれがテンプレートHaskellの提供と信じてより簡単に（そして少ないコードで）自分自身を生成させることができます。