8.6.1以降

制約が型上で量化することを可能にする．

QuantifiedConstraints 拡張は，制約において新たなレベルの表現力を与える，量化された制約を導入する．例えば，次の例を考えてみよう．

x1 == x2 から Eq a が要求される．これは問題ない． c1 == c2 からは Eq (f (Rose f a)) が要求されるが，これは現在のHaskellでは許されない．このような制約を解決する方法が無いからである．

QuantifiedConstraints があると，こう書けるようになる．

ここで，量化された制約 forall b. (Eq b) => Eq (f b) はローカルインスタンス宣言にいくらか似た振る舞いを見せ，このインスタンスを型付け可能にする．

論文 Quantified class constraints (by Bottu, Karachalias, Schrijvers, Oliveira, Wadler, Haskell Symposium 2017)はこの機能の技術的詳細を，例を挙げつつ表現しているため，このproposalに関する一次的な参考文献である．

量化された制約を導入することには，主に2つの利点がある．

まず、前の例で解決できなかった制約が解決できるようになる．例えば，一般的なRose型(訳注：リスト以外のコレクション型が扱えるようなRose Treeのこと)のための次のインスタンス宣言を考えてみよう．

この拡張により， forall b. Eq b => Eq (f b) という形式の制約が記述できるようになる．この制約は2つ目の (==) メソッドの使用により発生する Eq (f (Rose f x)) という制約を解決するために必要である．

次に，量化された制約はもっと簡潔で厳密に仕様を定めることを可能にする．例として，モナド変換子のためのMTL型クラスを考えてみよう．

開発者は，モナド変換子というものがモナド m を取って新たなモナド t m にするということを知っている．しかしこの性質は上記の宣言で形式的に規定されているものではない．このことは，モナド変換子の合成を定義する際に問題となる．

ここでの目標は，モナド m から t2 m に lift して，これをさらに lift して t1 (t2 m) とすることである．しかし，この2回目の lift は (t2 m) がモナドであるときのみ lift できるが，そのことが常に成り立つということを立証する方法はない．

量化された制約はこの性質を Trans クラス宣言の中で明示することを可能にする．

この発想はかなり古くからある．導出可能な型クラスの7節を参照せよ．

Haskell 2010 は context (型の中で => の左にあるやつ)を次のように定義する．

我々は class (注意: この非終端記号の名前はかなり誤解を招く)に2つの新たな形式を追加する．具体的には，インスタンス宣言に何が登場できるかである．

inst の定義はHaskell Reportから変更されていない(乱暴に言えばただの型である)．これが言語への唯一の構文的変更である．

注意：

GHCがインスタンス宣言の拡張を許しているとき，このクラスの新しい形式についてもまったく同じように拡張を許す． 特に， ExplicitForAll と MultiParameterTypeClasses 下では，次のような構文になる．

明示的な forall は多くの場合絶対に不可欠であることに留意せよ．rose-treeの例を考えてみよう．

forall b がなければ，意図に反して型変数 b がインスタンス宣言全体にわたって量化されることになってしまう．

これらの新しい量化された制約の一つは，インスタンス宣言内だけでなく，他の制約がかける場所であればどこにでも現れる． とりわけ，値の束縛時や値コンストラクタ，式の型シグネチャに現れる可能性がある．例えば，

先頭に型変数を持つ形式を用いることで，以下の例のようなものが可能になる．

Iceland Jackの要約を参照せよ．要点は， => の右側の部分は，クラスの代わりに，型変数(今回の場合 c )が頭についていてもよいということである．とはいえ，量化された型変数であるべきではない．

(訳注：ここでの型変数とはクラスのインスタンスが入るような型変数だと思われる．)

(注意: 以上の仕様は論文に記述されている範囲を超えているが，少しも新しい技術的困難を導入しなさそうである)

論文を参照せよ．

次の例を考えてみよう．

x == x から Eq (m Int) 制約が必要だが，コンテキストは Ord (m a) 制約を解決する方法を提供するだけである．しかし，与えられた forall a. Ord a => Ord (m a) 制約から，我々は，2つめの制約 forall a. Ord a => Eq (m a) を導出でき，そこから我々は直ちに Eq (m Int) を解決できる．このプロセスは， Ord a 制約が与えられたら２つめの Eq a 制約を導出するという，既存の親クラスのふるまいと非常によく似ている．

注意：この親クラスの扱いは論文の範囲を超えているが，(ユーザにとっては特に望ましいものだ．|ユーザーが明示的に欲しいと言ってきた仕様だ．)(訳注: どちらとも読める．訳者がどちらもGHCの歴史を知らないので放置．)

量化された制約は潜在的に局所的な公理の重なりにつながる可能性がある．たとえば次の例を考えてみよう．

F a のインスタンス宣言を型検査するときは， F の親クラス C が成り立つことを検査する必要がある．このようにして，我々は次のものを含む理論の下で制約 C a を課そうとする．

