Tecniche per i vincoli di traccia

Question

Ecco lo scenario: ho scritto del codice con una firma di tipo e le lamentele di GHC non sono state in grado di dedurre x ~ y per alcuni x e . Di solito puoi lanciare GHC un osso e aggiungere semplicemente l'isomorfismo ai vincoli di funzione, ma questa è una cattiva idea per diversi motivi:

1. Non enfatizza la comprensione del codice.
2. Si può finire con 5 vincoli in cui uno sarebbe sufficiente (per esempio, se il 5 è implicito da un vincolo più specifico)
3. Si può finire con vincoli fasulli se hai fatto qualcosa di sbagliato o se GHC viene inutile

ho appena trascorso diverse ore in lotta caso 3. sto giocando con syntactic-2.0, e stavo cercando di definire una versione indipendente dal dominio di share, simile alla versione definita in NanoFeldspar.hs.

ho avuto questo:

{-# 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), che non è certo quello che stavo per. Quindi o avevo scritto del codice che non intendevo (che richiedeva il vincolo), o GHC voleva quel vincolo a causa di altri vincoli che avevo scritto.

È risultato necessario aggiungere (Syntactic a, Syntactic b, Syntactic (a->b)) all'elenco dei vincoli, nessuno dei quali implica (Internal a) ~ (Internal b). Fondamentalmente sono incappato sui vincoli corretti; Non ho ancora un modo sistematico per trovarli.

Le mie domande sono:

1. Perché GHC propongo vincolo? Da nessuna parte in sintattica c'è un vincolo Internal a ~ Internal b, quindi da dove ha tratto il GHC?
2. In generale, quali tecniche possono essere utilizzate per tracciare l'origine di un vincolo che GHC ritiene sia necessario? Anche per i vincoli che io posso trovare , il mio approccio è essenzialmente quello di forzare brutalmente il percorso incriminato scrivendo fisicamente dei vincoli ricorsivi. Questo approccio sta fondamentalmente andando a scapito di una spirale infinita di vincoli e riguarda il metodo meno efficiente che io possa immaginare.

Answer 1

Prima di tutto, la funzione ha il tipo sbagliato; Sono abbastanza sicuro che dovrebbe essere (senza contesto) a -> (a -> b) -> b. GHC 7.10 è un po 'più utile nel farlo notare, perché con il tuo codice originale si lamenta di un vincolo mancante Internal (a -> b) ~ (Internal a -> Internal a). Dopo aver corretto il tipo share, GHC 7.10 rimane disponibile a guidarci:

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

2. Dopo aver aggiunto quanto sopra, otteniamo Could not deduce (sup ~ Domain (a -> b))

3. Dopo aver aggiunto che, otteniamo Could not deduce (Syntactic a), Could not deduce (Syntactic b) e Could not deduce (Syntactic (a -> b))

4. Dopo aggiungendo questi tre, infine, i tipografi; così si finisce con

   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 
   

Quindi direi GHC non è stato inutile in noi leader.

Per quanto riguarda le tue domande su tracing dove GHC ottiene i suoi requisiti di vincolo da, si potrebbe provare GHC's debugging flags, in particolare, -ddump-tc-trace, e poi leggere il registro risultante per vedere dove Internal (a -> b) ~ t e (Internal a -> Internal a) ~ t sono aggiunti al set Wanted, ma che sarà una lettura piuttosto lunga.