При написании кода с помощью UndecidableInstances раньше я столкнулся с чем-то, что я нашел очень странным. Мне удалось непреднамеренно создать некоторый код, который typechecks, когда я полагал, что это не должно:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
data Foo = Foo
class ConvertFoo a b where
convertFoo :: a -> b
instance (ConvertFoo a Foo, ConvertFoo Foo b) => ConvertFoo a b where
convertFoo = convertFoo . (convertFoo :: a -> Foo)
evil :: Int -> String
evil = convertFoo
В частности, функция convertFoo typechecks при задании любого ввода для получения любого выхода, что продемонстрировано функцией evil. Сначала я подумал, что, возможно, мне удалось случайно реализовать unsafeCoerce, но это не совсем так: на самом деле попытка вызвать мою функцию convertFoo (например, делая что-то вроде evil 3) просто переходит в бесконечный цикл.
Я понимаю, что происходит в смутном смысле. Мое понимание проблемы заключается в следующем:
- Экземпляр
convertFoo, который я определил, работает на любом входе и выходе,aиb, ограниченном только двумя дополнительными ограничениями, что функции преобразования должны существовать отa -> FooиFoo -> b. - Как бы то ни было, это определение может соответствовать любым типам ввода и вывода, поэтому кажется, что вызов
convertFoo :: a -> Fooсам выбирает само определениеconvertFoo, так как его единственный доступный в любом случае. - Так как
convertFooвызывает себя бесконечно, функция переходит в бесконечный цикл, который никогда не заканчивается. - Так как
convertFooникогда не заканчивается, тип этого определения нижний, поэтому технически ни один из типов не нарушается, а тип typechecks.
Теперь, даже если вышеуказанное понимание верное, я все еще запутался в том, почему вся программа имеет тип. В частности, я ожидал бы, что ограничения ConvertFoo a Foo и ConvertFoo Foo b будут терпеть неудачу, учитывая, что таких экземпляров не существует.
Я понимаю (по крайней мере, пушисто), что ограничения не имеют значения при выборе экземпляра - экземпляр выбирается на основе только главы экземпляра, тогда ограничения проверяются, поэтому я вижу, что эти ограничения могут быть решены просто из-за моего ConvertFoo a b экземпляр, который примерно такой же разрешительный, как может быть. Тем не менее, для этого потребуется, чтобы один и тот же набор ограничений был разрешен, что, по-моему, поставит typechecker в бесконечный цикл, заставляя GHC либо зависать при компиляции, либо давать мне ошибку (последняя из которых я видел раньше).
Ясно, однако, что typechecker не работает, потому что он с радостью оканчивается и с радостью компилирует мой код. Зачем? Как контекст экземпляра удовлетворен в этом конкретном примере? Почему это не дает мне ошибку типа или создает цикл проверки типов?
