Techniques de traçage des contraintes

Voici le scénario: j'ai écrit du code avec une signature de type et GHC ne peut pas déduire x ~ y pour certains xet y. Vous pouvez généralement lancer un os GHC et simplement ajouter l'isomorphisme aux contraintes de fonction, mais c'est une mauvaise idée pour plusieurs raisons:

1. Il ne met pas l'accent sur la compréhension du code.
2. Vous pouvez vous retrouver avec 5 contraintes là où une aurait suffi (par exemple, si les 5 sont impliquées par une contrainte plus spécifique)
3. Vous pouvez vous retrouver avec de fausses contraintes si vous avez fait quelque chose de mal ou si GHC n'est pas utile

Je viens de passer plusieurs heures à lutter contre le cas 3. Je joue avec syntactic-2.0et j'essayais de définir une version indépendante de domaine de share, similaire à la version définie dans NanoFeldspar.hs.

J'avais ceci:

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic

-- Based on NanoFeldspar.hs
data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi) 
      => a -> (a -> b) -> a
share = sugarSym Let

et GHC could not deduce (Internal a) ~ (Internal b) , ce qui n'est certainement pas ce que je recherchais. Donc, soit j'avais écrit du code que je n'avais pas l'intention de faire (ce qui nécessitait la contrainte), soit GHC voulait cette contrainte en raison d'autres contraintes que j'avais écrites.

Il s'avère que je devais ajouter (Syntactic a, Syntactic b, Syntactic (a->b))à la liste des contraintes, ce qui n'implique rien (Internal a) ~ (Internal b). Je suis essentiellement tombé sur les bonnes contraintes; Je n'ai toujours pas de moyen systématique de les trouver.

Mes questions sont:

1. Pourquoi GHC a-t-il proposé cette contrainte? Nulle part dans la syntaxe il n'y a de contrainte Internal a ~ Internal b, alors d'où vient le GHC?
2. En général, quelles techniques peuvent être utilisées pour retracer l'origine d'une contrainte dont GHC pense avoir besoin? Même pour les contraintes que je peux découvrir moi-même, mon approche consiste essentiellement à forcer brutalement le chemin offensant en écrivant physiquement des contraintes récursives. Cette approche consiste à descendre un trou infini de contraintes de lapin et est la méthode la moins efficace que j'imagine.

Tout d'abord, votre fonction a le mauvais type; Je suis presque sûr que ça devrait l'être (sans le contexte) a -> (a -> b) -> b. GHC 7.10 est un peu plus utile pour le souligner, car avec votre code d'origine, il se plaint d'une contrainte manquante Internal (a -> b) ~ (Internal a -> Internal a). Après avoir corrigé sharele type, GHC 7.10 reste utile pour nous guider:

1. Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))

2. Après avoir ajouté ce qui précède, nous obtenons Could not deduce (sup ~ Domain (a -> b))

3. Après avoir ajouté cela, nous obtenons Could not deduce (Syntactic a), Could not deduce (Syntactic b)etCould not deduce (Syntactic (a -> b))

4. Après avoir ajouté ces trois, il vérifie enfin typiquement; donc on se retrouve avec

   share :: (Let :<: sup,
             Domain a ~ sup,
             Domain b ~ sup,
             Domain (a -> b) ~ sup,
             Internal (a -> b) ~ (Internal a -> Internal b),
             Syntactic a, Syntactic b, Syntactic (a -> b),
             SyntacticN (a -> (a -> b) -> b) fi)
         => a -> (a -> b) -> b
   share = sugarSym Let

Je dirais donc que GHC n'a pas été inutile pour nous diriger.

En ce qui concerne votre question sur le traçage d'où GHC obtient ses exigences de contrainte, vous pouvez essayer les indicateurs de débogage de GHC , en particulier, -ddump-tc-tracepuis lire le journal résultant pour voir où Internal (a -> b) ~ tet (Internal a -> Internal a) ~ tsont ajoutés à l' Wantedensemble, mais ce sera une assez longue lecture .

Avez-vous essayé cela dans GHC 8.8+?

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi,
          _) 
      => a -> (a -> b) -> a
share = sugarSym Let

La clé est d'utiliser le type trou parmi les contraintes: _ => your difficult type