在给定类型级别的起始KnownNat的情况下查找KnownNat的下一个因子

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits

type family FindNextFactor (n :: Nat) (m :: Nat) :: Nat where
  FindNextFactor n m = If (Mod n m == 0) m (FindNextFactor n (m + 1))

findNextFactor :: KnownNat n => Proxy n -> Integer
findNextFactor proxy = natVal proxy + 1 + findNextFactor' (natVal proxy + 1)
  where
    findNextFactor' :: Integer -> Integer
    findNextFactor' m = case someNatVal m of
      Just (SomeNat proxy') -> case sameNat proxy proxy' of
        Just Refl -> findNextFactor' (m + 1)
        Nothing -> case sameNat proxy (FindNextFactor (natVal proxy) 2) of
          Just Refl -> m
          Nothing -> findNextFactor' (m + 1)
      Nothing -> findNextFactor' (m + 1)