Fwd: How Type inference work in presence of Functional Dependencies

Copying the mailing list, because I forgot.
On Thu, Sep 13, 2012 at 5:18 AM, satvik chauhan
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
participants (1)
-
Dan Doel