Ошибка типа при приписывании действительного типа forall переменной let-bound

Является ли это ошибкой в проверке типов?

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

Тот факт, что приведенное выше не позволяет ввести проверку, но этот контур преуспевает:

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

приводит меня к мысли, что "слабая конверсия prenex" (см. стр. 23 of этот документ) может быть каким-то образом связана. Вложение a forall в контравариантное положение, в котором он не может быть "выплыл", кажется, защищает его от этой странной ошибки.

Ответ 1

Я думаю, что здесь происходит следующее: в стандартном выражении типа Damas – Milner пусть привязки - единственное место, где происходит обобщение типа. Типичная подпись, которую использует ваш неудачный пример, - это подпись типа шаблона, которая "сглаживает тип шаблона очевидным образом". Теперь, в этом примере, не является "очевидным", должно ли это ограничение выполняться до или после обобщения, но ваш неудачный пример демонстрирует, я думаю, что он применяется до обобщения.

Более конкретно: в привязке let let x = id in ... происходит то, что id type forall a. a->a получает экземпляр в монотип, например a0 -> a0, который затем присваивается как тип x и затем обобщается как forall a0. a0 -> a0. Если, как я думаю, перед генерализацией проверяется подпись типа шаблона, она по существу просит компилятор проверить, что монотип a0 -> a0 является более общим, чем политип forall a. a -> a, которого нет.

Если мы переместим сигнатуру типа на уровень привязки, let x :: forall a. a-> a; x = id in ... подпись будет проверена после обобщения (так как это явно разрешено для включения полиморфной рекурсии), и не возникает ошибка типа.

Является ли это ошибкой или нет, я думаю, вопрос мнения. Кажется, что не существует реальной спецификации, которая бы рассказывала нам, какое здесь правильное поведение; есть только наши ожидания. Я бы предложил обсудить этот вопрос с людьми GHC.

Ответ 2

Не настоящий ответ, но слишком длинный для комментария:
Это может быть ошибка. Играя немного с выражением, неудивительно

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

работает, если разрешено записывать явные подсказки. Тем не менее, это тип стандартного ранга 1. Некоторые другие варианты:

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

Хорошо, это работает, я не знаю, почему лямбда ведет себя по-другому, но это так. Однако:

$ 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 дает ту же ошибку). Это удивительно.