私の質問は、関連付けられた型の制約 (つまり、種類の制約の型) に等式制約を配置する方法についてです。
特定のユース ケースは、部分的に適用された型によってパラメータ化されたクラスです。
class Foo c where -- c has kind *->*->*
type Ctx c m r :: Constraint
f :: (Ctx c m r) => c m r -> c m r
特定の例では、次のように書きたいと思います。
data Bar m r = ...
instance Foo Bar where
type Ctx Bar m r = (m~Maybe b)
-- m must be a Maybe, I don't care what its parameter is
f = ...
しかし、GHC は「スコープ外: 型変数 b」と文句を言います。この制約を表現する他の方法はありません。すべてのインスタンスで「m~Maybe b」が必要なわけではないため、この制約を f の型シグネチャに移動することはできません。b はインスタンスのどこにもスコープに入っていませんが (おそらくこれは GHC が不満を言っていることです)、そうである必要はありません。関数
f :: (a ~ Maybe b) => a -> a -> a
は有効ですが、制約でこれを実行できない理由はわかりません。この問題は、最上位の制約と関連する型の制約で発生します。
おそらく関連するのはこの質問ですが、スコープ内にない変数との等価性が必要な場合を除きます。