Errore di tipo durante l'attribuzione di un tipo forall valido a una variabile let-bound

Question

Si tratta di un errore nel correttore di tipi?

Prelude> let (x :: forall a. a -> a) = id in x 3 

<interactive>:0:31: 
    Couldn't match expected type `forall a. a -> a' 
       with actual type `a0 -> a0' 
    In the expression: id 
    In a pattern binding: (x :: forall a. a -> a) = id 

Il fatto che quanto sopra non riesce a digitare controllo, ma questa contorsione riesce:

Prelude> let (x :: (forall a. a -> a) -> Int) = (\f -> f 3) in x id 
3 

mi porta a pensare che "la conversione prenessa debole" (vedere a pagina 23 del this paper) potrebbe essere correlato in qualche modo . Incorporare un forall in una posizione controvariante in cui non può essere "fluttuato" sembra tenerlo al sicuro da questo errore strano.

Answer 1

Quello che penso stia succedendo qui è questo: nell'inferenza standard di tipo Milas –, i collegamenti sono l'unico posto in cui avviene la generalizzazione di un tipo. La firma del tipo utilizzata dall'esempio errato è pattern type signature che "vincola il tipo del modello in modo ovvio". Ora, in questo esempio, non è "ovvio" se questo vincolo debba verificarsi prima o dopo la generalizzazione, ma il tuo esempio fallito dimostra, penso, che viene applicato prima della generalizzazione.

Mettere più concretamente: in un let vincolante let x = id in ..., ciò che accade è che id 'tipo forall a. a->a s viene creata un'istanza in un monotipo, dire a0 -> a0, che viene poi assegnato come x' s tipo e viene poi generalizzata come forall a0. a0 -> a0. Se, come penso, la firma del tipo di modello viene verificata prima della generalizzazione, è essenzialmente chiedere al compilatore di verificare che il monotipo a0 -> a0 sia più generale del politipo forall a. a -> a, che non è.

Se spostiamo la firma del tipo sul livello di binding, let x :: forall a. a-> a; x = id in ... la firma viene verificata dopo la generalizzazione (poiché ciò è espressamente consentito per abilitare la ricorsione polimorfica) e non si verifica alcun errore di tipo.

Che si tratti di un errore o meno, credo sia una questione di opinione. Non sembra esserci una specifica che ci dirà qual è il comportamento giusto qui; ci sono solo le nostre aspettative. Suggerirei di discutere la questione con le persone della GHC.

Answer 2

Non è una risposta reale, ma è troppo lungo per un commento:
Potrebbe essere un bug. Giocare un po 'con l'espressione, senza sorprese

let x :: forall a. a -> a; x = id in x 3 

funziona se la scrittura di tute esplicite è abilitata. È un tipo di grado 1 standard di palude, però. Qualche altra variazione:

$ ghci-6.12.3 -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables 
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3 
3 

Va bene, che funziona, non so il motivo per cui la lambda comporta in modo diverso, ma lo fa. Tuttavia:

$ ghci -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables 
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3 

<interactive>:0:31: 
    Couldn't match expected type `t0 -> t1' 
       with actual type `forall a. a -> a' 
    The lambda expression `\ y -> id y' has one argument, 
    but its type `forall a. a -> a' has none 
    In the expression: \ y -> id y 
    In a pattern binding: (x :: forall a. a -> a) = \ y -> id y 

(7.2.2; 7.0.4 riporta lo stesso errore). Questo è sorprendente.