GitLab

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.