Почему этот код с использованием UndecidableInstances компилируется, а затем генерирует бесконечный цикл времени выполнения?
При написании кода с использованиемUndecidableInstances
раньше я столкнулся с чем-то очень странным. Мне удалось непреднамеренно создать некоторый код, который проверяет типы, когда я полагал, что это не должно:
{-# 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
проверки типов функций, когда данолюбой вход для производствалюбой выход, как продемонстрированоevil
функция. Сначала я подумал, что, возможно, мне удалось случайно осуществитьunsafeCoerce
, но это не совсем так: на самом деле пытается позвонитьconvertFoo
функция (делая что-то вродеevil 3
например) просто заходит в бесконечный цикл.
I вроде, как бы, что-то вроде понять, что происходит в смутном смысле. Мое понимание проблемы примерно так:
ПримерConvertFoo
что я определил работы налюбой ввод и вывод,a
а такжеb
ограничивается только двумя дополнительными ограничениями, из которых должны существовать функции преобразованияa -> Foo
а такжеFoo -> b
.Каким-то образом это определение может соответствовать любым типам ввода и вывода, поэтому может показаться, что вызовconvertFoo :: a -> Foo
выбирает само определениеconvertFoo
само по себе, так как это единственный доступный, в любом случае.посколькуconvertFoo
вызывает себя бесконечно, функция входит в бесконечный цикл, который никогда не заканчивается.посколькуconvertFoo
никогда не завершается, тип этого определения снизу, поэтомутехнически ни один из типов никогда не нарушается, а тип программы проверяется.Теперь, даже если вышеприведенное понимание верно, я все еще не понимаю, почему все типы программ проверяются. В частности, я бы ожидалConvertFoo a Foo
а такжеConvertFoo Foo b
ограничения на неудачу, учитывая, что таких экземпляров не существует.
I делать понимать (по крайней мере, нечетко), что ограничения не имеют значения при выборе экземпляра - экземпляр выбирается только на основе заголовка экземпляра, затем проверяются ограничения - так что я мог видеть, что эти ограничения могут разрешиться очень хорошо из-за моегоConvertFoo a b
экземпляр, который примерно настолько разрешительный, насколько это возможно. Однако для этого потребуется разрешить тот же набор ограничений, который, я думаю, поместит проверку типов в бесконечный цикл, в результате чего GHC либо зависнет при компиляции, либо выдаст ошибку переполнения стека (последнее из которых я видел до).
Понятно, что типограф проверяетне цикл, потому что он счастливо доводит до конца и счастливо компилирует мой код. Зачем? Как контекст экземпляра удовлетворяется в этом конкретном примере? Почему это не вызывает ошибку типа и не создает цикл проверки типов?