A memo on `Haskell Type Equality Constraints’

Yet another thing to know in GHC type reasoning

source:

Haskell Type Equality Constraints

概要

{-# LANGUAGE MultiParamTypeclasses #-}
instance C a a

と

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeFamilies #-}
instance (a ~ b) => C a b

は違うという話。つい上のように書いてしまって途方に暮れていた経験多数なのですが、なぜ下の方法だといいのでしょう。

なぜなら、型のマッチングはheadのマッチング後にcontextのマッチングという順序で行われるから：

What happens instead is that, when it sees myValue being used as a pair, GHC will first select the instance MyClass (a, b) without having even examined the constraints in the context. Only after it's already committed to using the instance MyClass (a, b) will it then examine the context and try to satisfy the MyClass a and MyClass b constraints.

この型を持つ変数の利用時に、二つ目の型パラメータに対応するフィールドを全く触らない場合では、そのsiteでは二つ目の型パラメータは未束縛な型（インスタンス）となる。これはもちろん一つ目の型パラメータと二つ目の型パラメータとが同一であるインスタンスにはマッチしない。従って利用可能なインスタンスがないというエラーになってしまう。もし型等価制約を持つinstanceでインスタンス化してあれば、この状況でC a bがまず選ばれ、その後で a ~ b という制約を付加して型推論が行われ、受理されるということのようだ。

なるほど。呼び出しの文脈では forall b . C a b としか型が定まらないのか。thePairの例でいうと fstは (a, b) -> a な型を持っているのだからその引数は(a, b) な型を持てることがまず必要で（型変数が型にinstantiateされるのとは違う。変数(a, b)が変数(a, a)にunificationできるかといえばそれは無理）、その後でさらなる推論： a , b それぞれが問題ないかどうかを判定するということのようだ。