[Haskell-cafe] Fwd: How Type inference work in presence of Functional Dependencies

[Dan Doel]

Copying the mailing list, because I forgot.

On Thu, Sep 13, 2012 at 5:18 AM, satvik chauhan <mystic.satvik at gmail.com> wrote:
> Consider the code below :
>
> {-# LANGUAGE
> MultiParamTypeClasses,FlexibleInstances,FunctionalDependencies,UndecidableInstances,FlexibleContexts
> #-}
> class Foo a c | a -> c
> instance Foo Int Float
> f :: (Foo Int a) => Int -> a
> f = undefined
>
> Now when I see the inferred type of f in ghci
>
>> :t f
>
>> f :: Int -> Float
>
> Now If I add the following code
>
> g :: Int -> Float
> g = undefined
>
> h :: (Foo Int a) => Int -> a
> h = g
>
>
> I get the error
>
> Could not deduce (a ~ Float)
>
>
> I am not able to understand what has happened here ? The restriction "Foo
> Int a" should have restricted the type of h to "Int -> Float" as shown in
> the inferred type of 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.

-- Dan