The linked typechecker plugin should help solve those trivial constraints, like KnownNat (n + 1), given KnownNat n. But a plugin is not a necessity.
The constraints library comes packed with many useful “proofs” about Nat arithmetic in the Data.Constraint.Nat module.
constraints defines its own concepts of Dicts (a constraint captured as a value) and :- (an “entailment” or implication; a :- b means that the constraint a “entails” the constraint b).
Those concepts may seem a bit abstract in the beginning. But let’s look at how we can use the library to solve the Could not deduce (KnownNat (n + 1)) issue.
Some necessary extensions:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
We need to produce a forall n. KnownNat n :- KnownNat (n + 1) value and then we need to “dispatch” it, so to speak, around the problematic expression.
For a first part, Data.Constraint.Nat has
plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
That’s what we need, with m ~ 1 (GHC finds the KnownNat 1 instance automatically).
The problematic expression from earlier was SomeVect on the rhs of
someVectCons x (SomeVect xs) = SomeVect $ VCons x xs
constraints has the \\ operator for “dispatching” an entailment. It’s used like this:
someVectCons x (SomeVect @n xs) = (SomeVect \\ plusNat @n @1) $ VCons x xs
And now it compiles!