量化された制約
QuantifiedConstraints
8.6.1以降
制約が型上で量化することを可能にする．
QuantifiedConstraints拡張は，制約において新たなレベルの表現力を与える，量化された制約を導入する．例えば，次の例を考えてみよう．
code:qc01.hs
data Rose f a = Branch a (f (Rose f a))
instance (Eq a, ???) => Eq (Rose f a)
where
(Branch x1 c1) == (Branch x2 c2)
= x1 == x1 && c1 == c2
x1 == x2 から Eq aが要求される．これは問題ない．c1 == c2 からはEq (f (Rose f a))が要求されるが，これは現在のHaskellでは許されない．このような制約を解決する方法が無いからである．
QuantifiedConstraintsがあると，こう書けるようになる．
code:qc02.hs
instance (Eq a, forall b. (Eq b) => Eq (f b))
=> Eq (Rose f a)
where
(Branch x1 c1) == (Branch x2 c2)
= x1 == x1 && c1 == c2
ここで，量化された制約forall b. (Eq b) => Eq (f b) はローカルインスタンス宣言にいくらか似た振る舞いを見せ，このインスタンスを型付け可能にする．
論文 Quantified class constraints (by Bottu, Karachalias, Schrijvers, Oliveira, Wadler, Haskell Symposium 2017)はこの機能の技術的詳細を，例を挙げつつ表現しているため，このproposalに関する一次的な参考文献である． 動機
量化された制約を導入することには，主に2つの利点がある．
まず、前の例で解決できなかった制約が解決できるようになる．例えば，一般的なRose型(訳注：リスト以外のコレクション型が扱えるようなRose Treeのこと)のための次のインスタンス宣言を考えてみよう．
code:qc03.hs
data Rose f x = Rose x (f (Rose f x))
instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where
(Rose x1 rs1) == (Rose x2 rs2) = x1 == x2 && rs1 == rs2
この拡張により，forall b. Eq b => Eq (f b)という形式の制約が記述できるようになる．この制約は2つ目の(==)メソッドの使用により発生するEq (f (Rose f x))という制約を解決するために必要である．
次に，量化された制約はもっと簡潔で厳密に仕様を定めることを可能にする．例として，モナド変換子のためのMTL型クラスを考えてみよう．
code:qc04.hs
class Trans t where
lift :: Monad m => m a -> (t m) a
開発者は，モナド変換子というものがモナドmを取って新たなモナドt mにするということを知っている．しかしこの性質は上記の宣言で形式的に規定されているものではない．このことは，モナド変換子の合成を定義する際に問題となる．
code:qc05.hs
newtype (t1 * t2) m a = C { runC :: t1 (t2 m) a }
instance (Trans t1, Trans t2) => Trans (t1 * t2) where
lift = C . lift . lift
ここでの目標は，モナドmからt2 mにliftして，これをさらにliftしてt1 (t2 m)とすることである．しかし，この2回目のliftは(t2 m)がモナドであるときのみliftできるが，そのことが常に成り立つということを立証する方法はない．
量化された制約はこの性質をTransクラス宣言の中で明示することを可能にする．
code:qc06.hs
class (forall m. Monad m => Monad (t m)) => Trans t where
lift :: Monad m => m a -> (t m) a
構文の変更点
Haskell 2010 はcontext (型の中で=>の左にあるやつ)を次のように定義する．
code:qc07
context ::= class
| ( class1, ..., classn )
class ::= qtycls tyvar
| qtycls (tyvar atype1 ... atypen)
我々はclass (注意: この非終端記号の名前はかなり誤解を招く)に2つの新たな形式を追加する．具体的には，インスタンス宣言に何が登場できるかである．
code:qc08
class ::= ...
| context => qtycls inst
| context => tyvar inst
instの定義はHaskell Reportから変更されていない(乱暴に言えばただの型である)．これが言語への唯一の構文的変更である．
注意：
GHCがインスタンス宣言の拡張を許しているとき，このクラスの新しい形式についてもまったく同じように拡張を許す． 特に，ExplicitForAllとMultiParameterTypeClasses下では，次のような構文になる．
code:qc09
class ::= ...
明示的なforallは多くの場合絶対に不可欠であることに留意せよ．rose-treeの例を考えてみよう．
code:qc10.hs
instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where ...
forall bがなければ，意図に反して型変数bがインスタンス宣言全体にわたって量化されることになってしまう．
これらの新しい量化された制約の一つは，インスタンス宣言内だけでなく，他の制約がかける場所であればどこにでも現れる． とりわけ，値の束縛時や値コンストラクタ，式の型シグネチャに現れる可能性がある．例えば，
code:qc11.hs
f :: (Eq a, forall b. Eq b => Eq (f b)) => Rose f a -> Rose f a -> Bool
f t1 t2 = not (t1 == t2)
先頭に型変数を持つ形式を用いることで，以下の例のようなものが可能になる．
code:qc12.hs
instance (forall xx. c (Free c xx)) => Monad (Free c) where
Free f >>= g = f g
Iceland Jackの要約を参照せよ．要点は，=>の右側の部分は，クラスの代わりに，型変数(今回の場合c)が頭についていてもよいということである．とはいえ，量化された型変数であるべきではない． (訳注：ここでの型変数とはクラスのインスタンスが入るような型変数だと思われる．)
(注意: 以上の仕様は論文に記述されている範囲を超えているが，少しも新しい技術的困難を導入しなさそうである) 型付けの変更点
親クラス
次の例を考えてみよう．
code: qc13.hs
f :: forall m. (forall a. Ord a => Ord (m a)) => m Int -> Bool
f x = x == x
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の歴史を知らないので放置．) 重複
量化された制約は潜在的に局所的な公理の重なりにつながる可能性がある．たとえば次の例を考えてみよう．
code: qc14.hs
class A a where {}
class B a where {}
class C a where {}
class (A a => C a) => D a where {}
class (B a => C a) => E a where {}
class C a => F a where {}
instance (B a, D a, E a) => F a where {}
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を置く)を行ったとしよう．
code: qc15.hs
instance (B a, E a, D a) => F a where {}
C aを課すときに出会う最初に一致する公理はB a => C aである．利用可能な局所公理B aがあるので，プログラムは突然受け入れられるようになる．プログラムが受け入れられるかどうかをインスタンスコンテキストの順序が決定するというこの振る舞いは，開発者にとってかなり混乱を招くようだ．
疑わしきは拒否する．別の方法は，制約を解決するときに重複する公理をチェックすることである．一致する公理が複数見つかった場合は，そのプログラムを拒否する．このアプローチは動くプログラムを拒否するかもしれないという点で少し保守的である．しかし，それは開発者にとってはるかにわかりやすいようにみえる．というのも，開発者はプログラムが拒否された理由を説明する明確なメッセージを受け取ることができるからである．
バックトラックする．最後に，単純な形式のバックトラックを導入するという手もある．これは単純に，最初に出合った一致する公理を選択し，課した制約下での解決が失敗したときに，後戻りして必要な制約に一致する可能性のある他の公理を探すだけである．
これは開発者にとって最も直感的でわかりやすいアプローチであるように思える．開発者は，自分のコードに重複する公理が含まれている可能性があるという事実や，インスタンスコンテキストの順序付けについて心配する必要はなくなる．しかし，バックトラックは通常のインスタンス選択(インスタンスの重複がある場合)にも同様に適用されることになるであろうから，はるかに広範囲にわたる変更となり，型推論器に大きな影響を与える．
今のところ，GHCは疑わしきは拒否するを採用している．それが実際にはどれくらいつらいかを見て，必要ならもっと意欲的なことを試みる．
インスタンスの検索
重複の解決に鑑みて，型クラス制約C tを解決しようとするとき，インスタンスの検索は以下のように行われる．
1. まず，量化されていない制約C tが与えられていないかを確認する．もしあるなら，それを使用して制約を解決する．
2. そうでなければ，与えられた有効な量化された制約をすべて確認する．ちょうど1つがC tと一致する場合は，それを選ぶ．複数が一致した場合は，エラーにする．
停止性
GHCはインスタンス解決が確実に終了するように，Paterson条件を使用する．量化された制約に対してこれらの規則はどのように修正されるだろうか？2つの点に於いてである．
それぞれの量化された制約は，それだけを持ち，インスタンス宣言の終了規則を満たさなければない．
「それぞれのクラス制約(C t1 .. tn)」の後に，「または各量化された制約(forall as. context => C t1 .. tn)」を追加する．
2番目の項目は量化された制約の先頭であり，そのコンテキストではないことに注意せよ．もし，インスタンス宣言を使おうとすれば，先頭は解決しなければならない新しい目的になるためである(訳注：つまりはこのような制約にすると，インスタンスを決定するためにインスタンスを決定する必要が出て来る可能性があり，これでは停止性を保証できないということである)．
もちろん，UndecidableInstancesは，普段と同じように，Paterson条件を解除する．
一貫性
量化された制約はローカルインスタンスの宣言と少し似ているが，大きな違いが1つある．それは，ローカルインスタンスはユーザではなくコンパイラによって作成されるため，一貫性が失われることはないという点である．次の例を考えてみよう．
code: qc16.hs
f :: (forall a. Eq a => Eq (f a)) => f b -> f Bool
f x = ...rhs...
... 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`を解決できなかったりと不安定な部分が多く，実用できる段階にはないことに留意せよ．