Ответ 1

Это не стандарт

В ответ на вопрос

Простой ответ заключается в том, что стандартный Haskell не разрешает объявление синонима типа, т.е. синоним типа =>. В отчете 2010 синтаксис объявления синонима типа:

type тип simpletype =

где type, если вы смотрите на раздел 4.1.2, не может содержать контекст.

Кстати, наличие переменной типа a в контексте не имеет значения. Без расширений GHC отклоняет

type IrrelevantConstraint a = Num Int => [a]

или, если на то пошло,

type QualifiedT = Num Int => String

Кроме того, даже если такой синоним типа разрешен, его нетривиальное использование будет стандартным Haskell, поскольку ручная замена показывает:

List2 a      === forall a.   Num a => [a]        -- Okay
List2 a -> b === forall a b. (Num a => [a]) -> b -- Not okay
a -> List2 b === forall a b. a -> Num b => [b]   -- Not okay

И т.д. для Maybe (List2 a) и т.д. В каждом случае это не то, что это тип более высокого ранга в обычном смысле. Я добавил явную полную нотацию, которая также, конечно, не стандартная, чтобы подчеркнуть этот факт.

Скорее, проблема в том, что каждый тип неадекватно квалифицирован, потому что внутри типа появляется =>. Опять же, если вы посмотрите разделы отчета 2010 года на подписи типов выражений и объявления, вы увидите, что => не является, строго говоря, частью типа, а скорее синтаксически отличной вещью, например:

exp → exp :: [context =>] type

Так как List2 недействителен Haskell2010, для его работы требуется некоторое расширение языка. В нем специально не указано, что RankNTypes разрешает объявления синонима типа, но, как вы заметили, это имеет такой эффект. Почему?

Там подсказка в документах GHC на RankNTypes:

Опция -XRankNTypes также требуется для любого типа с форелом или контекстом справа от стрелки (например, f :: Int -> forall a. a->a или g :: Int -> Ord a => a -> a). Такие типы технически ранжированы 1, но явно не Haskell-98, а дополнительный флаг, похоже, не стоит беспокоить.

Пример g связан с нашей проблемой List2: там нет forall, но есть контекст справа от стрелки, что является третьим примером, приведенным выше. Как это бывает, RankNTypes также включает второй пример.

Боковое перемещение по шаблону Haskell

В котором снимается пропущенный обход, г-н Форолл обнаруживается в неожиданном месте, и размышления о рангах и контекстах

Я не знаю, обязательно ли представление декларации шаблона Haskell обязательно связано с внутренним представлением или операцией typechecker. Но мы находим что-то необычное: a forall, где мы не ожидали бы, и без переменных типа:

> import Language.Haskell.TH
> :set -XTemplateHaskell
> runQ [d|type List2 a = Num a => [a]|]
[TySynD List2_2
        [PlainTV a_3]
        (ForallT []
                 [ClassP GHC.Num.Num [VarT a_3]]
                 (AppT ListT (VarT a_3)))]

-- simpler example:
> runQ [d|type T = Num Int => Int|]
[TySynD T_0
        []
        (ForallT []
                 [ClassP GHC.Num.Num [ConT GHC.Types.Int]]
                 (ConT GHC.Types.Int))]

Примечательная вещь здесь явно ложная ForallT. В Template Haskell это имеет смысл, потому что ForallT является единственным конструктором type с полем Cxt, то есть может содержать контекст. Если typechecker аналогично объединяет forall и контексты ограничений, имеет смысл, что RankNTypes повлиял на его поведение. Но делает?

Как реализовано в GHC

В котором обнаруживается, почему RankNTypes позволяет List2

Точная ошибка, которую мы получаем:

Illegal polymorphic or qualified type: Num a => [a]
Perhaps you intended to use RankNTypes or Rank2Types
In the type declaration for `List2'

Поиск по источнику GHC показывает, что эта ошибка генерируется в TcValidity.hs. Точка входа, о которой мы говорим, checkValidType.

Мы можем проверить, что компилятор действительно входит туда путем компиляции с помощью -ddump-tc-trace; последний вывод отладки перед сообщением об ошибке:

Starting validity check [Type constructor `List2']
checkValidType Num a => [a] :: *

Продолжая в checkValidType, мы видим, что отсутствует RankNTypes, RHS синонима типа должен иметь ранг 0. (К сожалению, вывод debug не указывает здесь значение ctxt, но предположительно TySynCtxt.)

Примечание выше checkValidType определяет ранги в этом контексте, таким образом:

    basic ::= tyvar | T basic ... basic

    r2  ::= forall tvs. cxt => r2a
    r2a ::= r1 -> r2a | basic
    r1  ::= forall tvs. cxt => r0
    r0  ::= r0 -> r0 | basic

Этот квадрат комментариев с экспериментом Template Haskell, т.е. что тип ранга-0 не может включать =>, и любой тип, включающий =>, должен включать forall и, следовательно, быть ранга 1 или 2, даже если есть нет переменных типа в forall. В терминологии описанной в TcType, контексты отображаются только в сигма-типах.

Другими словами, как реализовано, typechecker отклоняет RHS List2, потому что он интерпретирует RHS как ранг 1 из-за его квалификации класса.

В ветке, которая ведет к нашему сообщению об ошибке, начинается здесь, Если я правильно понимаю, theta представляет контекст ограничения. Ядром первой строки блока do является forAllAllowed rank, который делает то, на что это похоже. Напомним, что RHS синонима типа ограничено рангом 0; поскольку forall не разрешен, мы получаем ошибку.

Это объясняет, почему RankNTypes переопределяет это ограничение. Если мы проследим, откуда приходит параметр rank, через rank0 в checkValidType, а затем через предыдущие несколько строк, мы обнаруживаем, что флаг RankNTypes в основном переопределяет ограничение rank0. (Контрастируйте ситуацию с объявлениями по умолчанию.) И поскольку дополнительный контекст рассматривался как ошибка ранга, RankNTypes разрешает его.