Errors.hs

module Type.Errors
  ( -- * Generating Error Messages
    ErrorMessage (..)
  , PrettyPrintList
  , ShowTypeQuoted

    -- * Emitting Error Messages
  , TypeError
  , DelayError
  , DelayErrorFcf
  , NoError
  , NoErrorFcf

  -- * Observing Stuckness
  , IfStuck
  , WhenStuck
  , UnlessStuck

    -- * Observing Phantomness
  , PHANTOM
  , UnlessPhantom
  , UnlessPhantomFcf

    -- * Performing Type Substitutions
  , Subst
  , VAR
  , SubstVar

    -- * Working With Fcfs
  , Exp
  , Eval
  , Pure
  ) where

import Data.Coerce
import Data.Kind
import Fcf
import GHC.TypeLits



-- $setup
-- >>> :m +Data.Kind
-- >>> :m +Data.Proxy
-- >>> import GHC.Generics (Generic (..))
-- >>> :def! show_error (\msg -> pure $ "let foo :: DelayError (" ++ msg ++ ") => (); foo = (); in foo")
-- >>> :def! eval_error (\msg -> pure $ "let foo :: (" ++ msg ++ ") => (); foo = (); in foo")
-- >>> :{
-- data HasNoRep = HasNoRep
-- :}


