{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

{-|
Module: GHC.TcPlugin.API.Internal

This module provides operations to directly lift and unlift computations in
GHC's 'GHC.Tc.TcM' monad to the various type-checking plugin monads, in the form
of the functions

  > unsafeLiftTcM :: TcM a -> m a

  > unsafeWithRunInTcM :: ( ( forall a. m a -> TcM a ) -> TcM b ) -> m b

Here 'GHC.Tc.TcM' is GHC's internal type-checker monad.

It also exposes extra environment available in the solving/rewriting stages:

  > askRewriteEnv :: TcPluginM Rewrite RewriteEnv

  > askEvBinds :: TcPluginM Solve EvBindsVar

It is hoped that none of these internal operations are necessary, and that users
can fulfill their needs without importing this internal module.

Please file a bug on the issue tracker if you have encountered a situation
which requires the import of this module.

-}

module GHC.TcPlugin.API.Internal
  ( -- * Internal functions and types
    MonadTcPlugin(..), MonadTcPluginWork
  , unsafeLiftThroughTcM
    -- * Re-exported functions and types
  , TcPlugin(..), TcPluginStage(..)
  , TcPluginSolver
  , TcPluginM(..)
  , TcPluginErrorMessage(..)
  , TcPluginRewriter
  , MonadThings(..)
  , askRewriteEnv
  , askDeriveds
  , askEvBinds
  , mkTcPlugin
  , mkTcPluginErrorTy
  )
  where

-- base
import Data.Coerce
  ( Coercible )
import Data.Kind
  ( Type )
import GHC.TypeLits
  ( TypeError, ErrorMessage(..) )

-- transformers
import Control.Monad.Trans.Reader
  ( ReaderT(..) )

-- ghc
import qualified GHC.Builtin.Names
  as GHC.TypeLits
    ( errorMessageTypeErrorFamName
    , typeErrorTextDataConName
    , typeErrorAppendDataConName
    , typeErrorVAppendDataConName
    , typeErrorShowTypeDataConName
    )
import qualified GHC.Builtin.Types
  as GHC
    ( constraintKind )
import qualified GHC.Core.DataCon
  as GHC
    ( promoteDataCon )
import qualified GHC.Core.TyCon
  as GHC
    ( TyCon )
import qualified GHC.Core.TyCo.Rep
  as GHC
    ( PredType, Type(..), TyLit(..) )
import qualified GHC.Core.Type
  as GHC
    ( mkTyConApp, tcTypeKind )
import qualified GHC.Data.FastString
  as GHC
    ( fsLit )
import qualified GHC.Tc.Plugin
  as GHC
    ( tcLookupDataCon, tcLookupTyCon )
import qualified GHC.Tc.Types
  as GHC
    ( TcM, TcPlugin(..), TcPluginM
    , TcPluginSolver
#ifdef HAS_REWRITING
    , TcPluginRewriter
#else
    , getEvBindsTcPluginM
#endif
    , runTcPluginM, unsafeTcPluginTcM
    )
#ifdef HAS_REWRITING
import GHC.Tc.Types
    ( TcPluginSolveResult
    , TcPluginRewriteResult
    , RewriteEnv
    )
#endif
import qualified GHC.Tc.Types.Constraint
  as GHC
    ( Ct )
import qualified GHC.Tc.Types.Evidence
  as GHC
    ( EvBindsVar )
import qualified GHC.Types.Unique.FM
  as GHC
    ( UniqFM )
#if MIN_VERSION_ghc(9,1,0)
import GHC.Types.TyThing
  ( MonadThings(..) )
#else
import GHC.Driver.Types
  ( MonadThings(..) )
#endif

-- ghc-tcplugin-api
#ifndef HAS_REWRITING
import GHC.TcPlugin.API.Internal.Shim
  ( TcPluginSolveResult, TcPluginRewriteResult(..)
  , RewriteEnv
  , shimRewriter
  )
#endif

--------------------------------------------------------------------------------
-- Public types and functions.

-- | Stage of a type-checking plugin, used as a data kind.
data TcPluginStage
  = Init
  | Solve
  | Rewrite
  | Stop

-- | The @solve@ function of a type-checking plugin takes in Given and Wanted
-- constraints, and should return a 'GHC.Tc.Types.TcPluginSolveResult'
-- indicating which Wanted constraints it could solve, or whether any are
-- insoluble.
type TcPluginSolver
  =  [GHC.Ct] -- ^ Givens
  -> [GHC.Ct] -- ^ Wanteds
  -> TcPluginM Solve TcPluginSolveResult

-- | For rewriting type family applications, a type-checking plugin provides
-- a function of this type for each type family 'GHC.Core.TyCon.TyCon'.
--
-- The function is provided with the current set of Given constraints, together
-- with the arguments to the type family.
-- The type family application will always be fully saturated.
type TcPluginRewriter
  =  [GHC.Ct]     -- ^ Givens
  -> [GHC.Type]   -- ^ Type family arguments (saturated)
  -> TcPluginM Rewrite TcPluginRewriteResult

-- | A record containing all the stages necessary for the
-- operation of a type-checking plugin, as defined in this API.
--
-- __Note__: this is not the same record as GHC's built-in
-- 'GHC.Tc.Types.TcPlugin' record. Use 'mkTcPlugin' for the conversion.
--
-- To create a type-checking plugin, define something of this type
-- and then call 'mkTcPlugin' on the result.
-- This will return something that can be passed to 'GHC.Plugins.Plugin':
--
-- > plugin :: GHC.Plugins.Plugin
-- > plugin =
-- >   GHC.Plugins.defaultPlugin
-- >     { GHC.Plugins.tcPlugin =
-- >         \ args -> Just $
-- >            GHC.TcPlugin.API.mkTcPlugin ( myTcPlugin args )
-- >     }
-- >
-- > myTcPlugin :: [String] -> GHC.TcPlugin.API.TcPlugin
-- > myTcPlugin args = ...
data TcPlugin = forall s. TcPlugin
  { ()
tcPluginInit :: TcPluginM Init s
      -- ^ Initialise plugin, when entering type-checker.

  , ()
tcPluginSolve :: s -> TcPluginSolver
      -- ^ Solve some constraints.
      --
      -- This function will be invoked at two points in the constraint solving
      -- process: once to manipulate given constraints, and once to solve
      -- wanted constraints. In the first case (and only in the first case),
      -- no wanted constraints will be passed to the plugin.
      --
      -- The plugin can either return a contradiction,
      -- or specify that it has solved some constraints (with evidence),
      -- and possibly emit additional wanted constraints.
      --
      -- Use @ \\ _ _ _ -> pure $ TcPluginOK [] [] @ if your plugin
      -- does not provide this functionality.

  , ()
tcPluginRewrite
      :: s -> GHC.UniqFM
#if MIN_VERSION_ghc(9,0,0)
                GHC.TyCon
#endif
                TcPluginRewriter
    -- ^ Rewrite saturated type family applications.
    --
    -- The plugin is expected to supply a mapping from type family names to
    -- rewriting functions. For each type family 'GHC.Core.TyCon.TyCon',
    -- the plugin should provide a function which takes in the given constraints
    -- and arguments of a saturated type family application, and return
    -- a possible rewriting.
    -- See 'TcPluginRewriter' for the expected shape of such a function.
    --
    -- Use @ const emptyUFM @ if your plugin does not provide this functionality.

  , ()
tcPluginStop :: s -> TcPluginM Stop ()
   -- ^ Clean up after the plugin, when exiting the type-checker.
  }

-- | The monad used for a type-checker plugin, parametrised by
-- the 'TcPluginStage' of the plugin.
data family TcPluginM (s :: TcPluginStage) :: Type -> Type
newtype instance TcPluginM Init a =
  TcPluginInitM { forall a. TcPluginM 'Init a -> TcPluginM a
tcPluginInitM :: GHC.TcPluginM a }
  deriving newtype ( forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a
forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a
$c<$ :: forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a
fmap :: forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
Functor, Functor (TcPluginM 'Init)
forall a. a -> TcPluginM 'Init a
forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall a b c.
(a -> b -> c)
-> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
$c<* :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
*> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
$c*> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c
<*> :: forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
$c<*> :: forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
pure :: forall a. a -> TcPluginM 'Init a
$cpure :: forall a. a -> TcPluginM 'Init a
Applicative, Applicative (TcPluginM 'Init)
forall a. a -> TcPluginM 'Init a
forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TcPluginM 'Init a
$creturn :: forall a. a -> TcPluginM 'Init a
>> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
$c>> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
>>= :: forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
$c>>= :: forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
Monad )
#ifdef HAS_DERIVEDS
newtype instance TcPluginM Solve a =
  TcPluginSolveM { forall a.
TcPluginM 'Solve a
-> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> [GHC.Ct] -> GHC.TcPluginM a }
  deriving ( forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
$c<$ :: forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
fmap :: forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
Functor, Functor (TcPluginM 'Solve)
forall a. a -> TcPluginM 'Solve a
forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
forall a b.
TcPluginM 'Solve (a -> b)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b
forall a b c.
(a -> b -> c)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
$c<* :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
*> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
$c*> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c
<*> :: forall a b.
TcPluginM 'Solve (a -> b)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b
$c<*> :: forall a b.
TcPluginM 'Solve (a -> b)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b
pure :: forall a. a -> TcPluginM 'Solve a
$cpure :: forall a. a -> TcPluginM 'Solve a
Applicative, Applicative (TcPluginM 'Solve)
forall a. a -> TcPluginM 'Solve a
forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
forall a b.
TcPluginM 'Solve a
-> (a -> TcPluginM 'Solve b) -> TcPluginM 'Solve b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TcPluginM 'Solve a
$creturn :: forall a. a -> TcPluginM 'Solve a
>> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
$c>> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
>>= :: forall a b.
TcPluginM 'Solve a
-> (a -> TcPluginM 'Solve b) -> TcPluginM 'Solve b
$c>>= :: forall a b.
TcPluginM 'Solve a
-> (a -> TcPluginM 'Solve b) -> TcPluginM 'Solve b
Monad )
    via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar ( ReaderT [GHC.Ct] GHC.TcPluginM ) ) )
#else
newtype instance TcPluginM Solve a =
  TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> GHC.TcPluginM a }
  deriving ( Functor, Applicative, Monad )
    via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar GHC.TcPluginM ) )
#endif
newtype instance TcPluginM Rewrite a =
  TcPluginRewriteM { forall a.
TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM :: BuiltinDefs -> RewriteEnv -> GHC.TcPluginM a }
  deriving ( forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
forall a b.
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
$c<$ :: forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
fmap :: forall a b.
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
$cfmap :: forall a b.
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
Functor, Functor (TcPluginM 'Rewrite)
forall a. a -> TcPluginM 'Rewrite a
forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
forall a b.
TcPluginM 'Rewrite (a -> b)
-> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
forall a b c.
(a -> b -> c)
-> TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b
-> TcPluginM 'Rewrite c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
$c<* :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
*> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
$c*> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b
-> TcPluginM 'Rewrite c
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b
-> TcPluginM 'Rewrite c
<*> :: forall a b.
TcPluginM 'Rewrite (a -> b)
-> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
$c<*> :: forall a b.
TcPluginM 'Rewrite (a -> b)
-> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
pure :: forall a. a -> TcPluginM 'Rewrite a
$cpure :: forall a. a -> TcPluginM 'Rewrite a
Applicative, Applicative (TcPluginM 'Rewrite)
forall a. a -> TcPluginM 'Rewrite a
forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
forall a b.
TcPluginM 'Rewrite a
-> (a -> TcPluginM 'Rewrite b) -> TcPluginM 'Rewrite b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TcPluginM 'Rewrite a
$creturn :: forall a. a -> TcPluginM 'Rewrite a
>> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
$c>> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
>>= :: forall a b.
TcPluginM 'Rewrite a
-> (a -> TcPluginM 'Rewrite b) -> TcPluginM 'Rewrite b
$c>>= :: forall a b.
TcPluginM 'Rewrite a
-> (a -> TcPluginM 'Rewrite b) -> TcPluginM 'Rewrite b
Monad )
    via ( ReaderT BuiltinDefs ( ReaderT RewriteEnv GHC.TcPluginM ) )
newtype instance TcPluginM Stop a =
  TcPluginStopM { forall a. TcPluginM 'Stop a -> TcPluginM a
tcPluginStopM :: GHC.TcPluginM a }
  deriving newtype ( forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
$c<$ :: forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
fmap :: forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
Functor, Functor (TcPluginM 'Stop)
forall a. a -> TcPluginM 'Stop a
forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
forall a b.
TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
forall a b c.
(a -> b -> c)
-> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
$c<* :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
*> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
$c*> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c
<*> :: forall a b.
TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
$c<*> :: forall a b.
TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
pure :: forall a. a -> TcPluginM 'Stop a
$cpure :: forall a. a -> TcPluginM 'Stop a
Applicative, Applicative (TcPluginM 'Stop)
forall a. a -> TcPluginM 'Stop a
forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
forall a b.
TcPluginM 'Stop a -> (a -> TcPluginM 'Stop b) -> TcPluginM 'Stop b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TcPluginM 'Stop a
$creturn :: forall a. a -> TcPluginM 'Stop a
>> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
$c>> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
>>= :: forall a b.
TcPluginM 'Stop a -> (a -> TcPluginM 'Stop b) -> TcPluginM 'Stop b
$c>>= :: forall a b.
TcPluginM 'Stop a -> (a -> TcPluginM 'Stop b) -> TcPluginM 'Stop b
Monad )

-- | Ask for the evidence currently gathered by the type-checker.
--
-- Only available in the solver part of the type-checking plugin.
askEvBinds :: TcPluginM Solve GHC.EvBindsVar
askEvBinds :: TcPluginM 'Solve EvBindsVar
askEvBinds = forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
  \ BuiltinDefs
_defs
    EvBindsVar
evBinds
#ifdef HAS_DERIVEDS
    [Ct]
_deriveds
#endif
  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure EvBindsVar
evBinds

-- | Ask for the Derived constraints that the solver was provided with.
--
-- Always returns the empty list on GHC 9.4 or above.
askDeriveds :: TcPluginM Solve [GHC.Ct]
askDeriveds :: TcPluginM 'Solve [Ct]
askDeriveds =
#ifdef HAS_DERIVEDS
  forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM \ BuiltinDefs
_defs EvBindsVar
_evBinds [Ct]
deriveds -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Ct]
deriveds
#else
  pure []
#endif

-- | Ask for the current rewriting environment.
--
-- Only available in the rewriter part of the type-checking plugin.
askRewriteEnv :: TcPluginM Rewrite RewriteEnv
askRewriteEnv :: TcPluginM 'Rewrite RewriteEnv
askRewriteEnv = forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM ( \ BuiltinDefs
_ RewriteEnv
rewriteEnv -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RewriteEnv
rewriteEnv )

-- | A 'MonadTcPlugin' is essentially a reader monad over GHC's 'GHC.Tc.TcM' monad.
--
-- This means we have both a @lift@ and an @unlift@ operation,
-- similar to @MonadUnliftIO@ or @MonadBaseControl@.
--
-- See for instance 'unsafeLiftThroughTcM', which is an example of function that
-- one would not be able to write using only a @lift@ operation.
--
-- Note that you must import the internal module in order to access the methods.
-- Please report a bug if you find yourself needing this functionality.
class ( Monad m, ( forall x y. Coercible x y => Coercible (m x) (m y) ) ) => MonadTcPlugin (m :: Type -> Type) where

  {-# MINIMAL liftTcPluginM, unsafeWithRunInTcM #-}

  -- N.B.: these methods are not re-exported from the main module.

  -- | Lift a computation from GHC's 'GHC.TcPluginM' monad.
  liftTcPluginM :: GHC.TcPluginM a -> m a

  -- | Lift a computation from the 'GHC.Tc.TcM' monad.
  unsafeLiftTcM :: GHC.TcM a -> m a
  unsafeLiftTcM = forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM

  -- | Unlift a computation from the 'GHC.Tc.TcM' monad.
  --
  -- If this type signature seems confusing, I recommend reading Alexis King's
  -- excellent blog post on @MonadBaseControl@:
  --
  -- <https://lexi-lambda.github.io/blog/2019/09/07/demystifying-monadbasecontrol/ Demystifying MonadBaseControl>
  unsafeWithRunInTcM :: ( ( forall a. m a -> GHC.TcM a ) -> GHC.TcM b ) -> m b

instance MonadTcPlugin ( TcPluginM Init ) where
  liftTcPluginM :: forall a. TcPluginM a -> TcPluginM 'Init a
liftTcPluginM = forall a. TcPluginM a -> TcPluginM 'Init a
TcPluginInitM
  unsafeWithRunInTcM :: forall b.
((forall a. TcPluginM 'Init a -> TcM a) -> TcM b)
-> TcPluginM 'Init b
unsafeWithRunInTcM (forall a. TcPluginM 'Init a -> TcM a) -> TcM b
runInTcM
    = forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Init a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
      ( GHC.runTcPluginM . tcPluginInitM )
#else
      ( ( forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` ( forall a. HasCallStack => [Char] -> a
error [Char]
"tcPluginInit: cannot access EvBindsVar" ) ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TcPluginM 'Init a -> TcPluginM a
tcPluginInitM )
#endif
instance MonadTcPlugin ( TcPluginM Solve ) where
  liftTcPluginM :: forall a. TcPluginM a -> TcPluginM 'Solve a
liftTcPluginM  = forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
#ifdef HAS_DERIVEDS
                 forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ TcPluginM a
ma BuiltinDefs
_defs EvBindsVar
_evBinds [Ct]
_deriveds -> TcPluginM a
ma )
#else
                 . ( \ ma _defs _evBinds -> ma )
#endif
  unsafeWithRunInTcM :: forall b.
((forall a. TcPluginM 'Solve a -> TcM a) -> TcM b)
-> TcPluginM 'Solve b
unsafeWithRunInTcM (forall a. TcPluginM 'Solve a -> TcM a) -> TcM b
runInTcM
    = forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
      \ BuiltinDefs
builtinDefs
        EvBindsVar
evBinds
#ifdef HAS_DERIVEDS
        [Ct]
deriveds
#endif
      ->
        forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Solve a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
  -- (no deriveds)
          ( GHC.runTcPluginM
          . ( \ f -> f builtinDefs evBinds )
          . tcPluginSolveM )
#else
          ( ( forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` EvBindsVar
evBinds )
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
f -> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
f BuiltinDefs
builtinDefs EvBindsVar
evBinds [Ct]
deriveds )
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
TcPluginM 'Solve a
-> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
tcPluginSolveM
          )
#endif
instance MonadTcPlugin ( TcPluginM Rewrite ) where
  liftTcPluginM :: forall a. TcPluginM a -> TcPluginM 'Rewrite a
liftTcPluginM = forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ TcPluginM a
ma BuiltinDefs
_ RewriteEnv
_ -> TcPluginM a
ma )
  unsafeWithRunInTcM :: forall b.
((forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b)
-> TcPluginM 'Rewrite b
unsafeWithRunInTcM (forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b
runInTcM
    = forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM \ BuiltinDefs
builtinDefs RewriteEnv
rewriteEnv ->
      forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
        ( GHC.runTcPluginM
#else
        ( ( forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` ( forall a. HasCallStack => [Char] -> a
error [Char]
"tcPluginRewrite: cannot access EvBindsVar" ) )
#endif
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ BuiltinDefs -> RewriteEnv -> TcPluginM a
f -> BuiltinDefs -> RewriteEnv -> TcPluginM a
f BuiltinDefs
builtinDefs RewriteEnv
rewriteEnv )
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM )
instance MonadTcPlugin ( TcPluginM Stop ) where
  liftTcPluginM :: forall a. TcPluginM a -> TcPluginM 'Stop a
liftTcPluginM = forall a. TcPluginM a -> TcPluginM 'Stop a
TcPluginStopM
  unsafeWithRunInTcM :: forall b.
((forall a. TcPluginM 'Stop a -> TcM a) -> TcM b)
-> TcPluginM 'Stop b
unsafeWithRunInTcM (forall a. TcPluginM 'Stop a -> TcM a) -> TcM b
runInTcM
    = forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Stop a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
      ( GHC.runTcPluginM . tcPluginStopM )
#else
      ( ( forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` ( forall a. HasCallStack => [Char] -> a
error [Char]
"tcPluginStop: cannot access EvBindsVar" ) ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TcPluginM 'Stop a -> TcPluginM a
tcPluginStopM )
#endif

-- | Take a function whose argument and result types are both within the 'GHC.Tc.TcM' monad,
-- and return a function that works within a type-checking plugin monad.
--
-- Please report a bug if you find yourself needing to use this function.
unsafeLiftThroughTcM :: MonadTcPlugin m => ( GHC.TcM a -> GHC.TcM b ) -> m a -> m b
unsafeLiftThroughTcM :: forall (m :: * -> *) a b.
MonadTcPlugin m =>
(TcM a -> TcM b) -> m a -> m b
unsafeLiftThroughTcM TcM a -> TcM b
f m a
ma = forall (m :: * -> *) b.
MonadTcPlugin m =>
((forall a. m a -> TcM a) -> TcM b) -> m b
unsafeWithRunInTcM \ forall a. m a -> TcM a
runInTcM -> TcM a -> TcM b
f ( forall a. m a -> TcM a
runInTcM m a
ma )

-- | Use this function to create a type-checker plugin to pass to GHC.
mkTcPlugin
  :: TcPlugin     -- ^ type-checking plugin written with this library
  -> GHC.TcPlugin -- ^ type-checking plugin for GHC
mkTcPlugin :: TcPlugin -> TcPlugin
mkTcPlugin ( TcPlugin
              { tcPluginInit :: ()
tcPluginInit = TcPluginM 'Init s
tcPluginInit :: TcPluginM Init userDefs
              , s -> TcPluginSolver
tcPluginSolve :: s -> TcPluginSolver
tcPluginSolve :: ()
tcPluginSolve
              , s -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite :: ()
tcPluginRewrite
              , s -> TcPluginM 'Stop ()
tcPluginStop :: s -> TcPluginM 'Stop ()
tcPluginStop :: ()
tcPluginStop
              }
           ) =
  GHC.TcPlugin
    { tcPluginInit :: TcPluginM (TcPluginDefs s)
GHC.tcPluginInit    = TcPluginM 'Init s -> TcPluginM (TcPluginDefs s)
adaptUserInit    TcPluginM 'Init s
tcPluginInit
#ifdef HAS_REWRITING
    , GHC.tcPluginSolve   = adaptUserSolve   tcPluginSolve
    , GHC.tcPluginRewrite = adaptUserRewrite tcPluginRewrite
#else
    , tcPluginSolve :: TcPluginDefs s -> TcPluginSolver
GHC.tcPluginSolve   = (s -> TcPluginSolver)
-> (s -> UniqFM TyCon TcPluginRewriter)
-> TcPluginDefs s
-> TcPluginSolver
adaptUserSolveAndRewrite
                              s -> TcPluginSolver
tcPluginSolve s -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite
#endif
    , tcPluginStop :: TcPluginDefs s -> TcPluginM ()
GHC.tcPluginStop    = (s -> TcPluginM 'Stop ()) -> TcPluginDefs s -> TcPluginM ()
adaptUserStop    s -> TcPluginM 'Stop ()
tcPluginStop
    }
  where
    adaptUserInit :: TcPluginM Init userDefs -> GHC.TcPluginM ( TcPluginDefs userDefs )
    adaptUserInit :: TcPluginM 'Init s -> TcPluginM (TcPluginDefs s)
adaptUserInit TcPluginM 'Init s
userInit = do
      BuiltinDefs
tcPluginBuiltinDefs <- TcPluginM BuiltinDefs
initBuiltinDefs
      s
tcPluginUserDefs    <- forall a. TcPluginM 'Init a -> TcPluginM a
tcPluginInitM TcPluginM 'Init s
userInit
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ( TcPluginDefs { BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs, s
tcPluginUserDefs :: s
tcPluginUserDefs :: s
tcPluginUserDefs })

#ifdef HAS_REWRITING
  -- (no deriveds)
    adaptUserSolve :: ( userDefs -> TcPluginSolver )
                   -> TcPluginDefs userDefs
                   -> GHC.TcPluginSolver
    adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )
      = \ evBindsVar givens wanteds -> do
        tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds )
          tcPluginBuiltinDefs evBindsVar
    adaptUserRewrite :: ( userDefs -> GHC.UniqFM GHC.TyCon TcPluginRewriter )
                     -> TcPluginDefs userDefs -> GHC.UniqFM GHC.TyCon GHC.TcPluginRewriter
    adaptUserRewrite userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs })
      = fmap
          ( \ userRewriter rewriteEnv givens tys ->
            tcPluginRewriteM ( userRewriter givens tys ) tcPluginBuiltinDefs rewriteEnv
          )
          ( userRewrite tcPluginUserDefs )
#else
    adaptUserSolveAndRewrite
      :: ( userDefs -> TcPluginSolver )
      -> ( userDefs -> GHC.UniqFM
#if MIN_VERSION_ghc(9,0,0)
                         GHC.TyCon
#endif
                         TcPluginRewriter
         )
      -> TcPluginDefs userDefs
      -> GHC.TcPluginSolver
    adaptUserSolveAndRewrite :: (s -> TcPluginSolver)
-> (s -> UniqFM TyCon TcPluginRewriter)
-> TcPluginDefs s
-> TcPluginSolver
adaptUserSolveAndRewrite s -> TcPluginSolver
userSolve s -> UniqFM TyCon TcPluginRewriter
userRewrite ( TcPluginDefs { s
tcPluginUserDefs :: s
tcPluginUserDefs :: forall s. TcPluginDefs s -> s
tcPluginUserDefs, BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs :: forall s. TcPluginDefs s -> BuiltinDefs
tcPluginBuiltinDefs } )
      = \ [Ct]
givens [Ct]
deriveds [Ct]
wanteds -> do
        EvBindsVar
evBindsVar <- TcPluginM EvBindsVar
GHC.getEvBindsTcPluginM
        [Ct]
-> [Ct]
-> [Ct]
-> Rewriters
-> ([Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult)
-> TcPluginM TcPluginResult
shimRewriter
          [Ct]
givens [Ct]
deriveds [Ct]
wanteds
          ( forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
              ( \ TcPluginRewriter
userRewriter RewriteEnv
rewriteEnv [Ct]
gs [Type]
tys ->
                forall a.
TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM ( TcPluginRewriter
userRewriter [Ct]
gs [Type]
tys )
                  BuiltinDefs
tcPluginBuiltinDefs RewriteEnv
rewriteEnv
              )
              ( s -> UniqFM TyCon TcPluginRewriter
userRewrite s
tcPluginUserDefs )
          )
          ( \ [Ct]
gs [Ct]
ds [Ct]
ws ->
            forall a.
TcPluginM 'Solve a
-> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
tcPluginSolveM ( s -> TcPluginSolver
userSolve s
tcPluginUserDefs [Ct]
gs [Ct]
ws )
              BuiltinDefs
tcPluginBuiltinDefs EvBindsVar
evBindsVar [Ct]
ds
          )
#endif

    adaptUserStop :: ( userDefs -> TcPluginM Stop () ) -> TcPluginDefs userDefs -> GHC.TcPluginM ()
    adaptUserStop :: (s -> TcPluginM 'Stop ()) -> TcPluginDefs s -> TcPluginM ()
adaptUserStop s -> TcPluginM 'Stop ()
userStop ( TcPluginDefs { s
tcPluginUserDefs :: s
tcPluginUserDefs :: forall s. TcPluginDefs s -> s
tcPluginUserDefs } ) =
      forall a. TcPluginM 'Stop a -> TcPluginM a
tcPluginStopM forall a b. (a -> b) -> a -> b
$ s -> TcPluginM 'Stop ()
userStop s
tcPluginUserDefs

-- | Monads for type-checking plugins which are able to emit new constraints
-- and throw errors.
--
-- These operations are supported by the monads that 'tcPluginSolve'
-- and 'tcPluginRewrite' use; it is not possible to emit work or
-- throw type errors in 'tcPluginInit' or 'tcPluginStop'.
--
-- See 'mkTcPluginErrorTy' and 'GHC.TcPlugin.API.emitWork' for functions
-- which require this typeclass.
class MonadTcPlugin m => MonadTcPluginWork m where
  {-# MINIMAL #-} -- to avoid the methods appearing in the haddocks
  askBuiltins :: m BuiltinDefs
  askBuiltins = forall a. HasCallStack => [Char] -> a
error [Char]
"askBuiltins: no default implementation"
instance MonadTcPluginWork ( TcPluginM Solve ) where
  askBuiltins :: TcPluginM 'Solve BuiltinDefs
askBuiltins = forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
    \ BuiltinDefs
builtinDefs
      EvBindsVar
_evBinds
#ifdef HAS_DERIVEDS
      [Ct]
_deriveds
#endif
    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure BuiltinDefs
builtinDefs
instance MonadTcPluginWork ( TcPluginM Rewrite ) where
  askBuiltins :: TcPluginM 'Rewrite BuiltinDefs
askBuiltins = forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM \ BuiltinDefs
builtinDefs RewriteEnv
_evBinds -> forall (f :: * -> *) a. Applicative f => a -> f a
pure BuiltinDefs
builtinDefs

instance TypeError ( 'Text "Cannot emit new work in 'tcPluginInit'." )
      => MonadTcPluginWork ( TcPluginM Init ) where
  askBuiltins :: TcPluginM 'Init BuiltinDefs
askBuiltins = forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot emit new work in 'tcPluginInit'."
instance TypeError ( 'Text "Cannot emit new work in 'tcPluginStop'." )
      => MonadTcPluginWork ( TcPluginM Stop ) where
  askBuiltins :: TcPluginM 'Stop BuiltinDefs
askBuiltins = forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot emit new work in 'tcPluginStop'."

-- | Use this type like 'GHC.TypeLits.ErrorMessage' to write an error message.
-- This error message can then be thrown at the type-level by the plugin,
-- by emitting a wanted constraint whose predicate is obtained from 'mkTcPluginErrorTy'.
--
-- A 'GHC.Tc.Types.Constraint.CtLoc' will still need to be provided in order to inform GHC of the
-- origin of the error (e.g.: which part of the source code should be
-- highlighted?). See 'GHC.TcPlugin.API.setCtLocM'.
data TcPluginErrorMessage
  = Txt !String
  -- ^ Show the text as is.
  | PrintType !GHC.Type
  -- ^ Pretty print the given type.
  | (:|:) !TcPluginErrorMessage !TcPluginErrorMessage
  -- ^ Put two messages side by side.
  | (:-:) !TcPluginErrorMessage !TcPluginErrorMessage
  -- ^ Stack two messages vertically.
infixl 5 :|:
infixl 6 :-:

-- | Create an error type with the desired error message.
--
-- The result can be paired with a 'GHC.Tc.Types.Constraint.CtLoc' in order to throw a type error,
-- for instance by using 'GHC.TcPlugin.API.newWanted'.
mkTcPluginErrorTy :: MonadTcPluginWork m => TcPluginErrorMessage -> m GHC.PredType
mkTcPluginErrorTy :: forall (m :: * -> *).
MonadTcPluginWork m =>
TcPluginErrorMessage -> m Type
mkTcPluginErrorTy TcPluginErrorMessage
msg = do
  builtinDefs :: BuiltinDefs
builtinDefs@( BuiltinDefs { TyCon
typeErrorTyCon :: BuiltinDefs -> TyCon
typeErrorTyCon :: TyCon
typeErrorTyCon } ) <- forall (m :: * -> *). MonadTcPluginWork m => m BuiltinDefs
askBuiltins
  let
    errorMsgTy :: GHC.PredType
    errorMsgTy :: Type
errorMsgTy = BuiltinDefs -> TcPluginErrorMessage -> Type
interpretErrorMessage BuiltinDefs
builtinDefs TcPluginErrorMessage
msg
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
typeErrorTyCon [ Type
GHC.constraintKind, Type
errorMsgTy ]

instance ( Monad (TcPluginM s), MonadTcPlugin (TcPluginM s) )
      => MonadThings (TcPluginM s) where
  lookupThing :: Name -> TcPluginM s TyThing
lookupThing = forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadThings m => Name -> m TyThing
lookupThing

--------------------------------------------------------------------------------
-- Private types and functions.
-- Not exposed at all, even from the internal module.

data BuiltinDefs =
  BuiltinDefs
    { BuiltinDefs -> TyCon
typeErrorTyCon :: !GHC.TyCon
    , BuiltinDefs -> TyCon
textTyCon      :: !GHC.TyCon
    , BuiltinDefs -> TyCon
showTypeTyCon  :: !GHC.TyCon
    , BuiltinDefs -> TyCon
concatTyCon    :: !GHC.TyCon
    , BuiltinDefs -> TyCon
vcatTyCon      :: !GHC.TyCon
    }

data TcPluginDefs s
  = TcPluginDefs
  { forall s. TcPluginDefs s -> BuiltinDefs
tcPluginBuiltinDefs :: !BuiltinDefs
  , forall s. TcPluginDefs s -> s
tcPluginUserDefs    :: !s
  }

initBuiltinDefs :: GHC.TcPluginM BuiltinDefs
initBuiltinDefs :: TcPluginM BuiltinDefs
initBuiltinDefs = do
  TyCon
typeErrorTyCon  <-                        Name -> TcPluginM TyCon
GHC.tcLookupTyCon   Name
GHC.TypeLits.errorMessageTypeErrorFamName
  TyCon
textTyCon       <- DataCon -> TyCon
GHC.promoteDataCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM DataCon
GHC.tcLookupDataCon Name
GHC.TypeLits.typeErrorTextDataConName
  TyCon
showTypeTyCon   <- DataCon -> TyCon
GHC.promoteDataCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM DataCon
GHC.tcLookupDataCon Name
GHC.TypeLits.typeErrorShowTypeDataConName
  TyCon
concatTyCon     <- DataCon -> TyCon
GHC.promoteDataCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM DataCon
GHC.tcLookupDataCon Name
GHC.TypeLits.typeErrorAppendDataConName
  TyCon
vcatTyCon       <- DataCon -> TyCon
GHC.promoteDataCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM DataCon
GHC.tcLookupDataCon Name
GHC.TypeLits.typeErrorVAppendDataConName
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( BuiltinDefs { TyCon
vcatTyCon :: TyCon
concatTyCon :: TyCon
showTypeTyCon :: TyCon
textTyCon :: TyCon
typeErrorTyCon :: TyCon
vcatTyCon :: TyCon
concatTyCon :: TyCon
showTypeTyCon :: TyCon
textTyCon :: TyCon
typeErrorTyCon :: TyCon
.. } )

interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> GHC.PredType
interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> Type
interpretErrorMessage ( BuiltinDefs { TyCon
vcatTyCon :: TyCon
concatTyCon :: TyCon
showTypeTyCon :: TyCon
textTyCon :: TyCon
typeErrorTyCon :: TyCon
vcatTyCon :: BuiltinDefs -> TyCon
concatTyCon :: BuiltinDefs -> TyCon
showTypeTyCon :: BuiltinDefs -> TyCon
textTyCon :: BuiltinDefs -> TyCon
typeErrorTyCon :: BuiltinDefs -> TyCon
.. } ) = TcPluginErrorMessage -> Type
go
  where
    go :: TcPluginErrorMessage -> GHC.PredType
    go :: TcPluginErrorMessage -> Type
go ( Txt [Char]
str ) =
      TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
textTyCon [ TyLit -> Type
GHC.LitTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. FastString -> TyLit
GHC.StrTyLit forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> FastString
GHC.fsLit forall a b. (a -> b) -> a -> b
$ [Char]
str ]
    go ( PrintType Type
ty ) =
      TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
showTypeTyCon [ HasDebugCallStack => Type -> Type
GHC.tcTypeKind Type
ty, Type
ty ]
        -- The kind gets ignored by GHC when printing the error message (see GHC.Core.Type.pprUserTypeErrorTy).
        -- However, including the wrong kind can lead to ASSERT failures, so we compute the kind and pass it.
    go ( TcPluginErrorMessage
msg1 :|: TcPluginErrorMessage
msg2 ) =
      TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
concatTyCon [ TcPluginErrorMessage -> Type
go TcPluginErrorMessage
msg1, TcPluginErrorMessage -> Type
go TcPluginErrorMessage
msg2 ]
    go ( TcPluginErrorMessage
msg1 :-: TcPluginErrorMessage
msg2 ) =
      TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
vcatTyCon [ TcPluginErrorMessage -> Type
go TcPluginErrorMessage
msg1, TcPluginErrorMessage -> Type
go TcPluginErrorMessage
msg2 ]