インデックス付きモナドの再記入表記

Question

私はConor McBrideの "Kleisli of excrageous fortune"の論文に従っており、彼のコードhereの実装を掲載しました。簡単に言えば、彼は次のタイプとクラスを定義しています。後者のバインドは完全に正常に動作

-- Conor McBride's "demonic bind" 
(?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i 
(?>=) = flip bind 

-- Conor McBride's "angelic bind" 
(>>=) :: (IMonad m) => m (a := j) i -> (a -> m b j) -> m b i 
m >>= f = bind (\(V a) -> f a) m 

：

type a :-> b = forall i . a i -> b i 

class IFunctor f where imap :: (a :-> b) -> (f a :-> f b) 

class (IFunctor m) => IMonad m where 
    skip :: a :-> m a 
    bind :: (a :-> m b) -> (m a :-> m b) 

data (a := i) j where 
    V :: a -> (a := i) i 

それから彼は、最初のインデックスを制限する(:=)を使用しています後者はバインドの2種類を定義します

： returnと failは、次の対応する定義を使用して、 RebindableSyntax拡張子を持つインデックス付きモナドを使用する do表記を再バインドするための

...しかし、私は以前のバインドを取得できないという問題があります。 (?>=)）を使用してください。私の代わりにすること(>>=)とreturnを定義しようとした：

(>>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i 
(>>=) = (?>=) 

return :: (IMonad m) => a :-> m a 
return = skip 

は、その後、私は特定のインデックスに生息する保証されたデータタイプ作成：

data Unit a where 
    Unit :: Unit() 

をしかし、私はのための新しい定義を使用してdo表記を再バインドしようとすると、 (>>=)とreturn、それは以下の例に示されているように、動作しない。

-- Without do notation 
test1 = skip Unit >>= \Unit -> skip Unit 

-- With do notation 
test2 = do 
    Unit <- skip Unit 
    skip Unit 

test1型チェックが、私はすべてのことRebindableSyntaxがtest1にdo表記desugar test2をしましょう、そうtest1型かどうかをチェックし、その後、なぜtest2がないたと思ったから、奇妙である、test2ないのですか？私が手にエラーがある：私は明示的なforall構文の代わりに、:->型演算子を使用する場合でも、

Couldn't match expected type `t0 -> t1' 
      with actual type `a0 :-> m0 b0' 
Expected type: m0 a0 i0 -> (t0 -> t1) -> m Unit() 
    Actual type: m0 a0 i0 -> (a0 :-> m0 b0) -> m0 b0 i0 
In a stmt of a 'do' block: Unit <- skip Unit 
In the expression: 
    do { Unit <- skip Unit; 
     skip Unit } 

エラーが残っています。

今、私は、あなたが(>>)を定義することはできないという "悪魔的な束縛"を使うことに別の問題があることを知っています。誰が私がGHCに通常「型式チェック」をしていたとしても、「悪魔の縛り」をなくすことができない理由を説明できますか？

Answer 1

IIUCの場合、GHC desugarerは、タイプチェッカー（source）の後に実際にを実行します。それはあなたが観察する状況が理論的に可能な理由を説明します。型チェッカーにはおそらくdo-notationのためのいくつかの特殊な型定義ルールがあり、それらは型チェックツールがdesugarredコードで行うことと矛盾するかもしれません。

もちろん、それらが一貫していると期待するのは妥当なので、私はGHCバグを提出することをお勧めします。