Type families and injectivity in a subset of indexes

Question

I have the following type family:

{-# LANGUAGE TypeFamilyDependencies #-}

type family Const arr r = ret | ret -> r where
  Const (_ -> a) r = Const a r
  Const _  r = r

This is just the Const function in disguise, but the injectivity checker of GHC 8.2.1 doesn't recognise it as injective wrt. to its second argument:

    * Type family equation violates injectivity annotation.
      RHS of injective type family equation cannot be a type family:
        Const (_ -> a) r = Const a r
    * In the equations for closed type family `Const'
      In the type family declaration for `Const'
  |
4 |       Const (_ -> a) r = Const a r
  |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

If you leave out the first case, it works, which leads me to believe that the functionality is there, but is not really mature yet.

Can I formulate this some other way so that GHC recognises injectivity? It's actually for this marginally more complicated case (so arr is really used):

{-# LANGUAGE TypeFamilyDependencies #-}

type family ReplaceRet arr r = ret | ret -> r where
  ReplaceRet (a -> b) r = a -> ReplaceRet b r
  ReplaceRet _  r = r

Answer 1

You propose

type family ReplaceRet arr r = ret | ret -> r where
  ReplaceRet (a -> b) r = a -> ReplaceRet b r
  ReplaceRet _  r = r

but

ReplaceRet (Int -> Bool) Char = Int -> Char
ReplaceRet Bool (Int -> Char) = Int -> Char

So, it is not true that given ret, we can deduce r. We can't have the ret -> r dependency.

We could have arr ret -> r instead, but GHC does not (yet?) support this kind of dependencies on type families, as far as I know.

Const a b looks as if it respects ret -> b. Detecting that however requires an inductive proof, and GHC is not that smart to deduce that. Deciding injectivity is actually quite tricky: see the awkward cases in the paper, in Sect 4.1 for a few surprises. To overcome these issues, GHC had to be designed to be conservative in what it accepts.