컴파일 오류가

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이 오류를 제공합니다. 두 번째 예제가 컴파일되지 않는 이유는 무엇입니까?

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 

마지막 호출을 요구 하스켈에서 명확하게하는 명시 적 형식 인수를 고려한다. 그것은 하시다 uld는 Agda/Idris/Coq/...와 같은 의존형 언어에서 잘 작동합니다. 이들 (기본적으로 적어도)은 형식 인수를 명시 적으로 전달하기 때문입니다.