erreur de compilation avec une contrainte de classe sur un type fantôme dans une méthode par défaut

Question

Ce module (un peu absurde) compile:

{-# 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 

Si je retire j'attendre d'hériter de la définition de f de l'instance, la valeur par défaut de la méthode et équivaut à la même chose.

{-# 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 

Cela ne fonctionne pas, cependant. GHC 8.0.2 donne cette erreur:

• 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 []’ 

Je ne sais pas comment lire cette erreur, parce que je ne sais pas où est inséré le x0 imaginaire. Pourquoi le deuxième exemple ne compile-t-il pas?

Answer 1

GHC convertit essentiellement votre code à ceci:

{-# 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 @[] 

Maintenant, dans la dernière ligne, le type de variable x n'est pas portée puisque nous ne disposons pas d'un forall x explicite. Même s'il l'était, il n'est pas passé à defaultF en tant qu'argument de type explicite. Ainsi, le dernier appel defaultF pourrait être fait sur n'importe quel monoid, peut-être un autre!

Pour cet appel, le moteur d'inférence génère une nouvelle variable de type x0, d'où le message d'erreur de type :-(

Peut-être que l'instance de GHC mécanisme résultant devrait être mis à jour, maintenant que les types ambigus sont autorisés (ce qui est un bon chose, OMI).

Pour un simple cas, envisagez

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

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

Le dernier appel besoins un argument de type explicite disambiguating, dans Haskell. Il wo uld fonctionne bien dans les langages dactylographiés comme Agda/Idris/Coq/... car ceux-ci (par défaut, au moins) passent leurs arguments de type explicitement.