Haskell中基于CmpNat与singletons的证明相关函数实现

I’m working on building a set of functions to handle custom types in Haskell, using GHC 8.4.1. My setup relies on the singletons and constraints libraries, and I’ve enabled these language extensions to support the advanced type-level programming required:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ... #-}

The core goal here is to create type-safe functions that leverage singleton types to carry type-level information into runtime code, while using constraint kinds to enforce critical relationships between types.

内容的提问来源于stack exchange，提问作者illabout