{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}

-- | The 'ZonkM' monad, a stripped down 'TcM', used when zonking within
-- the typechecker in "GHC.Tc.Zonk.TcType".
--
-- See Note [Module structure for zonking] in GHC.Tc.Zonk.Type.
module GHC.Tc.Zonk.Monad
  ( -- * The 'ZonkM' monad, a stripped down 'TcM' for zonking
    ZonkM(ZonkM,runZonkM)
  , ZonkGblEnv(..), getZonkGblEnv, getZonkTcLevel

   -- ** Logging within 'ZonkM'
  , traceZonk

  )
  where

import GHC.Prelude

import GHC.Driver.Flags ( DumpFlag(Opt_D_dump_tc_trace) )

import GHC.Types.SrcLoc ( SrcSpan )

import GHC.Tc.Types.BasicTypes ( TcBinderStack )
import GHC.Tc.Utils.TcType   ( TcLevel )

import GHC.Utils.Logger
import GHC.Utils.Outputable

import Control.Monad          ( when )
import Control.Monad.IO.Class ( MonadIO(..) )

import GHC.Exts               ( oneShot )

--------------------------------------------------------------------------------

-- | Information needed by the 'ZonkM' monad, which is a slimmed down version
-- of 'TcM' with just enough information for zonking.
data ZonkGblEnv
  = ZonkGblEnv
    { ZonkGblEnv -> Logger
zge_logger       :: Logger     -- needed for traceZonk
    , ZonkGblEnv -> NamePprCtx
zge_name_ppr_ctx :: NamePprCtx --          ''
    , ZonkGblEnv -> SrcSpan
zge_src_span     :: SrcSpan  -- needed for skolemiseUnboundMetaTyVar
    , ZonkGblEnv -> TcLevel
zge_tc_level     :: TcLevel  --               ''
    , ZonkGblEnv -> TcBinderStack
zge_binder_stack :: TcBinderStack -- needed for tcInitTidyEnv
    }

-- | A stripped down version of 'TcM' which is sufficient for zonking types.
newtype ZonkM a = ZonkM' { forall a. ZonkM a -> ZonkGblEnv -> IO a
runZonkM :: ZonkGblEnv -> IO a }
{-
NB: we write the following instances by hand:

--  deriving (Functor, Applicative, Monad, MonadIO)
--    via ReaderT ZonkGblEnv IO

See Note [Instances for ZonkT] in GHC.Tc.Zonk.Env for the reasoning:

  - oneShot annotations,
  - strictness annotations to enable worker-wrapper.
-}

