Рассмотрим код ниже:

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

Теперь, когда я вижу предполагаемый тип F в GHCI

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

Теперь, если я добавлю следующий код

g :: Int -> Float 
g = undefined 

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

Я получаю ошибку

Could not deduce (a ~ Float)

Я не могу понять, что здесь произошло? ОграничениеFoo Int a должен был ограничить типh вInt -> Float как показано в предполагаемом типеf.

Это потому, что объединение типов происходит перед разрешением экземпляров?

[Обновить]

Объяснение, данное Дэном Доэлом в списке рассылки кафе

The answer, I believe, is that the difference between the fundep implementation and type families is local constraint information. Fundeps do no local propagation.

So in your first definition, you've locally provided 'Int -> a', which is acceptable to GHC. Then it figures out externally to the function that '(Foo Int a) => Int -> a' is actually Int -> Float.

In the second definition, you're trying to give 'Int -> Float', but GHC only knows locally that you need to provide 'Int -> a' with a constraint 'Foo Int a' which it won't use to determine that a ~ Float.

This is not inherent to fundeps. One could make a version of fundeps that has the local constraint rules (easily so by translating to the new type families stuff). But, the difference is also the reason that overlapping instances are supported for fundeps and not type families. But I won't get into that right now.

Я до сих пор не понимаю, что это значит. Поэтому все еще ищем более понятный ответ.