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?

I think this is type family non-injectivity: in `test`, GHC wants `Bar (f a) ~ Bar f`, where `a` is the argument to `test`. It has `forall b. Bar (f b) ~ Bar f`. It needs to instantiate that equality to get a concrete one, so I think it tries to find the instantiation by creating a unification variable `_b`, instantiating `b := _b`, and then unifying the resulting `Bar (f _b)` with `Bar (f a)` to solve for `_b`. However, it fails to reduce `Bar (f _b) ~ Bar (f a)` to `f _b ~ f a` and then `_b ~ a` because the first step requires `Bar` to be injective. No idea how to solve it "automatically". — HTNW, Jul 15 '20 at 12:54
That's odd. I can't even load the class definition for `Foo'`, let alone `test` itself (it tells me "Illegal type synonym family application ‘Bar f’ in instance: Bar f ~ Bar (f a)"). What version of GHC are you using? I tried 8.8 and 8.10 and they both give the same error. — Daniel Wagner, Jul 15 '20 at 14:41
@DanielWagner I was using version 8.6. That is weird. I got the same behaviour in newer versions of ghc by adding a wrapper `newtype Wrap f = Wrap (Bar f)` and using it in the class defnition. If I also use it in `test`, the error changes to `cannot construct the infinite type: f ~ f a`. — Greg C, Jul 15 '20 at 15:08

Li-yao Xia · Accepted Answer · 2020-07-15T17:23:48.963

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)

Quantified type equality of associated type families

1 Answers1