タイプ型クラスを使用して統一していないと型家族

Question

はスニペット

{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeFamilies #-} 

import Data.Proxy 

monadify' :: forall m sig. (Monad m, Sig sig) => Proxy sig -> Monadify m sig 
monadify' p = monadify p (return() :: m()) 

type family Monadify f a where 
    Monadify f (a -> r) = a -> Monadify f r 
    Monadify f a = f a 

class Sig sig where 
    monadify :: Monad m => Proxy sig -> m() -> Monadify m sig 

を考えてみましょう私はインスタンスを与えられていないましたが、使用例はf :: Int -> String -> Bool, monadify' f :: Int -> String -> IO Boolだろう。

これは、次のエラーメッセージが表示されてです。TypeCheckに失敗：

Couldn't match expected type ‘Monadify m sig’ 
      with actual type ‘Monadify m0 sig0’ 
NB: ‘Monadify’ is a type function, and may not be injective 
The type variables ‘m0’, ‘sig0’ are ambiguous 
In the ambiguity check for the type signature for ‘monadify'’: 
    monadify' :: forall (m :: * -> *) sig. 
       (Monad m, Sig sig) => 
       Monadify m sig 
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes 
In the type signature for ‘monadify'’: 
    monadify' :: forall m sig. (Monad m, Sig sig) => Monadify m sig 

直感的に、私は（私はしたい、それはです。TypeCheckべきであると言うだろうが、GHCは単射として注釈されていないタイプの家族、によって混乱してしまいます下位互換性のためではない）。それはm()とProxyからプリイメージを回復することができます。だから私は本当にここで何が問題なのか分かりません。

編集：エラーメッセージが示すように

、私は私の場合、すべての問題を修正した、AllowAmbiguousTypesに投げることができました。しかし、私はその拡張機能を使用することの結果を知らないだけでなく、なぜ私の例が型チェックをしないのかを知っています。

Monadify m sigを一元化しようとするユニファイアと関係があると感じて、sigとmが同一であることを証明できないと推測します。ユニファイナーは渡された引数を見て、それらが同一であることを知る必要がありましたが、それでAllowAmbiguousTypesが役立つかもしれません。

Answer 1

monadify'では問題はmonadifyではありません。

はあなたが

monadify' :: forall m sig. (Monad m, Sig sig) => Monadify m sig 

を呼び出していると仮定し、ここでその周りにプロキシが存在しない、Monadify単射を仮定せずに、コンパイラがm,sigのにインスタンス化されるべきかを知ることは不可能です。これはまた、(Monad m, Sig sig)がどのような場合に使用されるべきかを理解するためにも必要です。あなたがAllowAmbiguousTypesを使用する場合は、次のチェックを入力しない

Monadify ((->) Bool) (IO Char)  ~ Bool -> IO Char 
Monadify IO   (Bool -> Char) ~ Bool -> IO Char 

---

：

test :: forall m sig. (Monad m, Sig sig) 
    => Proxy sig -> Proxy m -> Monadify m sig 
test t _ = monadify' t 
-- Type variable m0 is ambiguous 

monadify' :: forall m sig. (Monad m, Sig sig) 
      => Proxy m -> Proxy sig -> Monadify m sig 

で作業を代わりに試してみてください。またMonadifyがない単射であることに注意してください私はそれが必要とする場合であっても、それは非常にクリーン見つけるために、私が代わりにすべてのプロキシおよび使用の型の引数を削除しようと思い、個人的に

test :: forall m sig. (Monad m, Sig sig) 
    => Proxy sig -> Proxy m -> Monadify m sig 
test t _ = monadify' @ m t 

：

私たちは、しかし、明示的な型の引数mを渡すことによって、それを修正することができますあいまいな型。