OverloadedLabels for checked ByteString literals

SafeByteStringLiteralsOverloadedLabels.hs

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

import qualified Data.ByteString.Char8 as BS
import Data.Kind
import Data.Proxy
import GHC.OverloadedLabels
import GHC.TypeError
import GHC.TypeLits
import Data.Type.Ord

type Is8BitSymbol :: Symbol -> Constraint
type Is8BitSymbol s = Is8BitMaybe (UnconsSymbol s)

type Is8BitMaybe :: Maybe (Char, Symbol) -> Constraint
type family Is8BitMaybe _mb where
  Is8BitMaybe Nothing = ()
  Is8BitMaybe (Just '(c, s)) = (Is8BitChar c, Is8BitSymbol s)

type Is8BitChar :: Char -> Constraint
type Is8BitChar c = OrdCond (Compare (CharToNat c) 255)
                            (() :: Constraint)
                            (() :: Constraint)
                            (Unsatisfiable (Text "Invalid character in ByteString literal: " :<>: ShowType c))

instance (Is8BitSymbol lit, KnownSymbol lit) => IsLabel lit BS.ByteString where
  fromLabel = BS.pack (symbolVal (Proxy @lit))


good, bad :: BS.ByteString
good = #"ascii is fine"
bad = #"bla語"
{-
    • Invalid character in ByteString literal: '\35486'
    • In the expression: #"bla語"
      In an equation for ‘bad’: bad = #"bla語"
-}

SafeByteStringLiteralsPatternSynonym.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RequiredTypeArguments #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wall -Wno-unused-top-binds #-}

module SafeByteStringLiteralsPatternSynonym
  ( BS.ByteString(Bytes)
  , pack
  ) where

import qualified Data.ByteString.Char8 as BS
import Data.Kind
import Data.Proxy
import GHC.TypeError
import GHC.TypeLits
import Data.Type.Ord

type Is8BitSymbol :: Symbol -> Constraint
type Is8BitSymbol s = Is8BitMaybe (UnconsSymbol s)

type Is8BitMaybe :: Maybe (Char, Symbol) -> Constraint
type family Is8BitMaybe _mb where
  Is8BitMaybe Nothing = ()
  Is8BitMaybe (Just '(c, s)) = (Is8BitChar c, Is8BitSymbol s)

type Is8BitChar :: Char -> Constraint
type Is8BitChar c = OrdCond (Compare (CharToNat c) 255)
                            (() :: Constraint)
                            (() :: Constraint)
                            (Unsatisfiable (Text "Invalid character in ByteString literal: " :<>: ShowType c))

type Known8BitSymbol lit = (Is8BitSymbol lit, KnownSymbol lit)

-- | Safe version of 'BS.pack' that requires the argument to be a string literal
-- for which all the characters fit in 8 bits.
pack :: forall (lit :: Symbol) -> Known8BitSymbol lit => BS.ByteString
pack s = BS.pack (symbolVal (Proxy @s))

-- Pattern synonym version of 'pack', so one can pattern match on known-valid
-- bytestrings.
--
-- TODO: ideally we would use visible dependent quantification here, but that
-- isn't supported yet for pattern synonyms, see
-- https://gitlab.haskell.org/ghc/ghc/-/issues/23704
--
pattern Bytes :: forall (s :: Symbol) . Known8BitSymbol s => BS.ByteString
pattern Bytes <- ((pack s ==) -> True)
  where
    Bytes = pack s


good :: BS.ByteString
good = Bytes @"ascii is fine"

good2 :: BS.ByteString -> Bool
good2 (Bytes @"including in pattern matching") = True
good2 _ = False

bad :: BS.ByteString
bad = Bytes @"bla語"
{-
    • Invalid character in ByteString literal: '\35486'
    • In the expression: Bytes @"bla語"
      In an equation for ‘bad’: bad = Bytes "bla語"
-}

f :: BS.ByteString -> Bool
f (Bytes @"語") = True
f _ = False
{-
    • Invalid character in ByteString literal: '\35486'
    • In the pattern: Bytes @"語"
      In an equation for ‘f’: f (Bytes @"語") = True
-}