Functional dependencies (for classes or type familes alike) can not refine given equality constraints
Motivation
Consider these two versions of foo
:
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators #-}
import Data.Type.Equality
type family Foo a = r | r -> a
fooTF :: (Foo a ~ Foo a') => a :~: a'
fooTF = Refl
class FooC a r | r -> a
fooC :: (FooC a r, FooC a' r) => a :~: a'
fooC = Refl
However, both fail to type check (as of 8.1):
loop.hs:11:9: error:
• Could not deduce: a ~ a'
from the context: Foo a ~ Foo a'
bound by the type signature for:
fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
at loop.hs:10:1-37
‘a’ is a rigid type variable bound by
the type signature for:
fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
at loop.hs:10:1-37
‘a'’ is a rigid type variable bound by
the type signature for:
fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
at loop.hs:10:1-37
Expected type: a :~: a'
Actual type: a :~: a
• In the expression: Refl
In an equation for ‘fooTF’: fooTF = Refl
• Relevant bindings include
fooTF :: a :~: a' (bound at loop.hs:11:1)
|
11 | fooTF = Refl
| ^^^^
loop.hs:16:8: error:
• Couldn't match type ‘a’ with ‘a'’
‘a’ is a rigid type variable bound by
the type signature for:
fooC :: forall a r a'. (FooC a r, FooC a' r) => a :~: a'
at loop.hs:15:1-41
‘a'’ is a rigid type variable bound by
the type signature for:
fooC :: forall a r a'. (FooC a r, FooC a' r) => a :~: a'
at loop.hs:15:1-41
Expected type: a :~: a'
Actual type: a :~: a
• In the expression: Refl
In an equation for ‘fooC’: fooC = Refl
• Relevant bindings include
fooC :: a :~: a' (bound at loop.hs:16:1)
|
16 | fooC = Refl
| ^^^^
I would have thought that trying to decompose qualities like this is the very essence of what functional dependencies are for, so I am quite confused.
Proposal
Make this work. I'm not sure exactly what this entails, because I don't currently understand the difference between what functional dependencies do do and this.
I will note, however, that doing so perhaps makes existing issues with functional dependencies like #10675 worse because we could get unsound equality evidence to do unsafe coercions with.