Type Inference in Patterns

Question

ho notato che GHC voleva una firma tipo che credo dovrebbe essere dedotto. Ho ridotto al minimo il mio esempio fino a questo, che quasi certamente non fa nulla significativo (Non consiglio esecuzione su tuoi preferiti tipi):

{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, 
      TypeOperators, NoMonomorphismRestriction #-} 
module Foo where 

import Data.Typeable 

data Bar rp rq 

data Foo b = Foo (Foo b) 


rebar :: forall rp rq rp' rp'' . (Typeable rp', Typeable rp'') 
    => Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq) 
rebar p1 p2 (Foo x) = 
    -- The signature for y should be inferred... 
    let y = rebar p1 p2 x -- :: Foo (Bar rp rq) 
    -- The case statement has nothing to do with the type of y 
    in case (eqT :: Maybe (rp' :~: rp'')) of 
    Just Refl -> y 

Senza una firma di tipo sulla definizione di y, ottengo l'errore:

Foo.hs:19:20: 
    Couldn't match type ‘rq0’ with ‘rq’ 
     ‘rq0’ is untouchable 
     inside the constraints (rp' ~ rp'') 
     bound by a pattern with constructor 
        Refl :: forall (k :: BOX) (a1 :: k). a1 :~: a1, 
       in a case alternative 
     at testsuite/Foo.hs:19:12-15 
     ‘rq’ is a rigid type variable bound by 
      the type signature for 
      rebar :: (Typeable rp', Typeable rp'') => 
         Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq) 
      at testsuite/Foo.hs:12:20 
    Expected type: Foo (Bar rp rq) 
     Actual type: Foo (Bar rp rq0) 
    Relevant bindings include 
     y :: Foo (Bar rp rq0) (bound at testsuite/Foo.hs:16:7) 
     rebar :: Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq) 
     (bound at testsuite/Foo.hs:14:1) 
    In the expression: y 
    In a case alternative: Just Refl -> y 
Failed, modules loaded: none. 

la cattura è avvenuta dalla restrizione monomorfismo temuto su più occasioni, ho acceso NoMonomorphismRestriction, ma questo non cambia il comportamento.

Perché il tipo di y non dedurre essere il tipo di uscita della funzione?

Answer 1

La restrizione monomorfismo vale solo per attacchi di alto livello. Il compilatore è a conoscenza del tipo reale di , ma non esiste alcun modo per dedurne un tipo monomorfico; questa è la causa dell'errore di tipo.Se davvero volete disattivare attacchi Let monomorfa, è necessario utilizzare l'estensione corretta:

{-# LANGUAGE NoMonoLocalBinds #-} 

Con esso, il codice compila.

Per ulteriori dettagli sulle associazioni monomorfiche, see the ghc wiki.

Answer 2

non ho familiarità con l'algoritmo tipizzazione di GHC. Comunque, ecco la mia ipotesi sul perché il compilatore non riesca a capirlo.

Considerate questo codice:

rebar :: forall rp rq rp' rp'' . (Typeable rp', Typeable rp'') 
    => Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq) 
rebar p1 p2 (Foo x) = 
    let y = ... :: Foo (Bar rp Char) 
    in case (eqT :: Maybe (Char :~: rq)) of 
    Just Refl -> y 

Questo dovrebbe compilare, poiché corrispondenza Refl dimostra Char ~ rq, quindi y alla fine ha il tipo corretto ritorno Foo (Bar rp rq). Il programma passa il controllo del tipo.

Tuttavia, supponiamo invece abbiamo

let y = ... :: Foo (Bar rp rq) 

in questo caso, y ha già il tipo corretto, e il Refl è inutile. Ancora una volta, il programma passa il controllo del tipo.

Ora, supponiamo di avere l'annotazione del tipo no. Come sarebbe la compilazione capire quale è il tipo corretto per l'associazione let y = ...? Dopo tutto, ci sono (almeno) due portandoli ad una corretta digitazione di tutta rebar.

Questo potrebbe anche spiegare perché se si aggiunge _ -> y funziona: in tal caso il compilatore sa che lo Refl non è necessario. Invece, se si aggiunge y -> error "", non è possibile dedurre nessuna informazione su .

La storia completa reale può essere più complicato di quanto sopra: qui sto comodamente ignorando le informazioni provenienti dalla definizione di y, vale a dire rebar p1 p2 x. In altre parole, sto solo considerando i vincoli che il contesto pone sulla definizione su , e non quelli che vanno nella direzione opposta.

Nel tuo esempio l'equazione tipo è in realtà rp' ~ rp'' che sembra irrilevante w.r.t. il tipo di y alla fine. Forse il compilatore non è abbastanza intelligente da capirlo.