Considere el siguiente código:

{-# LANGUAGE MultiParamTypeClasses,FlexibleInstances,FunctionalDependencies,UndecidableInstances,FlexibleContexts  #-}
class Foo a c | a -> c
instance Foo Int Float 
f :: (Foo Int a) => Int -> a 
f = undefined

Ahora cuando veo el tipo inferido de f en ghci

> :t f
> f :: Int -> Float

Ahora si agrego el siguiente código

g :: Int -> Float 
g = undefined 

h :: (Foo Int a) => Int -> a 
h = g

Me sale el error

Could not deduce (a ~ Float)

¿No puedo entender lo que ha pasado aquí? La restricciónFoo Int a debería haber restringido el tipo deh aInt -> Float como se muestra en el tipo inferido def.

¿Es porque la unificación de tipos está ocurriendo antes de resolver las instancias?

[Actualizar]

Una explicación dada por Dan Doel en la lista de correo del café.

La respuesta, creo, es que la diferencia entre la implementación de fundep y las familias de tipos es la información de restricciones locales. Los fundeps no hacen propagación local.

Así que en su primera definición, ha proporcionado localmente 'Int -> a', que es aceptable para GHC. Entonces se da cuenta externamente de la función que '(Foo Int a) => Int -> a' es en realidadInt -> Float.

En la segunda definición, estás tratando de dar 'Int -> Float', pero GHC solo sabe localmente que debe proporcionar'Int -> a'con una restricción'Foo Int a' que seno lo hará utilizar para determinar quea ~ Float.

Esto no es inherente a fundeps. Uno podría hacer una versión de fundeps que tenga las reglas de restricción local (fácilmente al traducir las cosas del nuevo tipo de familias). Pero, la diferencia es también la razón por la que las instancias superpuestas son compatibles con fundeps y no con familias de tipos. Pero no voy a entrar en eso ahora.

Todavía no entiendo lo que eso significa. Así que sigue buscando una respuesta mejor comprensible.