{-# COMPLETE ZonkM #-}
pattern ZonkM :: forall a. (ZonkGblEnv -> IO a) -> ZonkM a
pattern $mZonkM :: forall {r} {a}.
ZonkM a -> ((ZonkGblEnv -> IO a) -> r) -> ((# #) -> r) -> r
$bZonkM :: forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM m <- ZonkM' m
  where
    ZonkM ZonkGblEnv -> IO a
m = (ZonkGblEnv -> IO a) -> ZonkM a
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM' ((ZonkGblEnv -> IO a) -> ZonkGblEnv -> IO a
forall a b. (a -> b) -> a -> b
oneShot ZonkGblEnv -> IO a
m)
-- See Note [The one-shot state monad trick] in GHC.Utils.Monad

instance Functor ZonkM where
  fmap :: forall a b. (a -> b) -> ZonkM a -> ZonkM b
fmap a -> b
f (ZonkM ZonkGblEnv -> IO a
g) = (ZonkGblEnv -> IO b) -> ZonkM b
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM ((ZonkGblEnv -> IO b) -> ZonkM b)
-> (ZonkGblEnv -> IO b) -> ZonkM b
forall a b. (a -> b) -> a -> b
$ \ !ZonkGblEnv
env -> (a -> b) -> IO a -> IO b
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (ZonkGblEnv -> IO a
g ZonkGblEnv
env)
  a
a <$ :: forall a b. a -> ZonkM b -> ZonkM a
<$ ZonkM ZonkGblEnv -> IO b
g     = (ZonkGblEnv -> IO a) -> ZonkM a
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM ((ZonkGblEnv -> IO a) -> ZonkM a)
-> (ZonkGblEnv -> IO a) -> ZonkM a
forall a b. (a -> b) -> a -> b
$ \ !ZonkGblEnv
env -> a
a a -> IO b -> IO a
forall a b. a -> IO b -> IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ZonkGblEnv -> IO b
g ZonkGblEnv
env
  {-# INLINE fmap #-}
  {-# INLINE (<$) #-}
instance Applicative ZonkM where
  pure :: forall a. a -> ZonkM a
pure a
a = (ZonkGblEnv -> IO a) -> ZonkM a
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM (\ !ZonkGblEnv
_ -> a -> IO a
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)
  ZonkM ZonkGblEnv -> IO (a -> b)
f <*> :: forall a b. ZonkM (a -> b) -> ZonkM a -> ZonkM b
<*> ZonkM ZonkGblEnv -> IO a
x = (ZonkGblEnv -> IO b) -> ZonkM b
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM (\ !ZonkGblEnv
env -> ZonkGblEnv -> IO (a -> b)
f ZonkGblEnv
env IO (a -> b) -> IO a -> IO b
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ZonkGblEnv -> IO a
x ZonkGblEnv
env )
  ZonkM ZonkGblEnv -> IO a
m *> :: forall a b. ZonkM a -> ZonkM b -> ZonkM b
*> ZonkM b
f = (ZonkGblEnv -> IO b) -> ZonkM b
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM (\ !ZonkGblEnv
env -> ZonkGblEnv -> IO a
m ZonkGblEnv
env IO a -> IO b -> IO b
forall a b. IO a -> IO b -> IO b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ZonkM b -> ZonkGblEnv -> IO b
forall a. ZonkM a -> ZonkGblEnv -> IO a
runZonkM ZonkM b
f ZonkGblEnv
env)
  {-# INLINE pure #-}
  {-# INLINE (<*>) #-}
  {-# INLINE (*>) #-}

instance Monad ZonkM where
  ZonkM ZonkGblEnv -> IO a
m >>= :: forall a b. ZonkM a -> (a -> ZonkM b) -> ZonkM b
>>= a -> ZonkM b
f =
    (ZonkGblEnv -> IO b) -> ZonkM b
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM (\ !ZonkGblEnv
env -> do { r <- ZonkGblEnv -> IO a
m ZonkGblEnv
env
                        ; runZonkM (f r) env })
  >> :: forall a b. ZonkM a -> ZonkM b -> ZonkM b
(>>)   = ZonkM a -> ZonkM b -> ZonkM b
forall a b. ZonkM a -> ZonkM b -> ZonkM b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
(*>)
  {-# INLINE (>>=) #-}
  {-# INLINE (>>) #-}

instance MonadIO ZonkM where
  liftIO :: forall a. IO a -> ZonkM a
liftIO IO a
f = (ZonkGblEnv -> IO a) -> ZonkM a
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM (\ !ZonkGblEnv
_ -> IO a
f)
  {-# INLINE liftIO #-}

getZonkGblEnv :: ZonkM ZonkGblEnv
getZonkGblEnv :: ZonkM ZonkGblEnv
getZonkGblEnv = (ZonkGblEnv -> IO ZonkGblEnv) -> ZonkM ZonkGblEnv
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM ZonkGblEnv -> IO ZonkGblEnv
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
{-# INLINE getZonkGblEnv #-}

getZonkTcLevel :: ZonkM TcLevel
getZonkTcLevel :: ZonkM TcLevel
getZonkTcLevel = (ZonkGblEnv -> IO TcLevel) -> ZonkM TcLevel
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM (\ZonkGblEnv
env -> TcLevel -> IO TcLevel
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZonkGblEnv -> TcLevel
zge_tc_level ZonkGblEnv
env))

-- | Same as 'traceTc', but for the 'ZonkM' monad.
traceZonk :: String -> SDoc -> ZonkM ()
traceZonk :: String -> SDoc -> ZonkM ()
traceZonk String
herald SDoc
doc = (ZonkGblEnv -> IO ()) -> ZonkM ()
forall a. (ZonkGblEnv -> IO a) -> ZonkM a
ZonkM ((ZonkGblEnv -> IO ()) -> ZonkM ())
-> (ZonkGblEnv -> IO ()) -> ZonkM ()
forall a b. (a -> b) -> a -> b
$
  \ ( ZonkGblEnv { zge_logger :: ZonkGblEnv -> Logger
zge_logger = !Logger
logger, zge_name_ppr_ctx :: ZonkGblEnv -> NamePprCtx
zge_name_ppr_ctx = NamePprCtx
ppr_ctx }) ->
    do { let sty :: PprStyle
sty   = NamePprCtx -> PprStyle
mkDumpStyle NamePprCtx
ppr_ctx
             flag :: DumpFlag
flag  = DumpFlag
Opt_D_dump_tc_trace
             title :: String
title = String
""
             msg :: SDoc
msg   = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
herald) Int
2 SDoc
doc
       ; Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Logger -> DumpFlag -> Bool
logHasDumpFlag Logger
logger DumpFlag
flag) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
         Logger
-> PprStyle -> DumpFlag -> String -> DumpFormat -> SDoc -> IO ()
logDumpFile Logger
logger PprStyle
sty DumpFlag
flag String
title DumpFormat
FormatText SDoc
msg
       }
{-# INLINE traceZonk #-}
  -- see Note [INLINE conditional tracing utilities] in GHC.Tc.Utils.Monad