haskell-jp / questions #98 at 2021-08-20 17:17:30 +0900

はじめまして、Kasshiと申します。
ある時Free Arrowをつかいたくなって次のようなコードを書いてみたのですが、
`{-# LANGUAGE RankNTypes #-}`
`import Control.Category hiding (id ,(.))`
`import qualified Control.Category as Cat`

`newtype A f a b = Arr {unA :: forall r. Arrow r => (forall x y. f x y -> r x y) -> r a b}`
`instance Category (A f) where`
`id = Arr $ const Cat.id`
`Arr g . Arr f = Arr $ \p -> f p >>> g p`
Categoryのidのconst関数のところでGHCに
> Couldn't match type 'b0' with 'forall x y. f x y -> r x y'
と怒られてしまいました。

そこで`const Cat.id` を`\ _ -> Cat.id` と書き換えるとコンパイルが通りました。
多相関数がうまく型推論されていないことが原因と思われますが、これは仕様なのかバグなのかが分かりません。
知見をお持ちの方はご意見頂けると幸いです。

Impredicative polymorphismの罠にハマっているように見えます。私もあまり詳しくないのでちゃんと説明できないのですが... :cold_sweat:

GHC 8.10系だと通ってGHC 9.0.1だとコンパイルが通らなくなってるので、simplified subsumptionの影響を受けるコードっぽいですね

問題を単純化すると (const ()) :: (forall x. x -> x) -> () は通らなくて (\_ -> ()) :: (forall x. x -> x) -> () は通る、ということになります。前者は const () :: b -> () の b に forall x. x -> x というforallを含む型を当てはめることになるので（ImpredicativeTypesなしでは）エラー、後者はRankNTypesで引数の型が forall x. x -> x になれるのでオッケーみたいな感じですかね（よくわかってない）

返信ありがとうございます。多相な型は通常では推論されないということなのですね。もうすこし調べてみます。