NEW BOT Телеграм, страница

#ghc
Наверное самый мой крупный контрибьюшен на текущий момент времени. Полностью переписал разрешение имён для типовых паттернов и частично - проверку типов для них же. Вкрации:

f (Proxy @a) = ... -- @a ето типовой паттерн.

Такой синтаксис есть, ему уже 3 года, но "работает" он только в позиции аргумента у тайп конструктора. Вероятно дальше мне придётся реализовывать его и для обычных паттернов, но это уже совсем другая история. В чём была проблема? 3 года назад эти паттерны были сделаны под идейным руководством Джона Эриксона, а потому до моего патча было запрещено... ну примерно всё запрещено:

f1 :: forall a . Proxy a -> ...
f1 (Proxy @a) = ... -- неа, @a уже в скоупе

f2 (Proxy @a) = \(Proxy @a) -> ... -- неа

f3 (Proxy @(b :: (a, a))) = ... -- неа

f4 (Proxy @a) (Proxy @(b :: a)) = ... -- опять неа

f5 (Proxy @($(TH.varT (TH.mkName "t")))) = ... -- лол)))

И самое интересное - сделано это было на коленке, отдельными валидациями с нехитрыми эвристиками, когда звонить в колокол. В итоге мне пришлось полностью переписывать код, ответственный за это дело и изобретать инфраструктуру, правильным образом собирающую переменные с паттернов. Зато теперь
- TH сплайсы работают
- Нормальный скоупинг тайп/каинд сигнатур работает
- Шедоувинг типовых переменных работает, варнинги о шедоувинге тоже работают
- Линты о конфликтующих определениях работают
А всего-то и надо было - сделать по-человечески, как уже было сделано до этого на уровне термов. Это была моя прямая задача, но я на этом не остановился и дальше, за счёт заведения, пошёл править проверку типов у типовых паттернов. Проверка типов (те самые три года назад) была успешно реализована путём того, что типовые паттерны проверялись точно таким же образом, как и сигнатуры паттернов. Это до какого-то момента работало, а потом всё разваливалось. Представим такой код:

data T where
  MkT :: forall (f :: forall k. k -> Type).
    f Int -> f Maybe -> T

k :: T -> ()
k (MkT @f (x :: f Int) (y :: f Maybe)) = ()

Чё тут происходит: у нас f с полиморфным каиндом forall k. k -> Type. В первом использовании f Int типовая переменная k инстанцируется в каинд от Int, то есть Type и полная сигнатура f в этом использовании становится Type -> Type. Дальше мы находим второе использование f, а именно - f Maybe. Тут у нас при имеющихся вводных по всем правилам типизации в Хаскеле с нуля начинается инстанцирование уже другой переменной k в каинд от Maybe - Type -> Type. То есть во втором использовании каинд f должен быть (Type -> Type) -> Type.

Это то, как типизация должна работать. Но для этого нам надо чтобы у f был полиморфный каинд, т.е. имеющий forall k. - но так нельзя сделать, если мы относимся к f как к сигнатуре паттерна. Поэтому до моего патча этой самой f назначался каинд k -> Type, т.е. из какой-то k в Type. Дальше была проверка первого использования, где k сравнивалась с каиндом у Int - Type и GHC видел что ранее у k нет никаких ограничений лихо проводил равенство между k и Type. Второе использование уже пыталось сопоставить каинд Maybe - Type -> Type с k, имея в контексте информацию, что k равен Type. Type -> Type не равен Type, код идёт нахер, завершаем проверку типов.

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

https://gitlab.haskell.org/ghc/ghc/-/merge_requests/10725

GitLab

!10725: Draft: Type patterns (#22478, #18986) · Merge requests · Glasgow Haskell Compiler / GHC · GitLab

Improved name resolution and type checking of type patterns in constructors: HsTyPat: a new dedicated data type that represents type patterns in...

12 views22:36