インスタンス公理： (B a, D a, E a) => F a

インスタンスコンテキストからの局所公理： B a , D a , E a

これらの局所公理上の親クラス関係の閉包： A a => C a , B a => C a

しかしながら， A a => C a と B a => C a の公理は両方とも所望の制約 C a と一致する．これらの重複する局所公理を処理するためのアプローチはいくつかある．

最初を選ぶ．単に遭遇した中で最初に一致する公理を選ぶことができる．上記の例では，これは A a => C a になる．よって， A a を課す必要があるが，そのために我々は一致する有効な公理を持っていないので，上記のプログラムは拒否される．

しかし，インスタンスのコンテキストのためにわずかな調整( E a の前に D a を置く)を行ったとしよう．

C a を課すときに出会う最初に一致する公理は B a => C a である．利用可能な局所公理 B a があるので，プログラムは突然受け入れられるようになる．プログラムが受け入れられるかどうかをインスタンスコンテキストの順序が決定するというこの振る舞いは，開発者にとってかなり混乱を招くようだ．

疑わしきは拒否する．別の方法は，制約を解決するときに重複する公理をチェックすることである．一致する公理が複数見つかった場合は，そのプログラムを拒否する．このアプローチは動くプログラムを拒否するかもしれないという点で少し保守的である．しかし，それは開発者にとってはるかにわかりやすいようにみえる．というのも，開発者はプログラムが拒否された理由を説明する明確なメッセージを受け取ることができるからである．

バックトラックする．最後に，単純な形式のバックトラックを導入するという手もある．これは単純に，最初に出合った一致する公理を選択し，課した制約下での解決が失敗したときに，後戻りして必要な制約に一致する可能性のある他の公理を探すだけである．

これは開発者にとって最も直感的でわかりやすいアプローチであるように思える．開発者は，自分のコードに重複する公理が含まれている可能性があるという事実や，インスタンスコンテキストの順序付けについて心配する必要はなくなる．しかし，バックトラックは通常のインスタンス選択(インスタンスの重複がある場合)にも同様に適用されることになるであろうから，はるかに広範囲にわたる変更となり，型推論器に大きな影響を与える．

今のところ，GHCは疑わしきは拒否するを採用している．それが実際にはどれくらいつらいかを見て，必要ならもっと意欲的なことを試みる．

重複の解決に鑑みて，型クラス制約 C t を解決しようとするとき，インスタンスの検索は以下のように行われる．

1. まず，量化されていない制約 C t が与えられていないかを確認する．もしあるなら，それを使用して制約を解決する．

2. そうでなければ，与えられた有効な量化された制約をすべて確認する．ちょうど1つが C t と一致する場合は，それを選ぶ．複数が一致した場合は，エラーにする．

3. 量化された制約が一致しない場合は，インスタンスの解決およびインスタンスの重複の説明に従って，グローバルインスタンスを調べる．

GHCはインスタンス解決が確実に終了するように，Paterson条件を使用する．量化された制約に対してこれらの規則はどのように修正されるだろうか？2つの点に於いてである．

それぞれの量化された制約は，それだけを持ち，インスタンス宣言の終了規則を満たさなければない．

「それぞれのクラス制約 (C t1 .. tn) 」の後に，「または各量化された制約 (forall as. context => C t1 .. tn) 」を追加する．

2番目の項目は量化された制約の先頭であり，そのコンテキストではないことに注意せよ．もし，インスタンス宣言を使おうとすれば，先頭は解決しなければならない新しい目的になるためである(訳注：つまりはこのような制約にすると，インスタンスを決定するためにインスタンスを決定する必要が出て来る可能性があり，これでは停止性を保証できないということである)．

もちろん， UndecidableInstances は，普段と同じように，Paterson条件を解除する．

量化された制約はローカルインスタンスの宣言と少し似ているが，大きな違いが1つある．それは，ローカルインスタンスはユーザではなくコンパイラによって作成されるため，一貫性が失われることはないという点である．次の例を考えてみよう．

... rhs ... では、実際には任意の a に対して Eq (f a) のローカルインスタンスが存在する．しかし， f の呼び出し側では，コンパイラ自体が f に渡す証拠を生成する．例えば， f Nothing で呼び出された場合， f は Maybe であり，コンパイラは(呼び出し側で) forall a. E a => Eq (Maybe a) が成り立つことを証明しなければならない． Eq (Maybe a) の既存のインスタンス宣言を扱うことでこれを簡単に行うことができる．

つまり，量化された制約は矛盾を招くことはない．

ghc8.6.5現在， QunantifiedConstraints はかなり実験的な機能である．

equality(8.8で解決)や型族の解決(equalityの解決ができれば， t ~ Hoge h, ができなかったり，ネストした QuantifiedConstraints`を解決できなかったりと不安定な部分が多く，実用できる段階にはないことに留意せよ．