"Propagate the constraints" works for recursive examples, contrary to README

[adamgundry]

Hi @gelisam, I've just come across this project and it looks very nice. I especially appreciated the comparison of the typelevel-rewrite-rules approach to the other possible solutions out there. This is something that many packages don't include, but it is very useful.

That said, I think the discussion of "propagate the constraints" is overly negative when it comes to recursive functions. Using a constraint family, it is possible to recursively define the constraints required by a function like appendSingletons so that they can be propagated to the use site, like this:

type AppendLemma :: Nat -> Nat -> Constraint
type family AppendLemma m n where
  AppendLemma m Z     = m + Z  ~  m
  AppendLemma m (S n) = ( (m + S Z) + n  ~  m + S n
                        , AppendLemma (m + S Z) n
                        )

appendSingletons
  :: AppendLemma m n
  => Vec m a
  -> Vec n (Vec ('S 'Z) a)
  -> Vec (m + n) a
appendSingletons xsM VNil
  -- uses (m + 'Z) ~ m
  = xsM
appendSingletons xsM (singleton1 ::: singletons)
  -- uses (m + 'S 'Z + n) ~ (m + 'S n)
  = appendSingletons (xsM ++ singleton1) singletons

There's no need to accumulate an infinite number of constraints, because AppendLemma, like appendSingletons, is structurally recursive in its second argument.

Of course you're quite correct that this approach can accumulate a lot of constraints, thereby adding complexity and endangering compile-time performance (and potentially runtime -- I'm not sure how much of this will be removed by the optimizer). It's also problematic if you have existentially-quantified variables, because you may be unable to propagate constraints that mention them, and instead need to supply a proof at that point.