Técnicas para rastrear restrições

Aqui está o cenário: escrevi algum código com uma assinatura de tipo e as queixas do GHC não puderam deduzir x ~ y para alguns xe y. Geralmente, você pode jogar um osso no GHC e simplesmente adicionar o isomorfismo às restrições da função, mas essa é uma má idéia por vários motivos:

1. Não enfatiza a compreensão do código.
2. Você pode terminar com 5 restrições nas quais uma seria suficiente (por exemplo, se as 5 estiverem implícitas em mais uma restrição específica)
3. Você pode acabar com restrições falsas se tiver feito algo errado ou se o GHC estiver sendo inútil

Passei várias horas lutando contra o caso 3. Estou brincando syntactic-2.0e tentando definir uma versão independente do domínio share, semelhante à versão definida em NanoFeldspar.hs.

Eu tive isso:

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

e GHC could not deduce (Internal a) ~ (Internal b), que certamente não é o que eu estava procurando. Então, ou eu tinha escrito algum código que não pretendia (que exigia a restrição) ou o GHC queria essa restrição devido a outras restrições que eu havia escrito.

Acontece que eu precisava adicionar (Syntactic a, Syntactic b, Syntactic (a->b))à lista de restrições, nenhuma das quais implica (Internal a) ~ (Internal b). Eu basicamente me deparei com as restrições corretas; Ainda não tenho uma maneira sistemática de encontrá-los.

Minhas perguntas são:

1. Por que o GHC propôs essa restrição? Em nenhum lugar da sintática há uma restrição Internal a ~ Internal b, então de onde o GHC conseguiu isso?
2. Em geral, que técnicas podem ser usadas para rastrear a origem de uma restrição que o GHC acredita que precisa? Mesmo para as restrições que posso descobrir, minha abordagem é essencialmente bruta, forçando o caminho ofensivo, anotando fisicamente as restrições recursivas. Essa abordagem está basicamente diminuindo um buraco infinito de restrições e é o método menos eficiente que posso imaginar.

Primeiro de tudo, sua função tem o tipo errado; Tenho certeza de que deveria ser (sem o contexto) a -> (a -> b) -> b. O GHC 7.10 é um pouco mais útil em apontar isso, porque, com o seu código original, ele reclama de uma restrição ausente Internal (a -> b) ~ (Internal a -> Internal a). Depois de corrigir shareo tipo, o GHC 7.10 continua sendo útil para nos guiar:

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

2. Depois de adicionar o acima, obtemos Could not deduce (sup ~ Domain (a -> b))

3. Após acrescentando que, temos Could not deduce (Syntactic a), Could not deduce (Syntactic b)eCould not deduce (Syntactic (a -> b))

4. Depois de adicionar esses três, ele finalmente verifica; então acabamos com

   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

Então, eu diria que o GHC não tem sido inútil em nos liderar.

Quanto à sua pergunta sobre o rastreamento de onde o GHC obtém seus requisitos de restrição, tente os sinalizadores de depuração do GHC , em particular -ddump-tc-trace, e depois leia o log resultante para ver onde Internal (a -> b) ~ te os quais (Internal a -> Internal a) ~ tsão adicionados ao Wantedconjunto, mas isso será uma leitura bastante longa .

Você tentou isso no 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

A chave é usar o furo de tipo entre restrições: _ => your difficult type