Escriba error al atribuir un tipo de campo válido a una variable de límite

Question

¿Esto es un error en el comprobador de tipos?

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 

El hecho de que lo anterior falla al tipo de comprobación, pero esta contorsión tiene éxito:

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

me lleva a pensar que "débil conversión prenex" (ver la página 23 de this paper) podría estar relacionado de alguna manera . Incrustar un forall en una posición contravariante donde no puede "flotar" parece mantenerlo a salvo de este extraño error.

Answer 1

Lo que creo que está sucediendo aquí es esto: en estándar Damas – Milner tipo de inferencia, vamos a las fijaciones son el único lugar donde ocurre la generalización de un tipo. La firma de tipo que utiliza el ejemplo que falla es pattern type signature que "restringe el tipo de patrón de la manera obvia". Ahora, en este ejemplo, no es "obvio" si esta restricción debe ocurrir antes o después de la generalización, pero su ejemplo fallido demuestra, creo, que se aplica antes de la generalización.

Dicho más concretamente: en un let vinculante let x = id in ..., lo que sucede es que id 's tipo forall a. a->a se crea una instancia en un monotipo, a0 -> a0 decir, que se asigna luego como x' s tipo y luego se generaliza como forall a0. a0 -> a0. Si, como creo, la firma del tipo de patrón se comprueba antes de la generalización, básicamente se está pidiendo al compilador que verifique que el monotipo a0 -> a0 es más general que el politipo forall a. a -> a, que no lo es.

Si movemos la firma de tipo al nivel de enlace, let x :: forall a. a-> a; x = id in ..., la firma se comprueba después de la generalización (ya que esto está expresamente permitido para permitir la recursión polimórfica), y no se produce ningún error de tipo.

Si se trata de un error o no es, creo, una cuestión de opinión. No parece haber una especificación real que nos diga cuál es el comportamiento correcto aquí; solo hay nuestras expectativas Sugeriría discutir el asunto con la gente de GHC.

Answer 2

No es una respuesta real, pero es demasiado tiempo para un comentario:
Puede ser un error. Jugando un poco con la expresión, como era de esperar

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

funciona si la escritura foralls explícitas está activado. Sin embargo, es un tipo rango 1 estándar de pantano. Alguna otra variación:

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

bien, que funciona, no sé por qué el lambda se comporta de manera diferente, pero lo hace. Sin embargo:

$ 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 da el mismo error). Eso es sorprendente