La fonction d'enregistrement de GADT échoue là où la déconstruction réussit

Question

J'essaie d'envelopper ma tête autour des GADTs, et je soupçonne qu'il se passe quelque chose de magique que je ne comprends pas.

Considérez ce qui suit:

class C t 

data T a where 
    T :: (C a) => { getT :: a } -> T a 

f :: C a => a ->() 
f = undefined 

class D t where 
    g :: t a ->() 

instance D T where 
    g (T x) = f x 

Tout cela est bon et compile avec succès.

Considérons maintenant une définition instance légèrement différente T:

instance D T where 
    g x = f (getT x) 

Cela ressemble exactement la même chose que ci-dessus, mais il y a une erreur de compilation. Qu'est-ce qu'il se passe ici? Le type de données T n'a pas de variables existentielles, il a une contrainte simple pour son seul constructeur mais c'est tout.

Answer 1

Qu'est-ce qui se passe ici est que le match de modèle

g (T x) = f x 

raconte l'typechecker que vous avez satisfait la contrainte C a vous pouvez donc utiliser f. Sans la correspondance de modèle, vous n'introduisez jamais C a donc il ne peut pas satisfaire la contrainte.

Il fonctionne de telle sorte qu'une valeur T something :: T a inclut également le dictionnaire pour C a et le rend disponible lorsque le modèle correspond à T. Cependant, en utilisant getT ne vous donne aucun moyen d'obtenir le dictionnaire pour C a (comme vous pouvez le voir du type getT :: T a -> a).

---

Pour la postérité l'erreur est

• No instance for (C a) arising from a use of ‘f’ 
    Possible fix: 
    add (C a) to the context of 
     the type signature for: 
     g :: T a ->() 
• In the expression: f (getT x) 
    In an equation for ‘g’: g x = f (getT x) 
    In the instance declaration for ‘D T’