Al escribir un código usandoUndecidableInstances antes, me encontré con algo que me pareció muy extraño. Me las arreglé para crear involuntariamente un código que comprueba cuando creía que no debería:

{-# 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

Específicamente, elconvertFoo verifica el tipo de función cuando se daalguna entrada para produciralguna salida, como lo demuestra elevil función. Al principio, pensé que tal vez logré implementar accidentalmenteunsafeCoerce, pero eso no es del todo cierto: en realidad intento llamar a miconvertFoo función (haciendo algo comoevil 3, por ejemplo) simplemente entra en un bucle infinito.

I algo así como entender lo que está sucediendo en un sentido vago. Mi comprensión del problema es algo como esto:

La instancia deConvertFoo que he definido funciona enalguna entrada y salida,a yb, solo limitado por las dos restricciones adicionales de las que deben existir funciones de conversióna -> Foo yFoo -> b.De alguna manera, esa definición puede coincidir con cualquier tipo de entrada y salida, por lo que parece que la llamada aconvertFoo :: a -> Foo está eligiendo la definición misma deconvertFoo en sí, ya que es el único disponible, de todos modos.Ya queconvertFoo se llama infinitamente, la función entra en un bucle infinito que nunca termina.Ya queconvertFoo nunca termina, el tipo de esa definición es inferior, así quetécnicamente ninguno de los tipos se viola nunca, y el programa mecanografía.

Ahora, incluso si la comprensión anterior es correcta, todavía estoy confundido acerca de por qué todo el programa mecanografía. Específicamente, esperaría queConvertFoo a Foo yConvertFoo Foo b restricciones para fallar, dado que no existen tales instancias.

I hacer entiendo (al menos de forma difusa) que las restricciones no importan al elegir una instancia: la instancia se elige únicamente en función del encabezado de la instancia, luego se comprueban las restricciones, por lo que pude ver que esas restricciones podrían resolverse bien debido a miConvertFoo a b ejemplo, que es lo más permisivo posible. Sin embargo, eso requeriría que se resolviera el mismo conjunto de restricciones, lo que creo que pondría el typechecker en un bucle infinito, causando que GHC se bloquee en la compilación o me dé un error de desbordamiento de pila (el último de los cuales he visto antes de).

Claramente, sin embargo, el typechecker haceno bucle, porque felizmente toca fondo y compila mi código felizmente. ¿Por qué? ¿Cómo se satisface el contexto de la instancia en este ejemplo en particular? ¿Por qué esto no me da un error de tipo o produce un bucle de verificación de tipo?