haskell - GHC.TypeLits での ScopedTypeVariables と RankNTypes

Question

DataKindsタイプレベルのリテラルと一緒に使用して、タイプセーフな通貨変換ライブラリを作成しようとしています。これまでのところ、次のデータ型を定義しました。

data Currency (s :: Symbol) = Currency Double
    deriving Show

type USD = Currency "usd"
type GBP = Currency "gbp"

usd :: Double -> USD
usd = Currency

gbp :: Double -> GBP
gbp = Currency

data SProxy (s :: Symbol) = SProxy

それらの間で変換できる関数とともに：

convert :: forall a b. (KnownSymbol a, KnownSymbol b) => Currency a -> Currency b
convert (Currency a) = case (symbolVal (SProxy :: SProxy a), 
                             symbolVal (SProxy :: SProxy b)) of
          ("usd", "gbp") -> Currency (a * 0.75)
          ("gbp", "usd") -> Currency (a * 1.33)

ここではScopedTypeVariables、制約KnownSymbol aをに提供するために使用しましたsymbolVal SProxy。これは問題なく動作しますが、おそらくテキスト ファイルやfixerなどの API などの外部ソースからコンバージョン率を更新できるようにしたいと考えています。

明らかに、戻り値の型を でラップしてIO、形成することができます

convert :: forall a b. (KnownSymbol a, KnownSymbol b) => Currency a -> IO (Currency b)

しかし、私は純粋な API を維持できるようにしたいと考えています。最初に考えたのは、 を使用してコンバージョン率マップを取得することunsafePerformIOでしたが、これは安全ではないため、代わりgetConvertに の効果を持つタイプの別の関数を使用できると考えました。

getConvert :: IO (forall a b. (KnownSymbol a, KnownSymbol b) => Currency a -> Currency b)

(つまり、convert型関数を返す IO アクション) を次のように使用できるようにします。

do
    convert <- getConvert
    print $ convert (gbp 10) :: USD

しかし、私はこれを型チェックすることができませんでした - GHC は次のように不平を言っています:

Couldn't match expected type ‘forall (a :: Symbol) (b :: Symbol). 
                              (KnownSymbol a, KnownSymbol b) => 
                              Currency a -> Currency b’ 
with actual type ‘Currency a0 -> Currency b0’

GHCに の型を推測させたときreturn convert、それは私が望む型を推測しませんでしたが、代わりにforall a bを先頭の位置に移動しましたconvert' <- getConvert。No instance for (KnownSymbol n0)

私の質問は、なぜこれが型チェックを行わないのか、関数の正しい型は何でしょうgetConvertか?

ScopedTypeVariables最初は、量指定子をさまざまな方法でRankNTypes使用していることが事実である可能性があると考えましたforallが、トグルRankNTypesしても効果がありませんでした。また、GHC が提案したように量指定子を前に移動しようとしましたが、これでは必要なランク 2 型が得られません。