型変数の比較3 - 非等価性は矛盾する

TypeEq による型の非等価性判定は結果として矛盾することがある，というお話．

型変数の比較で，引数の型が異なることを表現する関数を作ろうとして次のようなコードを書いたとする：

typeEq' x y = type'eq x y :: HFalse

ここでGHCのeagerなcontext reductionは TypeEq x y HFalse => x -> y -> HFalse から 文脈を完全に取り去ってしまうので，typeEq' は

typeEq' :: x -> y -> HFalse

となってしまう！！ 結局，

ghci> :t \x -> typeEq' x x
\x -> typeEq' x x :: x -> HFalse

のように，同じ型を与えても型チェックが通ってしまう！！
上のコードはわかりやすいけれど，型レで作ったEDSLなんかで型の非等価性に頼ったコードを書いていると結果として致命的なバグを仕込んでしまうかもしれない(例えば(TypeEq x y c, C c ...) => ... と書いて，型の非等価性によってCのインスタンスを選択しTypeEqの制約が消えた後に，型変数x yがある文脈でunifyされてしまう可能性がある)．．
型の等価性については インスタンスは TypeEq x x HTrue の形をしているため， 型変数が unifyされない限り制約は消えてなくなることはないので，矛盾することはない．非等価性はアテにならないのに等価性は使えるということだ．しかたがない．

型の非等価性を型検査器が保証するようなGHC拡張を提案してみるのも手かもしれない．って，やりすぎか．(追記)と思ったら3年前の記事に似たような話があった．

追記

矛盾は言い過ぎかも．TypeEq x y HFalse とあった場合，x y が「その時点で異なる変数である」のであって，型変数が将来的に単一化されたり同じ型が代入されることは普通にあるわけだ． 実際，このスレッドで，type equalityにはいくつか種類があるよ的なことが議論されている。