sample of making and using proofs with CmpNat (and unsafeCoerce)

CmpNat-Proofs.hs

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

import Data.Constraint ((:-)(Sub), Dict(Dict))
import Data.Kind (Type)
import Data.Singletons (sing)
import Data.Singletons.Prelude (Sing(SEQ, SFalse, SGT, SLT, STrue), (%+), (%-), (%>), sCompare)
import Data.Singletons.Prelude.Num (PNum((+), (-)))
import Data.Singletons.Prelude.Ord (POrd((>)))
import Data.Singletons.TypeLits (SNat, Sing(SNat))
import Data.Type.Equality
import GHC.TypeLits (CmpNat, KnownNat, Nat)
import Unsafe.Coerce (unsafeCoerce)

data Foo where
  Foo
    :: forall (index :: Nat) (len :: Nat).
       (CmpNat index len ~ 'LT)
    => SNat index
    -> SNat len
    -> Foo

createFoo :: Foo
createFoo = Foo (sing @Nat @0) (sing @Nat @1)

incrementLength :: Foo -> Foo
incrementLength (Foo index len) =
  case bar index len of
    Sub Dict -> Foo index (len %+ (sing @_ @1))

bar :: forall n m. Sing n -> Sing m -> (CmpNat n m ~ 'LT) :- (CmpNat n (m + 1) ~ 'LT)
bar SNat SNat = Sub axiom
  where
    axiom :: CmpNat n m ~ 'LT => Dict (CmpNat n (m + 1) ~ 'LT)
    axiom = unsafeCoerce (Dict :: Dict (a ~ a))

-------------------------------------------------

data Bar :: Nat -> Nat -> Type where
  Bar
    :: forall (index :: Nat) (len :: Nat).
       (KnownNat index, KnownNat len, CmpNat index len ~ 'LT)
    => Bar index len

data Foo2 where
  Foo2 :: Bar index len -> Foo2

createFoo2 :: Foo2
createFoo2 = Foo2 $ Bar @0 @1

incrementLength2 :: Foo2 -> Foo2
incrementLength2 (Foo2 b) = Foo2 $ incLen b

incLen :: forall n m. Bar n m -> Bar n (m + 1)
incLen Bar =
  case bar (sing @_ @n) (sing @_ @m) of
    Sub Dict ->
      case (sing @_ @m) %+ (sing @_ @1) of
        SNat -> Bar

decrementLength2 :: Foo2 -> Maybe Foo2
decrementLength2 (Foo2 b) =
  case decLen2 b of
    Nothing -> Nothing
    Just newB -> Just $ Foo2 newB

decLen :: forall n m. (CmpNat n (m - 1) ~ 'LT) => Bar n m -> Bar n (m - 1)
decLen Bar =
  case (sing @_ @m) %- (sing @_ @1) of
    SNat -> Bar

decLen2 :: forall n m. Bar n m -> Maybe (Bar n (m - 1))
decLen2 Bar =
  case sCompare (sing @_ @n) ((sing @_ @m) %- (sing @_ @1)) of
    SLT ->
        case sing @_ @m %> sing @_ @0 of
          STrue ->
            case law2 (sing @_ @m) of
              Sub Dict -> Just Bar
          SFalse -> Nothing
    SEQ -> Nothing
    SGT -> Nothing

-- XXX: BEWARE! The following is incorrect.
-- For the reason why, see here:
-- https://stackoverflow.com/a/49710029/3040129
law2 :: forall m. Sing m -> (KnownNat m, m > 0 ~ 'True) :- KnownNat (m - 1)
law2 SNat = Sub axiom
  where
    axiom :: (KnownNat m, m > 0 ~ 'True) => Dict (KnownNat (m - 1))
    axiom = unsafeCoerce (Dict :: forall a. Dict (a ~ a))

This can be loaded into GHCI with the following command:

$ stack --resolver nightly-2018-03-18 ghci --package classy-prelude  --package singletons --package containers --package typelits-witnesses --package constraints