{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# 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
  , 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 )

-- 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 { TcPluginM 'Init a -> TcPluginM a
tcPluginInitM :: GHC.TcPluginM a }
  deriving newtype ( a -> TcPluginM 'Init b -> TcPluginM 'Init a
(a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
(forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b)
-> (forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a)
-> Functor (TcPluginM 'Init)
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
<$ :: a -> TcPluginM 'Init b -> TcPluginM 'Init a
$c<$ :: forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a
fmap :: (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
Functor, Functor (TcPluginM 'Init)
a -> TcPluginM 'Init a
Functor (TcPluginM 'Init)
-> (forall a. a -> TcPluginM 'Init a)
-> (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 a b.
    TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b)
-> (forall a b.
    TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a)
-> Applicative (TcPluginM 'Init)
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
(a -> b -> c)
-> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c
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
<* :: TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
$c<* :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
*> :: TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
$c*> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
liftA2 :: (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
<*> :: 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 :: a -> TcPluginM 'Init a
$cpure :: forall a. a -> TcPluginM 'Init a
$cp1Applicative :: Functor (TcPluginM 'Init)
Applicative, Applicative (TcPluginM 'Init)
a -> TcPluginM 'Init a
Applicative (TcPluginM 'Init)
-> (forall a b.
    TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b)
-> (forall a b.
    TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b)
-> (forall a. a -> TcPluginM 'Init a)
-> Monad (TcPluginM 'Init)
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
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 :: a -> TcPluginM 'Init a
$creturn :: forall a. a -> TcPluginM 'Init a
>> :: TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
$c>> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init 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
$cp1Monad :: Applicative (TcPluginM 'Init)
Monad )
#ifdef HAS_DERIVEDS
newtype instance TcPluginM Solve a =
  TcPluginSolveM { TcPluginM 'Solve a
-> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> [GHC.Ct] -> GHC.TcPluginM a }
  deriving ( a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
(a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
(forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b)
-> (forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a)
-> Functor (TcPluginM 'Solve)
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
<$ :: a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
$c<$ :: forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
fmap :: (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
Functor, Functor (TcPluginM 'Solve)
a -> TcPluginM 'Solve a
Functor (TcPluginM 'Solve)
-> (forall a. a -> TcPluginM 'Solve a)
-> (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 a b.
    TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b)
-> (forall a b.
    TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a)
-> Applicative (TcPluginM 'Solve)
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
TcPluginM 'Solve (a -> b)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b
(a -> b -> c)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c
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
<* :: TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
$c<* :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
*> :: TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
$c*> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
liftA2 :: (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
<*> :: 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 :: a -> TcPluginM 'Solve a
$cpure :: forall a. a -> TcPluginM 'Solve a
$cp1Applicative :: Functor (TcPluginM 'Solve)
Applicative, Applicative (TcPluginM 'Solve)
a -> TcPluginM 'Solve a
Applicative (TcPluginM 'Solve)
-> (forall a b.
    TcPluginM 'Solve a
    -> (a -> TcPluginM 'Solve b) -> TcPluginM 'Solve b)
-> (forall a b.
    TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b)
-> (forall a. a -> TcPluginM 'Solve a)
-> Monad (TcPluginM 'Solve)
TcPluginM 'Solve a
-> (a -> TcPluginM 'Solve b) -> TcPluginM 'Solve b
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
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 :: a -> TcPluginM 'Solve a
$creturn :: forall a. a -> TcPluginM 'Solve a
>> :: TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
$c>> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve 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
$cp1Monad :: Applicative (TcPluginM 'Solve)
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 { TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM :: BuiltinDefs -> RewriteEnv -> GHC.TcPluginM a }
  deriving ( a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
(forall a b.
 (a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b)
-> (forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a)
-> Functor (TcPluginM 'Rewrite)
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
<$ :: a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
$c<$ :: forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
fmap :: (a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
$cfmap :: forall a b.
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
Functor, Functor (TcPluginM 'Rewrite)
a -> TcPluginM 'Rewrite a
Functor (TcPluginM 'Rewrite)
-> (forall a. a -> TcPluginM 'Rewrite a)
-> (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 a b.
    TcPluginM 'Rewrite a
    -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b)
-> (forall a b.
    TcPluginM 'Rewrite a
    -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a)
-> Applicative (TcPluginM 'Rewrite)
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
TcPluginM 'Rewrite (a -> b)
-> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
(a -> b -> c)
-> TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b
-> TcPluginM 'Rewrite c
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
<* :: TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
$c<* :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
*> :: TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
$c*> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
liftA2 :: (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
<*> :: 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 :: a -> TcPluginM 'Rewrite a
$cpure :: forall a. a -> TcPluginM 'Rewrite a
$cp1Applicative :: Functor (TcPluginM 'Rewrite)
Applicative, Applicative (TcPluginM 'Rewrite)
a -> TcPluginM 'Rewrite a
Applicative (TcPluginM 'Rewrite)
-> (forall a b.
    TcPluginM 'Rewrite a
    -> (a -> TcPluginM 'Rewrite b) -> TcPluginM 'Rewrite b)
-> (forall a b.
    TcPluginM 'Rewrite a
    -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b)
-> (forall a. a -> TcPluginM 'Rewrite a)
-> Monad (TcPluginM 'Rewrite)
TcPluginM 'Rewrite a
-> (a -> TcPluginM 'Rewrite b) -> TcPluginM 'Rewrite b
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
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 :: a -> TcPluginM 'Rewrite a
$creturn :: forall a. a -> TcPluginM 'Rewrite a
>> :: TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
$c>> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite 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
$cp1Monad :: Applicative (TcPluginM 'Rewrite)
Monad )
    via ( ReaderT BuiltinDefs ( ReaderT RewriteEnv GHC.TcPluginM ) )
newtype instance TcPluginM Stop a =
  TcPluginStopM { TcPluginM 'Stop a -> TcPluginM a
tcPluginStopM :: GHC.TcPluginM a }
  deriving newtype ( a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
(a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
(forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b)
-> (forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a)
-> Functor (TcPluginM 'Stop)
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
<$ :: a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
$c<$ :: forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
fmap :: (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
Functor, Functor (TcPluginM 'Stop)
a -> TcPluginM 'Stop a
Functor (TcPluginM 'Stop)
-> (forall a. a -> TcPluginM 'Stop a)
-> (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 a b.
    TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b)
-> (forall a b.
    TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a)
-> Applicative (TcPluginM 'Stop)
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
(a -> b -> c)
-> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c
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
<* :: TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
$c<* :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
*> :: TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
$c*> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
liftA2 :: (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
<*> :: 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 :: a -> TcPluginM 'Stop a
$cpure :: forall a. a -> TcPluginM 'Stop a
$cp1Applicative :: Functor (TcPluginM 'Stop)
Applicative, Applicative (TcPluginM 'Stop)
a -> TcPluginM 'Stop a
Applicative (TcPluginM 'Stop)
-> (forall a b.
    TcPluginM 'Stop a -> (a -> TcPluginM 'Stop b) -> TcPluginM 'Stop b)
-> (forall a b.
    TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b)
-> (forall a. a -> TcPluginM 'Stop a)
-> Monad (TcPluginM 'Stop)
TcPluginM 'Stop a -> (a -> TcPluginM 'Stop b) -> TcPluginM 'Stop b
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
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 :: a -> TcPluginM 'Stop a
$creturn :: forall a. a -> TcPluginM 'Stop a
>> :: TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
$c>> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop 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
$cp1Monad :: Applicative (TcPluginM 'Stop)
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 = (BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM EvBindsVar)
-> TcPluginM 'Solve EvBindsVar
forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
  \ BuiltinDefs
_defs
    EvBindsVar
evBinds
#ifdef HAS_DERIVEDS
    [Ct]
_deriveds
#endif
  -> EvBindsVar -> TcPluginM EvBindsVar
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
  (BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM [Ct])
-> TcPluginM 'Solve [Ct]
forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM \ BuiltinDefs
_defs EvBindsVar
_evBinds [Ct]
deriveds -> [Ct] -> TcPluginM [Ct]
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 = (BuiltinDefs -> RewriteEnv -> TcPluginM RewriteEnv)
-> TcPluginM 'Rewrite RewriteEnv
forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM ( \ BuiltinDefs
_ RewriteEnv
rewriteEnv -> RewriteEnv -> TcPluginM 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 = TcPluginM a -> m a
forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM (TcPluginM a -> m a) -> (TcM a -> TcPluginM a) -> TcM a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcM a -> TcPluginM a
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 :: TcPluginM a -> TcPluginM 'Init a
liftTcPluginM = TcPluginM a -> TcPluginM 'Init a
forall a. TcPluginM a -> TcPluginM 'Init a
TcPluginInitM
  unsafeWithRunInTcM :: ((forall a. TcPluginM 'Init a -> TcM a) -> TcM b)
-> TcPluginM 'Init b
unsafeWithRunInTcM (forall a. TcPluginM 'Init a -> TcM a) -> TcM b
runInTcM
    = TcM b -> TcPluginM 'Init b
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM b -> TcPluginM 'Init b) -> TcM b -> TcPluginM 'Init b
forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Init a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
      ( GHC.runTcPluginM . tcPluginInitM )
#else
      ( ( TcPluginM a -> EvBindsVar -> TcM a
forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` ( [Char] -> EvBindsVar
forall a. HasCallStack => [Char] -> a
error [Char]
"tcPluginInit: cannot access EvBindsVar" ) ) (TcPluginM a -> TcM a)
-> (TcPluginM 'Init a -> TcPluginM a) -> TcPluginM 'Init a -> TcM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM 'Init a -> TcPluginM a
forall a. TcPluginM 'Init a -> TcPluginM a
tcPluginInitM ) 
#endif
instance MonadTcPlugin ( TcPluginM Solve ) where
  liftTcPluginM :: TcPluginM a -> TcPluginM 'Solve a
liftTcPluginM  = (BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
#ifdef HAS_DERIVEDS
                 ((BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
 -> TcPluginM 'Solve a)
-> (TcPluginM a
    -> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM a
-> TcPluginM 'Solve a
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 a. TcPluginM 'Solve a -> TcM a) -> TcM b)
-> TcPluginM 'Solve b
unsafeWithRunInTcM (forall a. TcPluginM 'Solve a -> TcM a) -> TcM b
runInTcM
    = (BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM b)
-> TcPluginM 'Solve b
forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
      \ BuiltinDefs
builtinDefs
        EvBindsVar
evBinds
#ifdef HAS_DERIVEDS
        [Ct]
deriveds
#endif
      ->
        TcM b -> TcPluginM b
forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM (TcM b -> TcPluginM b) -> TcM b -> TcPluginM b
forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Solve a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
          ( GHC.runTcPluginM
#ifdef HAS_DERIVEDS
          . ( \ f -> f builtinDefs evBinds deriveds )
#else
          . ( \ f -> f builtinDefs evBinds )
#endif
          . tcPluginSolveM )
#else
          ( ( TcPluginM a -> EvBindsVar -> TcM a
forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` EvBindsVar
evBinds )
          (TcPluginM a -> TcM a)
-> (TcPluginM 'Solve a -> TcPluginM a)
-> TcPluginM 'Solve a
-> TcM a
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 )
          ((BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a) -> TcPluginM a)
-> (TcPluginM 'Solve a
    -> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
-> TcPluginM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM 'Solve a
-> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
forall a.
TcPluginM 'Solve a
-> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
tcPluginSolveM
          )
#endif
instance MonadTcPlugin ( TcPluginM Rewrite ) where
  liftTcPluginM :: TcPluginM a -> TcPluginM 'Rewrite a
liftTcPluginM = (BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM ((BuiltinDefs -> RewriteEnv -> TcPluginM a)
 -> TcPluginM 'Rewrite a)
-> (TcPluginM a -> BuiltinDefs -> RewriteEnv -> TcPluginM a)
-> TcPluginM a
-> TcPluginM 'Rewrite a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ TcPluginM a
ma BuiltinDefs
_ RewriteEnv
_ -> TcPluginM a
ma )
  unsafeWithRunInTcM :: ((forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b)
-> TcPluginM 'Rewrite b
unsafeWithRunInTcM (forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b
runInTcM
    = (BuiltinDefs -> RewriteEnv -> TcPluginM b) -> TcPluginM 'Rewrite b
forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM \ BuiltinDefs
builtinDefs RewriteEnv
rewriteEnv ->
      TcM b -> TcPluginM b
forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM (TcM b -> TcPluginM b) -> TcM b -> TcPluginM b
forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
        ( GHC.runTcPluginM
#else
        ( ( TcPluginM a -> EvBindsVar -> TcM a
forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` ( [Char] -> EvBindsVar
forall a. HasCallStack => [Char] -> a
error [Char]
"tcPluginRewrite: cannot access EvBindsVar" ) )
#endif
        (TcPluginM a -> TcM a)
-> (TcPluginM 'Rewrite a -> TcPluginM a)
-> TcPluginM 'Rewrite a
-> TcM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ BuiltinDefs -> RewriteEnv -> TcPluginM a
f -> BuiltinDefs -> RewriteEnv -> TcPluginM a
f BuiltinDefs
builtinDefs RewriteEnv
rewriteEnv )
        ((BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM a)
-> (TcPluginM 'Rewrite a
    -> BuiltinDefs -> RewriteEnv -> TcPluginM a)
-> TcPluginM 'Rewrite a
-> TcPluginM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
forall a.
TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM )
instance MonadTcPlugin ( TcPluginM Stop ) where
  liftTcPluginM :: TcPluginM a -> TcPluginM 'Stop a
liftTcPluginM = TcPluginM a -> TcPluginM 'Stop a
forall a. TcPluginM a -> TcPluginM 'Stop a
TcPluginStopM
  unsafeWithRunInTcM :: ((forall a. TcPluginM 'Stop a -> TcM a) -> TcM b)
-> TcPluginM 'Stop b
unsafeWithRunInTcM (forall a. TcPluginM 'Stop a -> TcM a) -> TcM b
runInTcM
    = TcM b -> TcPluginM 'Stop b
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM b -> TcPluginM 'Stop b) -> TcM b -> TcPluginM 'Stop b
forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Stop a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
      ( GHC.runTcPluginM . tcPluginStopM )
#else
      ( ( TcPluginM a -> EvBindsVar -> TcM a
forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` ( [Char] -> EvBindsVar
forall a. HasCallStack => [Char] -> a
error [Char]
"tcPluginStop: cannot access EvBindsVar" ) ) (TcPluginM a -> TcM a)
-> (TcPluginM 'Stop a -> TcPluginM a) -> TcPluginM 'Stop a -> TcM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM 'Stop a -> TcPluginM a
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 :: (TcM a -> TcM b) -> m a -> m b
unsafeLiftThroughTcM TcM a -> TcM b
f m a
ma = ((forall a. m a -> TcM a) -> TcM b) -> m b
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 ( m a -> TcM a
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 TcPluginRewriter
tcPluginRewrite :: s -> UniqFM TcPluginRewriter
tcPluginRewrite :: ()
tcPluginRewrite
              , s -> TcPluginM 'Stop ()
tcPluginStop :: s -> TcPluginM 'Stop ()
tcPluginStop :: ()
tcPluginStop
              }
           ) =
  TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
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 TcPluginRewriter)
-> TcPluginDefs s
-> TcPluginSolver
adaptUserSolveAndRewrite
                              s -> TcPluginSolver
tcPluginSolve s -> UniqFM 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    <- TcPluginM 'Init s -> TcPluginM s
forall a. TcPluginM 'Init a -> TcPluginM a
tcPluginInitM TcPluginM 'Init s
userInit
      TcPluginDefs s -> TcPluginM (TcPluginDefs s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( TcPluginDefs :: forall s. BuiltinDefs -> s -> TcPluginDefs s
TcPluginDefs { BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs, s
tcPluginUserDefs :: s
tcPluginUserDefs :: s
tcPluginUserDefs })

#ifdef HAS_REWRITING
    adaptUserSolve :: ( userDefs -> TcPluginSolver )
                   -> TcPluginDefs userDefs
                   -> GHC.EvBindsVar
                   -> GHC.TcPluginSolver
    adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )
     evBindsVar
#ifdef HAS_DERIVEDS
      = \ givens deriveds wanteds -> do
        tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds )
          tcPluginBuiltinDefs evBindsVar deriveds
#else
      = \ givens _deriveds wanteds -> do
        tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds )
          tcPluginBuiltinDefs evBindsVar
#endif

    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 TcPluginRewriter)
-> TcPluginDefs s
-> TcPluginSolver
adaptUserSolveAndRewrite s -> TcPluginSolver
userSolve s -> UniqFM 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
          ( (TcPluginRewriter
 -> RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult)
-> UniqFM TcPluginRewriter -> Rewriters
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
              ( \ TcPluginRewriter
userRewriter RewriteEnv
rewriteEnv [Ct]
gs [Type]
tys ->
                TcPluginM 'Rewrite TcPluginRewriteResult
-> BuiltinDefs -> RewriteEnv -> TcPluginM TcPluginRewriteResult
forall a.
TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM ( TcPluginRewriter
userRewriter [Ct]
gs [Type]
tys )
                  BuiltinDefs
tcPluginBuiltinDefs RewriteEnv
rewriteEnv
              )
              ( s -> UniqFM TcPluginRewriter
userRewrite s
tcPluginUserDefs )
          )
          ( \ [Ct]
gs [Ct]
ds [Ct]
ws ->
            TcPluginM 'Solve TcPluginSolveResult
-> BuiltinDefs
-> EvBindsVar
-> [Ct]
-> TcPluginM TcPluginSolveResult
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 } ) =
      TcPluginM 'Stop () -> TcPluginM ()
forall a. TcPluginM 'Stop a -> TcPluginM a
tcPluginStopM (TcPluginM 'Stop () -> TcPluginM ())
-> TcPluginM 'Stop () -> TcPluginM ()
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 = [Char] -> m BuiltinDefs
forall a. HasCallStack => [Char] -> a
error [Char]
"askBuiltins: no default implementation"
instance MonadTcPluginWork ( TcPluginM Solve ) where
  askBuiltins :: TcPluginM 'Solve BuiltinDefs
askBuiltins = (BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM BuiltinDefs)
-> TcPluginM 'Solve BuiltinDefs
forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
    \ BuiltinDefs
builtinDefs
      EvBindsVar
_evBinds
#ifdef HAS_DERIVEDS
      [Ct]
_deriveds
#endif
    -> BuiltinDefs -> TcPluginM BuiltinDefs
forall (f :: * -> *) a. Applicative f => a -> f a
pure BuiltinDefs
builtinDefs
instance MonadTcPluginWork ( TcPluginM Rewrite ) where
  askBuiltins :: TcPluginM 'Rewrite BuiltinDefs
askBuiltins = (BuiltinDefs -> RewriteEnv -> TcPluginM BuiltinDefs)
-> TcPluginM 'Rewrite BuiltinDefs
forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM \ BuiltinDefs
builtinDefs RewriteEnv
_evBinds -> BuiltinDefs -> TcPluginM BuiltinDefs
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 = [Char] -> TcPluginM 'Init BuiltinDefs
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 = [Char] -> TcPluginM 'Stop BuiltinDefs
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 :: TcPluginErrorMessage -> m Type
mkTcPluginErrorTy TcPluginErrorMessage
msg = do
  builtinDefs :: BuiltinDefs
builtinDefs@( BuiltinDefs { TyCon
typeErrorTyCon :: BuiltinDefs -> TyCon
typeErrorTyCon :: TyCon
typeErrorTyCon } ) <- m BuiltinDefs
forall (m :: * -> *). MonadTcPluginWork m => m BuiltinDefs
askBuiltins
  let
    errorMsgTy :: GHC.PredType
    errorMsgTy :: Type
errorMsgTy = BuiltinDefs -> TcPluginErrorMessage -> Type
interpretErrorMessage BuiltinDefs
builtinDefs TcPluginErrorMessage
msg
  Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
typeErrorTyCon [ Type
GHC.constraintKind, Type
errorMsgTy ]

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

-- 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
  { TcPluginDefs s -> BuiltinDefs
tcPluginBuiltinDefs :: !BuiltinDefs
  , 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 (DataCon -> TyCon) -> TcPluginM DataCon -> TcPluginM TyCon
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 (DataCon -> TyCon) -> TcPluginM DataCon -> TcPluginM TyCon
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 (DataCon -> TyCon) -> TcPluginM DataCon -> TcPluginM TyCon
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 (DataCon -> TyCon) -> TcPluginM DataCon -> TcPluginM TyCon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM DataCon
GHC.tcLookupDataCon Name
GHC.TypeLits.typeErrorVAppendDataConName
  BuiltinDefs -> TcPluginM BuiltinDefs
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( BuiltinDefs :: TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> BuiltinDefs
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 (TyLit -> Type) -> ([Char] -> TyLit) -> [Char] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FastString -> TyLit
GHC.StrTyLit (FastString -> TyLit) -> ([Char] -> FastString) -> [Char] -> TyLit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> FastString
GHC.fsLit ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ [Char]
str ]
    go ( PrintType Type
ty ) =
      TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
showTypeTyCon [ HasDebugCallStack => Type -> Type
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 ]