------------------------------------------------------------------------------
-- | Pretty print a list.
--
-- >>> :show_error PrettyPrintList '[Bool]
-- ...
-- ... 'Bool'
-- ...
--
-- >>> :show_error PrettyPrintList '[1, 2]
-- ...
-- ... '1', and '2'
-- ...
--
-- >>> :show_error PrettyPrintList '["hello", "world", "cool"]
-- ...
-- ... "hello", "world", and "cool"
-- ...
--
-- @since 0.1.0.0
type family PrettyPrintList (vs :: [k]) :: ErrorMessage where
  PrettyPrintList '[]       = 'Text ""
  PrettyPrintList '[a]      = ShowTypeQuoted a
  PrettyPrintList '[a, b]   = ShowTypeQuoted a ':<>: 'Text ", and " ':<>: ShowTypeQuoted b
  PrettyPrintList (a ': vs) = ShowTypeQuoted a ':<>: 'Text ", " ':<>: PrettyPrintList vs


------------------------------------------------------------------------------
-- | Like 'ShowType', but quotes the type if necessary.
--
-- >>> :show_error ShowTypeQuoted Int
-- ...
-- ... 'Int'
-- ...
--
-- >>> :show_error ShowTypeQuoted "symbols aren't quoted"
-- ...
-- ... "symbols aren't quoted"
-- ...
--
-- @since 0.1.0.0
type family ShowTypeQuoted (t :: k) :: ErrorMessage where
  ShowTypeQuoted (t :: Symbol) = 'ShowType t
  ShowTypeQuoted t             = 'Text "'" ':<>: 'ShowType t ':<>: 'Text "'"


------------------------------------------------------------------------------
-- | Error messages produced via 'TypeError' are often /too strict/, and will
-- be emitted sooner than you'd like. The solution is to use 'DelayError',
-- which will switch the error messages to being consumed lazily.
--
-- >>> :{
-- foo :: TypeError ('Text "Too eager; prevents compilation") => ()
-- foo = ()
-- :}
-- ...
-- ... Too eager; prevents compilation
-- ...
--
-- >>> :{
-- foo :: DelayError ('Text "Lazy; emitted on use") => ()
-- foo = ()
-- :}
--
-- >>> foo
-- ...
-- ... Lazy; emitted on use
-- ...
--
-- @since 0.1.0.0
type DelayError err = Eval (DelayErrorFcf err)


------------------------------------------------------------------------------
-- | Like 'DelayError', but implemented as a first-class family.
-- 'DelayErrorFcf' is useful when used as the last argument to 'IfStuck' and
-- 'UnlessStuck'.
--
-- @since 0.1.0.0
data DelayErrorFcf :: ErrorMessage -> Exp k
type instance Eval (DelayErrorFcf a) = TypeError a


------------------------------------------------------------------------------
-- | A helper definition that /doesn't/ emit a type error. This is
-- occassionally useful to leave as the residual constraint in 'IfStuck' when
-- you only want to observe if an expression /isn't/ stuck.
--
-- @since 0.1.0.0
type NoError = (() :: Constraint)


------------------------------------------------------------------------------
-- | Like 'NoError', but implemented as a first-class family.  'NoErrorFcf' is
-- useful when used as the last argument to 'IfStuck' and 'UnlessStuck'.
--
-- @since 0.1.0.0
type NoErrorFcf = Pure NoError


------------------------------------------------------------------------------
-- | @'IfStuck' expr b c@ leaves @b@ in the residual constraints whenever
-- @expr@ is stuck, otherwise it 'Eval'uates @c@.
--
-- Often you want to leave a 'DelayError' in @b@ in order to report an error
-- when @expr@ is stuck.
--
-- The @c@ parameter is a first-class family, which allows you to perform
-- arbitrarily-complicated type-level computations whenever @expr@ isn't stuck.
-- For example, you might want to produce a typeclass 'Constraint' here.
-- Alternatively, you can nest calls to 'IfStuck' in order to do subsequent
-- processing.
--
-- This is a generalization of <https://kcsongor.github.io/ kcsongor>'s @Break@
-- machinery described in
-- <https://kcsongor.github.io/report-stuck-families/ detecting the undetectable>.
--
-- @since 0.1.0.0
type family IfStuck (expr :: k) (b :: k1) (c :: Exp k1) :: k1 where
  IfStuck (_ AnythingOfAnyKind) b c = b
  IfStuck a                     b c = Eval c

data AnythingOfAnyKind


------------------------------------------------------------------------------
-- | Like 'IfStuck', but specialized to the case when you don't want to do
-- anything if @expr@ isn't stuck.
--
-- >>> :{
-- observe_no_rep
--     :: WhenStuck
--          (Rep t)
--          (DelayError ('Text "No Rep instance for " ':<>: ShowTypeQuoted t))
--     => t
--     -> ()
-- observe_no_rep _ = ()
-- :}
--
-- >>> observe_no_rep HasNoRep
-- ...
-- ... No Rep instance for 'HasNoRep'
-- ...
--
-- >>> observe_no_rep True
-- ()
--
-- @since 0.1.0.0
type WhenStuck expr b   = IfStuck expr b NoErrorFcf


------------------------------------------------------------------------------
-- | Like 'IfStuck', but leaves no residual constraint when @expr@ is stuck.
-- This can be used to ensure an expression /isn't/ stuck before analyzing it
-- further.
--
-- See the example under 'UnlessPhantomFcf' for an example of this use-case.
--
-- @since 0.1.0.0
type UnlessStuck expr c = IfStuck expr NoError c


------------------------------------------------------------------------------
-- | A meta-variable for marking which argument should be a phantom when
-- working with 'UnlessPhantom' and 'UnlessPhantomFcf'.
--
-- 'PHANTOM' is polykinded and can be used in several settings.
--
-- See 'UnlessPhantom' for examples.
--
-- @since 0.1.0.0
type PHANTOM = VAR


------------------------------------------------------------------------------
-- | @'UnlessPhantom' expr err@ determines if the type described by @expr@
-- is phantom in the variables marked via 'PHANTOM'. If it's not, it produces
-- the error message @err@.
--
-- For example, consider the definition:
--
-- >>> :{
-- data Qux a b = Qux b
-- :}
--
-- which is phantom in @a@:
--
-- >>> :eval_error UnlessPhantom (Qux PHANTOM Int) ('Text "Ok")
-- ()
--
-- but not in @b@:
--
-- >>> :eval_error UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!")
-- ...
-- ... Bad!
-- ...
--
-- Unfortunately there is no known way to emit an error message if the variable
-- /is/ a phantom.
--
-- @since 0.1.0.0
type UnlessPhantom exp err = Eval (UnlessPhantomFcf exp err)


------------------------------------------------------------------------------
-- | Like 'UnlessPhantom', but implemented as a first-class family. As such,
-- this allows 'UnlessPhantomFcf' to be chained after 'IfStuck' to only be run
-- if an expression isn't stuck.
--
-- This can be used to avoid emitting false error messages when a type variable
-- isn't phantom, just ambiguous.
--
-- >>> :{
-- observe_phantom
--     :: UnlessStuck
--          f
--          (UnlessPhantomFcf
--            (f PHANTOM)
--            ('Text "It's not phantom!"))
--     => f p
--     -> ()
-- observe_phantom _ = ()
-- :}
--
-- >>> observe_phantom Proxy
-- ()
--
-- >>> observe_phantom (Just 5)
-- ...
-- ... It's not phantom!
-- ...
--
-- In the next example, we leave @observe_phantom@ unsaturated, and therefore
-- @f@ isn't yet known. Without guarding the 'UnlessPhantomFcf' behind
-- 'UnlessStuck', this would incorrectly produce the message "It's not
-- phantom!"
--
-- >>> observe_phantom
-- ...
-- ... No instance for (Show ...
-- ...
--
-- @since 0.1.0.0
data UnlessPhantomFcf :: k -> ErrorMessage -> Exp Constraint
type instance Eval (UnlessPhantomFcf exp err) =
  Coercible (SubstVar exp Stuck)
            (SubstVar exp (DelayError err))


------------------------------------------------------------------------------
-- | @'Subst' expr a b@ substitutes all instances of @a@ for @b@ in @expr@.
--
-- >>> :kind! Subst (Either Int Int) Int Bool
-- ...
-- = Either Bool Bool
--
-- >>> :kind! Subst (Either Int Bool) Int [Char]
-- ...
-- = Either [Char] Bool
--
-- >>> :kind! Subst (Either Int Bool) Either (->)
-- ...
-- = Int -> Bool
--
-- @since 0.1.0.0
type family Subst (e :: k1) (var :: k2) (sub :: k2) :: k1 where
  Subst var var sub   = sub
  Subst (a b) var sub = Subst a var sub (Subst b var sub)
  Subst a var sub     = a

data Var
type family SubMe :: Type -> k

------------------------------------------------------------------------------
-- | 'VAR' is a meta-varaible which marks a substitution in 'SubstVar'. The
-- result of @'SubstVar' expr val@ is @expr[val/'VAR']@.
--
-- 'VAR' is polykinded and can be used in several settings.
--
-- See 'SubstVar' for examples.
--
-- @since 0.1.0.0
type VAR = SubMe Var


------------------------------------------------------------------------------
-- | Like 'Subst', but uses the explicit meta-variable 'VAR' to mark
-- substitution points.
--
-- >>> :kind! SubstVar (Either VAR Bool) [Char]
-- ...
-- = Either [Char] Bool
--
-- >>> :kind! SubstVar (VAR Int Bool :: Type) (->)
-- ...
-- = Int -> Bool
--
-- @since 0.1.0.0
type family SubstVar (e :: k1) (r :: k2) :: k1 where
  SubstVar (_ Var) r = r
  SubstVar (a b) r   = SubstVar a r (SubstVar b r)
  SubstVar a r       = a