A type class for statically checking if data is fully strict

CheckStrictness.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}

module CheckStrictness where
import GHC.Generics
import GHC.TypeLits

-- | A type class that decides if a data type is fully strict or not,
-- meaning that forcing it to whnf will fully force it
type IsStrict a = IsStrict' (Text " • When checking strictness of: " :<>: ShowType a) a

-- The error message argument is here to preserve context
class IsStrict' (e :: ErrorMessage) a

-- Automatically derive for generic types
instance {-# OVERLAPPABLE  #-}
        (Generic a , GIsStrict (Text " • In type: " :<>: ShowType a :$$: e) (Rep a a))
        => IsStrict' e a

-- Primitive data doesn't have generics, so we implement them manually
instance IsStrict' e Int
instance IsStrict' e Char

-- Prevent type checking loops for simple strict recursive types.
-- If the recursion goes via multiple levels or changes types, this won't prevent it.
-- in those cases, write a manual instance for the type
class BreakLoop (e :: ErrorMessage) a (b :: Bool)
instance IsStrict' e a => BreakLoop e a False
instance BreakLoop e a True -- Loop, so don't recurse further


type family IsEqual a b :: Bool where
    IsEqual a a = True
    IsEqual a b = False


class GIsStrict (e :: ErrorMessage) a
instance (GIsStrict e (f p), GIsStrict e (g p)) => GIsStrict e ((f :*: g) p)
instance (GIsStrict e (f p), GIsStrict e (g p)) => GIsStrict e ((f :+: g) p)
instance GIsStrict e (U1 p)
instance GIsStrict e (V1 p)
-- instance IsStrict' e k => GIsStrict e (Rec0 k p)
instance BreakLoop e k (IsEqual k p) => GIsStrict e (Rec0 k p)

instance GIsStrict e (f p) => GIsStrict e (D1 m f p)
instance GIsStrict (Text " • In constructor: " :<>: Text nm :$$: e) (f p) => GIsStrict e (C1 (MetaCons nm fx b) f p)
instance GIsStrict (Text " • In strict field" :<>: ShowName nm :<>: Text " of type " :<>: ShowType k :$$: e) (Rec0 k p) => GIsStrict e (S1 (MetaSel nm su ss DecidedStrict) (Rec0 k) p)
instance GIsStrict (Text " • In unpacked field" :<>: ShowName nm :<>: Text " of type " :<>: ShowType k :$$: e) (Rec0 k p) => GIsStrict e (S1 (MetaSel nm su ss DecidedUnpack) (Rec0 k) p)

instance TypeError (Text "Found lazy field" :<>: ShowName nm :<>: Text " of type " :<>: ShowType k :$$: e)
  => GIsStrict e (S1 (MetaSel nm su ss DecidedLazy) (Rec0 k) p)

type family ShowName a where
    ShowName Nothing = Text ""
    ShowName (Just nm) = Text " ‘" :<>: Text nm :<>: Text "‘"

nfStrict :: IsStrict a => a -> ()
nfStrict a = a `seq` ()

-- * Examples:

-- >>> nfStrict @(Int, Int)
-- Found lazy field of type Int
--  • In constructor: (,)
--  • In type: (Int, Int)
--  • When checking strictness of: (Int, Int)

-- >>> nfStrict @Char 'a'
-- ()

-- >>> nfStrict @String
-- Found lazy field of type Char
--  • In constructor: :
--  • In type: [Char]
--  • When checking strictness of: String
-- Found lazy field of type [Char]
--  • In constructor: :
--  • In type: [Char]
--  • When checking strictness of: String

data StrictPair a b = P !a !b
  deriving Generic

-- Non-strict type in strict field
-- >>> nfStrict @(StrictPair Int String)
-- Found lazy field of type Char
--  • In constructor: :
--  • In type: [Char]
--  • In strict field of type [Char]
--  • In constructor: P
--  • In type: StrictPair Int String
--  • When checking strictness of: StrictPair Int String
-- Found lazy field of type [Char]
--  • In constructor: :
--  • In type: [Char]
--  • In strict field of type [Char]
--  • In constructor: P
--  • In type: StrictPair Int String
--  • When checking strictness of: StrictPair Int String


-- Explicit record selector name
-- >>> nfStrict @(Rec0 Int ())
-- Found lazy field ‘unK1‘ of type Int
--  • In constructor: K1
--  • In type: K1 R Int ()
--  • When checking strictness of: Rec0 Int ()

-- >>> nfStrict @(StrictPair () Int) (P () 0)
-- ()

-- Only strict in the spine
data SpineStrictList a = SSLNil | SSLCons a !(SpineStrictList a) deriving Generic

-- Would cause infinite recursion in type checking without explicit loop breaking
-- >>> nfStrict @(SpineStrictList String)
-- Found lazy field of type Char
--  • In constructor: :
--  • In type: [Char]
--  • In strict field of type [Char]
--  • In constructor: SSLCons
--  • In type: SpineStrictList String
--  • When checking strictness of: SpineStrictList String
-- Found lazy field of type [Char]
--  • In constructor: :
--  • In type: [Char]
--  • In strict field of type [Char]
--  • In constructor: SSLCons
--  • In type: SpineStrictList String
--  • When checking strictness of: SpineStrictList String

-- Fully strict list
data StrictList a = SLNil | SLCons !a !(StrictList a) deriving Generic

-- A strict list of strict data is strict
-- >>> nfStrict @(StrictList Int) (SLCons 0 SLNil)
-- ()

-- But a strict list of non-strict data is not strict
-- >>> nfStrict @(StrictList String)
-- Found lazy field of type Char
--  • In constructor: :
--  • In type: [Char]
--  • In strict field of type [Char]
--  • In constructor: SLCons
--  • In type: StrictList String
--  • When checking strictness of: StrictList String
-- Found lazy field of type [Char]
--  • In constructor: :
--  • In type: [Char]
--  • In strict field of type [Char]
--  • In constructor: SLCons
--  • In type: StrictList String
--  • When checking strictness of: StrictList String

CheckStrictness2.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
-- {-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE QuantifiedConstraints #-}

module CheckStrictness2 where
import GHC.Generics
import GHC.TypeLits
import Data.Proxy (Proxy (Proxy))

-- An alternative version where you need to explicitly derive the instances
-- The errors are slightly less detailed, but the loop issues are gone

-- | A type class that decides if a data type is fully strict or not,
-- meaning that forcing it to whnf will fully force it
-- The error message argument is here to preserve context
class IsStrict a where
  fastDeepseq :: a -> b -> b
  -- Need to have a method in order to use default signatures to restrict simple deriving
  -- The other alternative would be to only use deriving via, but that's more error prone
  default fastDeepseq :: (Generic a, GIsStrict ('Text " • When checking strictness of: " ':<>: 'ShowType a) (Rep a a)) =>
      a -> b -> b
  fastDeepseq = seq

newtype Generically a = Generically a

-- Automatically derive for generic types
instance (Generic a , GIsStrict (Text " • In type: " :<>: ShowType a) (Rep a a))
        => IsStrict (Generically a) where
  fastDeepseq :: (Generic a, GIsStrict ('Text " • In type: " ':<>: 'ShowType a) (Rep a a)) =>
      Generically a -> b -> b
  fastDeepseq = seq

newtype AssumeStrict a = AssumeStrict a

instance IsStrict (AssumeStrict a) where
  fastDeepseq = seq

-- Primitive data doesn't have generics, so we implement them manually
deriving via (AssumeStrict Int) instance IsStrict Int
deriving via (AssumeStrict Char) instance IsStrict Char


class GIsStrict (e :: ErrorMessage) a
instance (GIsStrict e (f p), GIsStrict e (g p)) => GIsStrict e ((f :*: g) p)
instance (GIsStrict e (f p), GIsStrict e (g p)) => GIsStrict e ((f :+: g) p)
instance GIsStrict e (U1 p)
instance GIsStrict e (V1 p)
instance IsStrict k => GIsStrict e (Rec0 k p)

instance GIsStrict e (f p) => GIsStrict e (D1 m f p)
instance GIsStrict (Text " • In constructor: " :<>: Text nm :$$: e) (f p) => GIsStrict e (C1 (MetaCons nm fx b) f p)
instance GIsStrict (Text " • In strict field" :<>: ShowName nm :<>: Text " of type " :<>: ShowType k :$$: e) (Rec0 k p) => GIsStrict e (S1 (MetaSel nm su ss DecidedStrict) (Rec0 k) p)
instance GIsStrict (Text " • In unpacked field" :<>: ShowName nm :<>: Text " of type " :<>: ShowType k :$$: e) (Rec0 k p) => GIsStrict e (S1 (MetaSel nm su ss DecidedUnpack) (Rec0 k) p)
instance TypeError (Text "Found lazy field" :<>: ShowName nm :<>: Text " of type " :<>: ShowType k :$$: e)
  => GIsStrict e (S1 (MetaSel nm su ss DecidedLazy) (Rec0 k) p)

type family ShowName a where
    ShowName Nothing = Text ""
    ShowName (Just nm) = Text " ‘" :<>: Text nm :<>: Text "‘"

-- | For a strict data type, seq is the same as deepseq
nfStrict :: IsStrict a => a -> ()
nfStrict a = a `seq` ()

-- * Examples:

-- >>> instance IsStrict (a , b)
-- Found lazy field of type a
--  • In constructor: (,)
--  • When checking strictness of: (a, b)
-- Found lazy field of type b
--  • In constructor: (,)
--  • When checking strictness of: (a, b)

-- >>> instance IsStrict String
-- Found lazy field of type Char
--  • In constructor: :
--  • When checking strictness of: String
-- Found lazy field of type [Char]
--  • In constructor: :
--  • When checking strictness of: String

-- >>> nfStrict @(Int, Int)
-- No instance for (IsStrict (Int, Int))
--   arising from a use of ‘nfStrict’

-- >>> nfStrict @Char 'a'
-- ()

-- >>> nfStrict @String
-- No instance for (IsStrict String) arising from a use of ‘nfStrict’

data StrictPair a b = P !a !b
  deriving (Generic, IsStrict)

-- Non-strict type in strict field
-- >>> nfStrict @(StrictPair Int String)
-- No instance for (IsStrict [Char]) arising from a use of ‘nfStrict’

-- >>> instance IsStrict (Rec0 a b)
-- Found lazy field ‘unK1‘ of type a
--  • In constructor: K1
--  • When checking strictness of: Rec0 a b

-- Explicit record selector name
-- >>> nfStrict @(Rec0 Int ())
-- No instance for (IsStrict (Rec0 Int ()))
--   arising from a use of ‘nfStrict’

instance IsStrict ()

-- >>> nfStrict @(StrictPair () Int) (P () 0)
-- No instance for (IsStrict ()) arising from a use of ‘nfStrict’

-- Only strict in the spine
data SpineStrictList a = SSLNil | SSLCons a !(SpineStrictList a) deriving (Generic, IsStrict)

-- instance IsStrict a => IsStrict (SpineStrictList a)

-- No longer need loop breaking to protect this
-- >>> nfStrict @(SpineStrictList String)
-- No instance for (IsStrict [Char]) arising from a use of ‘nfStrict’

-- Spine strict is enough to make it derive full strictness
-- >>> nfStrict @(SpineStrictList Int) (SSLCons 0 SSLNil)
-- ()

-- Fully strict list
data StrictList a = SLNil | SLCons !a !(StrictList a) deriving (Generic, IsStrict)

-- instance IsStrict a => IsStrict (StrictList a)

-- A strict list of strict data is strict
-- >>> nfStrict @(StrictList Int) (SLCons 0 SLNil)
-- ()

-- But a strict list of non-strict data is not strict
-- >>> nfStrict @(StrictList String)
-- No instance for (IsStrict [Char]) arising from a use of ‘nfStrict’