Is there any way to convince GHC that this (injective) type family is injective?

Question

Messing around with GHC's DataKinds, I tried implementing type-level binary nats. They're simple enough to implement, but if I want them to be useful in common cases, then GHC needs to believe that the Succ type family is injective (so that type inference will work at least as well as it does for unary type-level nats). However, I'm having a difficult time convincing GHC that this is the case. Consider the following encoding of binary nats:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
module Nat2 where

data Nat = Zero | Pos Nat1
data Nat1 = One | Bit0 Nat1 | Bit1 Nat1
  -- by separating Nat and Nat1 we avoid dealing w/ Bit0^n Zero as a spurrious representation of 0

type Succ :: Nat -> r
type family Succ n :: r | r -> n where
  Succ 'Zero = 'Pos 'One
  Succ ('Pos x) = 'Pos (Succ1 x)
  
type Succ1 :: Nat1 -> r
type family Succ1 n :: r | r -> n where
  Succ1 'One = 'Bit0 'One
  Succ1 ('Bit0 x) = 'Bit1 x
  Succ1 ('Bit1 x) = 'Bit0 (Succ1 x)

GHC can't accept this, because it can't tell that Succ1 is injective:

Nat2.hs:15:3: error: [GHC-05175]
    • Type family equation right-hand sides overlap; this violates
      the family's injectivity annotation:
        Succ Zero = Pos One -- Defined at Nat2.hs:15:3
        Succ (Pos x) = Pos (Succ1 x) -- Defined at Nat2.hs:16:3
    • In the equations for closed type family ‘Succ’
      In the type family declaration for ‘Succ’
   |
15 |   Succ 'Zero = 'Pos 'One
   |   ^^^^^^^^^^^^^^^^^^^^^^

Nat2.hs:20:3: error: [GHC-05175]
    • Type family equation right-hand sides overlap; this violates
      the family's injectivity annotation:
        Succ1 One = Bit0 One -- Defined at Nat2.hs:20:3
        Succ1 (Bit1 x) = Bit0 (Succ1 x) -- Defined at Nat2.hs:22:3
    • In the equations for closed type family ‘Succ1’
      In the type family declaration for ‘Succ1’
   |
20 |   Succ1 'One = 'Bit0 'One
   |   ^^^^^^^^^^^^^^^^^^^^^^^

We think it's injective because, by inspection of Succ1, One is never in its image, so the Bit0 (Succ1 x) case never returns Bit0 One, and thus the Bit1 case will never conflict with the One case. The same argument ("One is not in the image of Succ1") shows that Succ itself is also injective. However, GHC is not quite clever enough to find this argument.

So, question: in this case (and cases like these), is there any way to convince GHC that an injective type family is in fact injective? (Perhaps a typechecker plugin where I can provide a function that inverts Succ1? Perhaps a pragma that says "try inferring backwards from this family as if it were injective; if you hit any ambiguities you're allowed to crash"?)

Handler

Doesn't your ghc complain also about Succ being non-injective? Mine does (8.2.2) – Dobson

Yep, good catch. Edited the OP. Note that the proof that Succ is injective uses the same key argument as the proof that Succ1 is injective (namely, "One is not in the image of Succ1"), so I'm hoping that any method that can convince GHC that Succ1 is injective also works to convince it about Succ. – Handler

I'm curious: what happens if you switch to a more regular zeroless representation, like data Bit = One | Two; type Nat = [Bit], or perhaps data Nat = Zero | Bit1 Nat | Bit2 Nat? If you can't make those work, your chances of making something fancier work seem pretty slim. – Bernettabernette

The trouble with data Nat = Zero | Bit1 Nat | Bit2 Nat is that in that case, the function Succ isn't injective: Succ Zero and Succ (Bit0 Zero) both map to Bit1 Zero. The hope is that, given a representation of binary nats where Succ is injective, GHC can be made to believe this (or at least take it on my word). – Handler

@So8res, there is no Bit0 in the representation I mentioned--it's 1-2 rather than 0-1. – Bernettabernette

Well, what I was attempting doesn't seem to work anyway. Oh well. – Bernettabernette

@Bernettabernette oh, neat. But yeah, that still requires convincing GHC somehow to accept an argument of the form "I should be allowed to recurse here because the only potentially ambiguous output does not appear in the image of the function" – Handler

I've messed around a bit with an encoding of numbers as a non-empty sequence of streaks of 0- and 1-bits, where each streak length is encoded as a Peano-style positive number. You need an indication of the number being even or odd. There's an implicit MSB of 1 after the sequence. 0 is encoded separately as in your scheme. It is very difficult to work with this encoding so I didn't finish it, but it looks like increment could be injective in it (it involves at most 3 streaks so all cases may be listed explicitly). – Dobson

Answer 1

You can use GADTs to add a phantom type parameter to Nat1, so that One has a different type than Bit0 and Bit1, but one that's still compatible everywhere you need it to be, like this:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
module Nat2 where

data Nat where
  Zero :: Nat
  Pos :: Nat1 a -> Nat
data Nat1 a where
  One :: Nat1 'False
  Bit0 :: Nat1 a -> Nat1 'True
  Bit1 :: Nat1 a -> Nat1 'True
  -- by separating Nat and Nat1 we avoid dealing w/ Bit0^n Zero as a spurrious representation of 0

type Succ :: Nat -> r
type family Succ n :: r | r -> n where
  Succ 'Zero = 'Pos 'One
  Succ ('Pos x) = 'Pos (Succ1 x :: Nat1 'True)

type Succ1 :: Nat1 a -> r
type family Succ1 n :: r | r -> n where
  Succ1 'One = 'Bit0 'One
  Succ1 ('Bit0 x) = 'Bit1 x
  Succ1 ('Bit1 x) = 'Bit0 (Succ1 x :: Nat1 'True)

I also got it to work by creating another type entirely:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
module Nat2 where

data Nat = Zero | Pos Nat1
data Nat1 = One | SomeBit NatBit
data NatBit = Bit0 Nat1 | Bit1 Nat1
  -- by separating Nat and Nat1 we avoid dealing w/ Bit0^n Zero as a spurrious representation of 0

type Succ :: Nat -> r
type family Succ n :: r | r -> n where
  Succ 'Zero = 'Pos 'One
  Succ ('Pos x) = 'Pos ('SomeBit (Succ1 x))

type Succ1 :: Nat1 -> r
type family Succ1 n :: r | r -> n where
  Succ1 'One = 'Bit0 'One
  Succ1 ('SomeBit ('Bit0 x)) = 'Bit1 x
  Succ1 ('SomeBit ('Bit1 x)) = 'Bit0 ('SomeBit (Succ1 x))

Passive