コンパイルエラーが

Question

この（やや無意味な）モジュールがコンパイルされます。私はfのインスタンスの定義を削除した場合、私はメソッドのデフォルトを継承することを期待する

{-# LANGUAGE AllowAmbiguousTypes #-} 
{-# LANGUAGE ExplicitForAll #-} 

module Foo where 

class A t where 
    f :: forall x m. Monoid x => t m -> m 
    f = undefined 

instance A [] where 
    f = undefined 

同じものになります。

{-# LANGUAGE AllowAmbiguousTypes #-} 
{-# LANGUAGE ExplicitForAll #-} 

module Foo where 

class A t where 
    f :: forall x m. Monoid x => t m -> m 
    f = undefined 

instance A [] where 

ただし、これは機能しません。

• Could not deduce (Monoid x0) 
    arising from a use of ‘Foo.$dmf’ 
    from the context: Monoid x 
    bound by the type signature for: 
       f :: Monoid x => [m] -> m 
    at src/Foo.hs:10:10-13 
    The type variable ‘x0’ is ambiguous 
    These potential instances exist: 
    instance Monoid a => Monoid (IO a) -- Defined in ‘GHC.Base’ 
    instance Monoid Ordering -- Defined in ‘GHC.Base’ 
    instance Monoid a => Monoid (Maybe a) -- Defined in ‘GHC.Base’ 
    ...plus 7 others 
    (use -fprint-potential-instances to see them all) 
• In the expression: Foo.$dmf @[] 
    In an equation for ‘f’: f = Foo.$dmf @[] 
    In the instance declaration for ‘A []’ 

私が想像x0が挿入されている場合、私は知らないので、このエラーを読んでするかどうかはわかりません：GHC 8.0.2は、このエラーが発生します。なぜ2番目の例はコンパイルされませんか？

Answer 1

GHCは、基本的にこれにあなたのコードに変換されます。

{-# LANGUAGE AllowAmbiguousTypes #-} 
{-# LANGUAGE ExplicitForAll #-} 

module Foo where 

defaultF :: forall t x m. (A t, Monoid x) => t m -> m 
defaultF = undefined 

class A t where 
    f :: forall x m. Monoid x => t m -> m 
    f = defaultF @t @x @m 

instance A [] where 
    f = defaultF @[] 

今、私たちは明示的なforall xを持っていないので、x変数の型がスコープ内にない最後の行に。たとえあったとしても、明示的な型引数としてdefaultFに渡されません。したがって、最後のdefaultFコールは、おそらく別のモノモノでも可能です！その呼び出しのために

、推論エンジンは、新鮮なx0型変数を生成し、それゆえ

:-(タイプのエラーメッセージは、たぶんメカニズムを導出するGHCのインスタンスが良いである（あいまいなタイプが許可されている今あること、更新する必要があります事、IMO）。単純なケースでは

、

a :: forall x. Monoid x => Int 
a = undefined 

b :: forall x. Monoid x => Int 
b = a 

を考える最後の呼び出しは Haskellでは曖昧さ明示的な型の引数を、必要とする。それはめざしuldはAgda/Idris/Coq/...のような依存型言語では正常に動作します。なぜなら、これらの（デフォルトでは少なくとも）型引数を明示的に渡すからです。