impredicative型を作成する方法クラス型で動作する

Question

ImpredicativeTypesで何ができるかを見ていて、正確に何ができるのか見たいと思っていました。 TypeClassesとのやりとりに関しては、私が気がついたことに遭遇したときには奇妙な振る舞いがあります。

:t mempty 
mempty :: forall a. Monoid a => a 

:t Right 
Right :: forall a b. b -> Either a b 

は、だから、私はimpredicatively入力された表現を作るためにそれらを組み合わせることができ考え出し：拡張子がすべてのことは不合理でいないようですimpredicativeタイプを推測しないように私が知っているように

:t Right mempty 
Right mempty :: forall a b. Monoid b => Either a b 

は、ルックスこのような機能の追加を開始したときの一般的なケースでは、その型推論は必ずしも可能ではありません。私は文字通りRight型シグネチャにbの上に貼り付けていますよう

:t Right mempty :: forall a. Either a (forall b. Monoid b => b) 

、非常に合理的なように見えた私には：

は、だから、私はちょうど私が明示的にimpredicativeタイプを望んでいた事実を作ることを決定しましたタイプがmemptyの場合は、forallを持ち上げないでください。

しかし、それは私に次のエラー与える：むしろ不条理なようだ

No instance for (Monoid (forall b. Monoid b => b)) 

を。 Monoidはすべて定義の意味でMonoidです。

誰かが私にここで何が起こっているのか正確に説明できますか？実際にタイプを使用しているときに実際に1つのインスタンスを決定することは難しく、不可能であるという問題であり、GHCは実際には「No instance ...」ではなく「No explicit/decidable instance for ...」を意味しますか？

:t Right undefined :: forall a. Either a (forall b. b) 

タイプのチェックをして、私は指定されたimpredicativeタイプを私に戻っています：あなたは、状況のすべてのもののうち、型クラスを取る側の注意点としては

は、[OK]を動作するように表示されます。

Answer 1

この質問には返信がないとマークされていないので、私はコメントの中で述べられたことを繰り返し述べます。

基本的にはImpredicativeTypesは完全にサポートされておらず、誰も実際にどのように動作すべきか分かりません。だから、現在の状態で意味のある何かをしようとするのは悪い考えです。答えはちょうど「それをやろうとしないでください」です。