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, Sep 14 '17 at 20:22
Right, I should go to bed. Want to turn this into an answer I can accept? — Sebastian Graf, Sep 14 '17 at 20:23
Sorry, @chi beat you to it (and probably began writing that answer before you commented). Thanks! — Sebastian Graf, Sep 14 '17 at 20:25
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, Sep 14 '17 at 20:27

score 4 · Accepted Answer · edited Sep 16 '17 at 10:27

4

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.

edited Sep 16 '17 at 10:27

Benjamin Hodgson

42,952
15
108
157

answered Sep 14 '17 at 20:23

chi

111,837
3
133
218

Well, that is for `ReplaceRet`. What about `Const`? – Sebastian Graf Sep 14 '17 at 20:27
2

@SebastianGraf That's a good point. The issue is that you need to reason inductively on the structure of types to deduce that `Const a r` is OK. GHC doesn't go that far. BTW, I remember that in the paper on injectivity annotations the authors show tricky cases that look injective, but are not -- so they had to design GHC to be quite restrictive on what it accepts :-( It could be improved, of course... – chi Sep 14 '17 at 20:31
Thanks, edit your answer to include that and I'll accept (again) :) – Sebastian Graf Sep 14 '17 at 20:32

Type families and injectivity in a subset of indexes

1 Answers1