Playing around with length indexed text

Sized.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE TypeOperators #-}

module Data.Text.Sized
  ( Text
  , toSized
  ) where

import Data.Proxy (Proxy(Proxy))
import qualified Data.Text as Unsized
import GHC.TypeLits (type (+), KnownNat, Nat, natVal)

data Text (n :: Nat) where
  Text :: Unsized.Text -> Text n
  deriving (Eq, Ord, Show)

toSized ::
     forall n. (KnownNat n)
  => Unsized.Text
  -> Maybe (Text n)
toSized t
  | natVal (Proxy :: Proxy n) == fromIntegral (Unsized.length t) = Just (Text t)
  | otherwise = Nothing

fromSized :: Text n -> Unsized.Text
fromSized (Text t) = t

pack ::
     forall n. (KnownNat n)
  => String
  -> Maybe (Text n)
pack = toSized . Unsized.pack

singleton :: Char -> Text 1
singleton = Text . Unsized.singleton

cons :: KnownNat n => Char -> Text n -> Text (n + 1)
cons c (Text t) = Text (Unsized.cons c t)

snoc :: KnownNat n => Text n -> Char -> Text (n + 1)
snoc (Text t) c = Text (Unsized.snoc t c)

append :: (KnownNat n, KnownNat m) => Text n -> Text m -> Text (n + m)
append (Text a) (Text b) = Text (a `Unsized.append` b)

empty :: Text 0
empty = Text Unsized.empty

-- This won't compile, which is interesting!
--  > :t Unsized.foldr cons empty
-- <interactive>:1:15: error:
--     • Couldn't match type ‘1’ with ‘0’
--       Expected type: Char -> Text 0 -> Text 0
--         Actual type: Char -> Text 0 -> Text (0 + 1)
--     • In the first argument of ‘Unsized.foldr’, namely ‘cons’
--       In the expression: Unsized.foldr cons empty
-- toSized :: KnownNat n => Unsized.Text -> Text n
-- toSized = Unsized.foldr cons empty