Sorted.hs

{-# LANGUAGE GHC2021, TypeData, GADTs, UndecidableInstances #-}

module Sorted where

data SortedList a rel head where
  SortedNil :: SortedList a rel top
  SortedCons :: rel x top -> a x -> SortedList a rel top -> SortedList a rel x

class Rel rel x y where
  rel :: rel x y

(*:) :: Rel rel x top => a x -> SortedList a rel top -> SortedList a rel x
(*:) x xs = SortedCons rel x xs
infixr *:

type data TyNat = Z | S TyNat
data Nat n where
  Z :: Nat Z
  S :: Nat n -> Nat (S n)

data NatLTE x y where
  NatLTE_base :: NatLTE Z y
  NatLTE_step :: NatLTE x y -> NatLTE (S x) (S y)

instance Rel NatLTE Z y where
  rel = NatLTE_base

instance (Rel NatLTE x y, S y ~ y') => Rel NatLTE (S x) y' where
  rel = NatLTE_step rel

example :: SortedList Nat NatLTE Z
example = Z *: S Z *: S (S (S (S Z))) *: S (S (S (S (S (S Z))))) *: SortedNil