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

Isn't the problem that ReplaceRet (Int -> Int) Int and ReplaceRet Int (Int -> Int) both resolve to the type Int -> Int, so the type isn't injective in the second argument? — K. A. Buhr
Right, I should go to bed. Want to turn this into an answer I can accept? — Sebastian Graf
Sorry, @chi beat you to it (and probably began writing that answer before you commented). Thanks! — Sebastian Graf
IMO, injectivity annotations are very weak in GHC right now. Even if F is declared injective, GHC will still not deduce a ~ b from F a ~ F b. Injectivity seems to only prevent some ambiguous types, as exemplified in the docs. I'd rather turn on AmbiguousTypes and deal with ambiguities using explicit type arguments. — chi

chi chi · Accepted Answer · 2017-09-14T20:23:54

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.

Type families and injectivity in a subset of indexes

1 Answers