Could not deduce SingI of predecessor Nat

Question

I am trying to write a weaken function for finite sets of integers. I am using the singletons package. I have defined and promoted addition, subtraction and predecessor functions, as well as proved some equations on them to help the type-checker. But the error I am getting is quite unrelated to all that.

weaken :: forall n m k . (SingI n, SingI m, SingI k, (Minus m n) ~ NatJust k) => Fin n -> Fin m
weaken ZF =  gcastWith (apply Refl $ plus_minus sm sn sk) ZF
  where sn = sing :: SNat n
        sm = sing :: SNat m
        sk = sing :: SNat k
weaken (SF n) = gcastWith (apply Refl $ succ_pred sm) (SF (weaken n))
  where sn = sing :: SNat n
        sm = sing :: SNat m
        sk = sing :: SNat k

The error I am getting is on the recursive call of weaken (SF (weaken n)) and is the following: Could not deduce (SingI n1), where n1 is correctly inferred to be the type-level predecessor of type n. I could add a SingI (Pred n) constraint but this simply moves the problem one level down (GHC now says it can't deduce the equivalent of (SingI (Pred (Pred n)))).

How can I convince GHC that SingI (Pred n) follows from SingI n (and why doesn't the singletons package already do this)?

Answer 1

GHC.TypeLits, which ultimately provides us type-level non-negative Integer-s, exports no functions that would let us do singleton runtime operations. For example, given KnownNat a and KnownNat b, there is no standard function to produce KnownNat (a + b) at runtime.

singletons solves this by implementing the singleton Nat operations unsafely.

singletons subtraction function throws an error for negative results (and doesn't truncate to 0 as we'd wish), so we can't reuse that for pred and have to implement it ourselves:

{-# language TypeApplications #-} -- plus all the usual exts

import Data.Singletons.Prelude
import Data.Singletons.TypeLits
import Unsafe.Coerce

type family Pred (n :: Nat) :: Nat where
  Pred 0 = 0
  Pred n = n :- 1

sPred :: Sing n -> Sing (Pred n)
sPred sn = case fromSing sn of
  0 -> unsafeCoerce (sing @_ @0)
  n -> case toSing @Nat (n - 1) of
    SomeSing sn -> unsafeCoerce sn

You can use sPred to get Sing (Pred n), then withSingI or singInstance to convert that into SingI (Pred n).

However, you probably shouldn't use SingI in weaken. The purpose of SingI is to plug around singleton parameters automatically in contexts where you don't use them for anything besides forwarding them to other functions. Instead just use Sing, and you can avoid sing and type annotation noise. In my experience Sing is preferable to SingI in about 90% of the time for singletons programming.