replicate from the singletons paper doesn't typecheck - issue with induction with SingI

[miguel-negrao]

Hi,

I can't seem to replicate the replicate :-) function from the singletons paper (page 5).

$(singletons [d|
    data Nat = Zero | Succ Nat 
    |])

type Vec :: Nat -> Type -> Type
data Vec (n :: Nat) a where
    Nil :: Vec Zero a
    (:>) :: a -> Vec n a -> Vec (Succ n) a

replicate :: forall n a . (SingI n) => a -> Vec n a
replicate a = case (sing :: Sing n) of
                SZero -> Nil
                SSucc _ -> a :> replicate a

I get the error:

• Could not deduce (SingI n1) arising from a use of ‘replicate’
  from the context: SingI n
    bound by the type signature for:
               replicate'' :: forall (n :: Nat) a. SingI n => a -> Vec n a
    at ...
  or from: n ~ 'Succ n1
    bound by a pattern with constructor:
               SSucc :: forall (n :: Nat). Sing n -> SNat ('Succ n),
             in a case alternative
    at ...
• In the second argument of ‘(:>)’, namely ‘replicate a’
  In the expression: a :> replicate a
  In a case alternative: SSucc _ -> a :> replicate a

In general I can't seem to do induction with SingI n where n is a Nat. I've been going around this to define all the functions as receiving SNat and then doing some versions with SingI n which just call the SNat versions, but the papers claims that I could define a function like replicate using implicit Nat directly.

Any help with this is appreciated !

ghci> :show packages
active package flags:
  -package-id singletons-th-3.0-77a811e0625d4be29862a8a50e4fe678624221aad3c5f672d06dd459b5f7f298
  -package-id singletons-base-3.0-1eb26d4e4f464d3bee0e7479232ec2e664eb67670023dda0f2bc7c568e731720
  -package-id singletons-3.0.2-01b5eec50446fa7eadc2a5cc3e38303305b4824f6f93151564f2cfa2d15e8edc
  -package-id base-4.15.1.0

ghc --version
The Glorious Glasgow Haskell Compilation System, version 9.2.7

[int-index]

The paper assumes that the SingI constraint would be carried by the generated SSucc constructor. To achieve a better runtime representation, the library doesn't actually do that and you need to use withSingI to satisfy the constraint:

 replicate :: forall n a . (SingI n) => a -> Vec n a
 replicate a = case (sing :: Sing n) of
                 SZero -> Nil
-                SSucc _ ->               a :> replicate a
+                SSucc m -> withSingI m $ a :> replicate a

[int-index]

Another option is to use the Sing pattern synonym

 replicate :: forall n a . (SingI n) => a -> Vec n a
 replicate a = case (sing :: Sing n) of
                 SZero -> Nil
-                SSucc _    -> a :> replicate a
+                SSucc Sing -> a :> replicate a

The effect is the same, matching on Sing satisfies the SingI constraint.

[RyanGlScott]

@int-index's analysis is spot-on. As for why the modern singletons library no longer adds SingI constraints to singled data constructors, see this comment.

I'll opt to close this issue, but feel free to re-open it if there is something else amiss.

[miguel-negrao]

Thank you all for the clarifications ! I can now solve the issue with withSingI.

Another option is to use the Sing pattern synonym

 replicate :: forall n a . (SingI n) => a -> Vec n a
 replicate a = case (sing :: Sing n) of
                 SZero -> Nil
-                SSucc _    -> a :> replicate a
+                SSucc Sing -> a :> replicate a

The effect is the same, matching on Sing satisfies the SingI constraint.

When I try this I get the following warning. Is that expected ?

Pattern match(es) are non-exhaustive
In a case alternative:
    Patterns not matched:
        SSucc SZero
        SSucc (SSucc _)

[RyanGlScott]

What GHC/singletons versions are you using? I do not see any warnings when using GHC 9.8.1/singletons-3.0.2.

[int-index]

@RyanGlScott GHC 9.2.7 and singletons-3.0.2 according to the issue description

[miguel-negrao]

Sorry, my mistake, actually I was using ghc 9.0.2. Updating to 9.4.7 (current recommended in ghcup) solves the issue.

[RyanGlScott]

Thanks for confirming! My guess is that you ran into an old GHC bug that made its pattern-match coverage checking results unreliable in the presence of GADTs + pattern synonyms. Happily, newer GHCs appear to handle this much better.