Quantified type equality of associated type families

Question

I have an associated type family Bar in a type class Foo. Foo' requires that Bar f ~ Bar (f a) for all a, but in another function test I get an error Couldn't match type 'Bar f' with 'Bar (f a)', even though it depends on Foo' f. The code:

{-# LANGUAGE TypeFamilies, PolyKinds, QuantifiedConstraints #-}

import Data.Proxy

class Foo f where
  type Bar f

class (Foo f, forall a. Foo (f a), forall a. Bar f ~ Bar (f a)) => Foo' f where

test :: Foo' f => Proxy (f a) -> Bar (f a) -> Bar f
test _ = id

Why can't GHC figure out this type equality and is there a way to help the typechecker without asserting the concrete equality in test?

Answer 1

Type families and quantified constraints don't mix. Much even less with type equalities. But there is a way to keep them separate to achieve more or less the same result.

A quantified constraint is actually restricted in the ways it can be used. It's not sufficient to know that a constraint holds for all types, you also need a way to know which types you need to specialize it to. GHC achieves this by representing quantified constraints as a sort of "local instance" subject to the common rules of instance resolution. I'm not sure quantified type equalities even mean anything. In summary, it's not enough that a quantified constraint can be instantiated to do what we want; that instantiation must happen in the regular course of instance resolution, and that puts restrictions on the allowed forms of quantified constraints.

The trick is to define a class synonym for the body of the quantified constraint:

class    (Bar f ~ Bar (f a)) => EBar f a
instance (Bar f ~ Bar (f a)) => EBar f a

That way we can rewrite the quantified constraint as forall x. EBar f x, no type families in sight:

class (Foo f, forall a. Foo (f a), forall x. EBar f x) => Foo' f where

To use this class, we need an explicit function to specialize the quantified constraint (the problem is that if we use an equality Bar f ~ Bar (f a) directly, the type checker can't relate that to the quantified constraint forall x. EBar f x, which looks nothing like it):

-- Morally a function on constraints `(forall x. EBar f x) => EBar f a`
-- in continuation-passing style: (x => y) is isomorphic to forall r. (y => r) -> (x => r)
ebar :: forall f a r. (EBar f a => Proxy (f a) -> r) -> (forall x. EBar f x) => Proxy (f a) -> r
ebar f = f

test :: Foo' f => Proxy (f a) -> Bar (f a) -> Bar f
test = ebar (\_ -> id)

---

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FlexibleInstances, TypeFamilies, PolyKinds, QuantifiedConstraints #-}

import Data.Proxy

class Foo f where
  type Bar f

class (Foo f, forall a. Foo (f a), forall a. EBar f a) => Foo' f where

class    (Bar f ~ Bar (f a)) => EBar f a
instance (Bar f ~ Bar (f a)) => EBar f a

ebar :: forall f a r. (EBar f a => Proxy (f a) -> r) -> (forall x. EBar f x) => Proxy (f a) -> r
ebar f = f

test :: Foo' f => Proxy (f a) -> Bar (f a) -> Bar f
test = ebar (\_ -> id)