{-# 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, typeKind )
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 -> 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
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
fmap :: forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
$c<$ :: forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a
<$ :: forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a
Functor, Functor (TcPluginM 'Init)
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)
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
$cpure :: forall a. a -> TcPluginM 'Init a
pure :: forall a. a -> TcPluginM 'Init a
$c<*> :: forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
<*> :: forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c
$c*> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
*> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
$c<* :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
<* :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
Applicative, Applicative (TcPluginM 'Init)
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)
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
$c>>= :: forall a b.
TcPluginM 'Init a -> (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 -> TcPluginM 'Init b -> TcPluginM 'Init b
>> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
$creturn :: forall a. a -> TcPluginM 'Init a
return :: forall a. a -> TcPluginM 'Init a
Monad )
#ifdef HAS_DERIVEDS
newtype instance TcPluginM Solve a =
  TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> [GHC.Ct] -> GHC.TcPluginM a }
  deriving ( Functor, Applicative, Monad )
    via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar ( ReaderT [GHC.Ct] GHC.TcPluginM ) ) )
#else
newtype instance TcPluginM Solve a =
  TcPluginSolveM { forall a.
TcPluginM 'Solve a -> BuiltinDefs -> EvBindsVar -> TcPluginM a
tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> GHC.TcPluginM a }
  deriving ( (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
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
fmap :: forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
$c<$ :: forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
<$ :: forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
Functor, Functor (TcPluginM 'Solve)
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)
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
$cpure :: forall a. a -> TcPluginM 'Solve a
pure :: forall a. a -> TcPluginM 'Solve a
$c<*> :: forall a b.
TcPluginM 'Solve (a -> b)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b
<*> :: forall a b.
TcPluginM 'Solve (a -> b)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c
$c*> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
*> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
$c<* :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
<* :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
Applicative, Applicative (TcPluginM 'Solve)
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)
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
$c>>= :: forall a b.
TcPluginM 'Solve a
-> (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 -> TcPluginM 'Solve b -> TcPluginM 'Solve b
>> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
$creturn :: forall a. a -> TcPluginM 'Solve a
return :: forall a. a -> TcPluginM 'Solve a
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 -> 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
$cfmap :: forall a b.
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
fmap :: forall a b.
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
$c<$ :: forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
<$ :: forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
Functor, Functor (TcPluginM 'Rewrite)
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)
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
$cpure :: forall a. a -> TcPluginM 'Rewrite a
pure :: forall a. a -> TcPluginM 'Rewrite a
$c<*> :: forall a b.
TcPluginM 'Rewrite (a -> b)
-> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
<*> :: forall a b.
TcPluginM 'Rewrite (a -> b)
-> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b
-> TcPluginM 'Rewrite c
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b
-> TcPluginM 'Rewrite c
$c*> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
*> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
$c<* :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
<* :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
Applicative, Applicative (TcPluginM 'Rewrite)
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)
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
$c>>= :: forall a b.
TcPluginM 'Rewrite a
-> (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
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
>> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
$creturn :: forall a. a -> TcPluginM 'Rewrite a
return :: forall a. a -> TcPluginM 'Rewrite a
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 -> 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
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
fmap :: forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
$c<$ :: forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
<$ :: forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
Functor, Functor (TcPluginM 'Stop)
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)
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
$cpure :: forall a. a -> TcPluginM 'Stop a
pure :: forall a. a -> TcPluginM 'Stop a
$c<*> :: forall a b.
TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
<*> :: forall a b.
TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c
$c*> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
*> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
$c<* :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
<* :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
Applicative, Applicative (TcPluginM 'Stop)
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)
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
$c>>= :: forall a b.
TcPluginM 'Stop a -> (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 -> TcPluginM 'Stop b -> TcPluginM 'Stop b
>> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
$creturn :: forall a. a -> TcPluginM 'Stop a
return :: forall a. a -> TcPluginM 'Stop a
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 -> TcPluginM EvBindsVar)
-> TcPluginM 'Solve EvBindsVar
forall a.
(BuiltinDefs -> EvBindsVar -> TcPluginM a) -> TcPluginM 'Solve a
TcPluginSolveM
  \ BuiltinDefs
_defs
    EvBindsVar
evBinds
#ifdef HAS_DERIVEDS
    _deriveds
#endif
  -> EvBindsVar -> TcPluginM EvBindsVar
forall a. a -> TcPluginM a
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
  TcPluginSolveM \ _defs _evBinds deriveds -> pure deriveds
#else
  [Ct] -> TcPluginM 'Solve [Ct]
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
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 a. a -> TcPluginM a
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 a. 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 :: forall a. TcPluginM a -> TcPluginM 'Init a
liftTcPluginM = TcPluginM a -> TcPluginM 'Init a
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
    = TcM b -> TcPluginM 'Init b
forall a. TcM a -> TcPluginM 'Init a
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
      ( TcPluginM a -> TcM a
forall a. TcPluginM a -> TcM a
GHC.runTcPluginM (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 )
#else
      ( ( `GHC.runTcPluginM` ( error "tcPluginInit: cannot access EvBindsVar" ) ) . tcPluginInitM )
#endif
instance MonadTcPlugin ( TcPluginM Solve ) where
  liftTcPluginM :: forall a. TcPluginM a -> TcPluginM 'Solve a
liftTcPluginM  = (BuiltinDefs -> EvBindsVar -> TcPluginM a) -> TcPluginM 'Solve a
forall a.
(BuiltinDefs -> EvBindsVar -> TcPluginM a) -> TcPluginM 'Solve a
TcPluginSolveM
#ifdef HAS_DERIVEDS
                 . ( \ ma _defs _evBinds _deriveds -> ma )
#else
                 ((BuiltinDefs -> EvBindsVar -> TcPluginM a) -> TcPluginM 'Solve a)
-> (TcPluginM a -> BuiltinDefs -> EvBindsVar -> TcPluginM a)
-> TcPluginM a
-> TcPluginM 'Solve a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ TcPluginM a
ma BuiltinDefs
_defs EvBindsVar
_evBinds -> TcPluginM a
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
    = (BuiltinDefs -> EvBindsVar -> TcPluginM b) -> TcPluginM 'Solve b
forall a.
(BuiltinDefs -> EvBindsVar -> TcPluginM a) -> TcPluginM 'Solve a
TcPluginSolveM
      \ BuiltinDefs
builtinDefs
        EvBindsVar
evBinds
#ifdef HAS_DERIVEDS
        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
  -- (no deriveds)

          ( TcPluginM a -> TcM a
forall a. TcPluginM a -> TcM a
GHC.runTcPluginM
          (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 -> TcPluginM a
f -> BuiltinDefs -> EvBindsVar -> TcPluginM a
f BuiltinDefs
builtinDefs EvBindsVar
evBinds )
          ((BuiltinDefs -> EvBindsVar -> TcPluginM a) -> TcPluginM a)
-> (TcPluginM 'Solve a -> BuiltinDefs -> EvBindsVar -> TcPluginM a)
-> TcPluginM 'Solve a
-> TcPluginM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM 'Solve a -> BuiltinDefs -> EvBindsVar -> TcPluginM a
forall a.
TcPluginM 'Solve a -> BuiltinDefs -> EvBindsVar -> TcPluginM a
tcPluginSolveM )
#else
          ( ( `GHC.runTcPluginM` evBinds )
          . ( \ f -> f builtinDefs evBinds deriveds )
          . tcPluginSolveM
          )
#endif
instance MonadTcPlugin ( TcPluginM Rewrite ) where
  liftTcPluginM :: forall a. 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 b.
((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
        ( TcPluginM a -> TcM a
forall a. TcPluginM a -> TcM a
GHC.runTcPluginM
#else
        ( ( `GHC.runTcPluginM` ( error "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 :: forall a. TcPluginM a -> TcPluginM 'Stop a
liftTcPluginM = TcPluginM a -> TcPluginM 'Stop a
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
    = TcM b -> TcPluginM 'Stop b
forall a. TcM a -> TcPluginM 'Stop a
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
      ( TcPluginM a -> TcM a
forall a. TcPluginM a -> TcM a
GHC.runTcPluginM (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 )
#else
      ( ( `GHC.runTcPluginM` ( error "tcPluginStop: cannot access EvBindsVar" ) ) . 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 a. m a -> TcM a) -> TcM b) -> m b
forall b. ((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 :: ()
tcPluginSolve :: s -> TcPluginSolver
tcPluginSolve
              , s -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite :: ()
tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite
              , s -> TcPluginM 'Stop ()
tcPluginStop :: ()
tcPluginStop :: s -> TcPluginM 'Stop ()
tcPluginStop
              }
           ) =
  GHC.TcPlugin
    { tcPluginInit :: TcPluginM (TcPluginDefs s)
GHC.tcPluginInit    = TcPluginM 'Init s -> TcPluginM (TcPluginDefs s)
adaptUserInit    TcPluginM 'Init s
tcPluginInit
#ifdef HAS_REWRITING
    , tcPluginSolve :: TcPluginDefs s -> TcPluginSolver
GHC.tcPluginSolve   = (s -> TcPluginSolver) -> TcPluginDefs s -> TcPluginSolver
adaptUserSolve   s -> TcPluginSolver
tcPluginSolve
    , tcPluginRewrite :: TcPluginDefs s -> UniqFM TyCon TcPluginRewriter
GHC.tcPluginRewrite = (s -> UniqFM TyCon TcPluginRewriter)
-> TcPluginDefs s -> UniqFM TyCon TcPluginRewriter
adaptUserRewrite s -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite
#else
    , GHC.tcPluginSolve   = adaptUserSolveAndRewrite
                              tcPluginSolve 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 a. a -> TcPluginM a
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 :: (s -> TcPluginSolver) -> TcPluginDefs s -> TcPluginSolver
adaptUserSolve s -> TcPluginSolver
userSolve ( TcPluginDefs { s
tcPluginUserDefs :: forall s. TcPluginDefs s -> s
tcPluginUserDefs :: s
tcPluginUserDefs, BuiltinDefs
tcPluginBuiltinDefs :: forall s. TcPluginDefs s -> BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs } )
      = \ EvBindsVar
evBindsVar [Ct]
givens [Ct]
wanteds -> do
        TcPluginM 'Solve TcPluginSolveResult
-> BuiltinDefs -> EvBindsVar -> TcPluginM TcPluginSolveResult
forall a.
TcPluginM 'Solve a -> BuiltinDefs -> EvBindsVar -> TcPluginM a
tcPluginSolveM ( s -> TcPluginSolver
userSolve s
tcPluginUserDefs [Ct]
givens [Ct]
wanteds )
          BuiltinDefs
tcPluginBuiltinDefs EvBindsVar
evBindsVar
    adaptUserRewrite :: ( userDefs -> GHC.UniqFM GHC.TyCon TcPluginRewriter )
                     -> TcPluginDefs userDefs -> GHC.UniqFM GHC.TyCon GHC.TcPluginRewriter
    adaptUserRewrite :: (s -> UniqFM TyCon TcPluginRewriter)
-> TcPluginDefs s -> UniqFM TyCon TcPluginRewriter
adaptUserRewrite s -> UniqFM TyCon TcPluginRewriter
userRewrite ( TcPluginDefs { s
tcPluginUserDefs :: forall s. TcPluginDefs s -> s
tcPluginUserDefs :: s
tcPluginUserDefs, BuiltinDefs
tcPluginBuiltinDefs :: forall s. TcPluginDefs s -> BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs })
      = (TcPluginRewriter -> TcPluginRewriter)
-> UniqFM TyCon TcPluginRewriter -> UniqFM TyCon TcPluginRewriter
forall a b. (a -> b) -> UniqFM TyCon a -> UniqFM TyCon b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
          ( \ TcPluginRewriter
userRewriter RewriteEnv
rewriteEnv [Ct]
givens [TcType]
tys ->
            TcPluginM 'Rewrite TcPluginRewriteResult
-> BuiltinDefs -> RewriteEnv -> TcPluginM TcPluginRewriteResult
forall a.
TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM ( TcPluginRewriter
userRewriter [Ct]
givens [TcType]
tys ) BuiltinDefs
tcPluginBuiltinDefs RewriteEnv
rewriteEnv
          )
          ( s -> UniqFM TyCon TcPluginRewriter
userRewrite s
tcPluginUserDefs )
#else
    adaptUserSolveAndRewrite
      :: ( userDefs -> TcPluginSolver )
      -> ( userDefs -> GHC.UniqFM
#if MIN_VERSION_ghc(9,0,0)
                         GHC.TyCon
#endif
                         TcPluginRewriter
         )
      -> TcPluginDefs userDefs
      -> GHC.TcPluginSolver
    adaptUserSolveAndRewrite userSolve userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )
      = \ givens deriveds wanteds -> do
        evBindsVar <- GHC.getEvBindsTcPluginM
        shimRewriter
          givens deriveds wanteds
          ( fmap
              ( \ userRewriter rewriteEnv gs tys ->
                tcPluginRewriteM ( userRewriter gs tys )
                  tcPluginBuiltinDefs rewriteEnv
              )
              ( userRewrite tcPluginUserDefs )
          )
          ( \ gs ds ws ->
            tcPluginSolveM ( userSolve tcPluginUserDefs gs ws )
              tcPluginBuiltinDefs evBindsVar 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 :: forall s. TcPluginDefs s -> s
tcPluginUserDefs :: 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 -> TcPluginM BuiltinDefs)
-> TcPluginM 'Solve BuiltinDefs
forall a.
(BuiltinDefs -> EvBindsVar -> TcPluginM a) -> TcPluginM 'Solve a
TcPluginSolveM
    \ BuiltinDefs
builtinDefs
      EvBindsVar
_evBinds
#ifdef HAS_DERIVEDS
      _deriveds
#endif
    -> BuiltinDefs -> TcPluginM BuiltinDefs
forall a. a -> TcPluginM a
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 a. a -> TcPluginM a
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 :: forall (m :: * -> *).
MonadTcPluginWork m =>
TcPluginErrorMessage -> m TcType
mkTcPluginErrorTy TcPluginErrorMessage
msg = do
  builtinDefs :: BuiltinDefs
builtinDefs@( BuiltinDefs { TyCon
typeErrorTyCon :: TyCon
typeErrorTyCon :: BuiltinDefs -> TyCon
typeErrorTyCon } ) <- m BuiltinDefs
forall (m :: * -> *). MonadTcPluginWork m => m BuiltinDefs
askBuiltins
  let
    errorMsgTy :: GHC.PredType
    errorMsgTy :: TcType
errorMsgTy = BuiltinDefs -> TcPluginErrorMessage -> TcType
interpretErrorMessage BuiltinDefs
builtinDefs TcPluginErrorMessage
msg
  TcType -> m TcType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcType -> m TcType) -> TcType -> m TcType
forall a b. (a -> b) -> a -> b
$ TyCon -> [TcType] -> TcType
GHC.mkTyConApp TyCon
typeErrorTyCon [ TcType
GHC.constraintKind, TcType
errorMsgTy ]

instance ( Monad (TcPluginM s), MonadTcPlugin (TcPluginM s) )
      => MonadThings (TcPluginM s) where
  lookupThing :: Name -> TcPluginM s TyThing
lookupThing = TcM TyThing -> TcPluginM s TyThing
forall a. TcM a -> TcPluginM s a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM TyThing -> TcPluginM s TyThing)
-> (Name -> TcM TyThing) -> Name -> TcPluginM s TyThing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcM TyThing
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 (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 a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( BuiltinDefs { TyCon
typeErrorTyCon :: TyCon
textTyCon :: TyCon
showTypeTyCon :: TyCon
concatTyCon :: TyCon
vcatTyCon :: TyCon
typeErrorTyCon :: TyCon
textTyCon :: TyCon
showTypeTyCon :: TyCon
concatTyCon :: TyCon
vcatTyCon :: TyCon
.. } )

interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> GHC.PredType
interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> TcType
interpretErrorMessage ( BuiltinDefs { TyCon
typeErrorTyCon :: BuiltinDefs -> TyCon
textTyCon :: BuiltinDefs -> TyCon
showTypeTyCon :: BuiltinDefs -> TyCon
concatTyCon :: BuiltinDefs -> TyCon
vcatTyCon :: BuiltinDefs -> TyCon
typeErrorTyCon :: TyCon
textTyCon :: TyCon
showTypeTyCon :: TyCon
concatTyCon :: TyCon
vcatTyCon :: TyCon
.. } ) = TcPluginErrorMessage -> TcType
go
  where
    go :: TcPluginErrorMessage -> GHC.PredType
    go :: TcPluginErrorMessage -> TcType
go ( Txt [Char]
str ) =
      TyCon -> [TcType] -> TcType
GHC.mkTyConApp TyCon
textTyCon [ TyLit -> TcType
GHC.LitTy (TyLit -> TcType) -> ([Char] -> TyLit) -> [Char] -> TcType
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] -> TcType) -> [Char] -> TcType
forall a b. (a -> b) -> a -> b
$ [Char]
str ]
    go ( PrintType TcType
ty ) =
      TyCon -> [TcType] -> TcType
GHC.mkTyConApp TyCon
showTypeTyCon [ (() :: Constraint) => TcType -> TcType
TcType -> TcType
GHC.typeKind TcType
ty, TcType
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 -> [TcType] -> TcType
GHC.mkTyConApp TyCon
concatTyCon [ TcPluginErrorMessage -> TcType
go TcPluginErrorMessage
msg1, TcPluginErrorMessage -> TcType
go TcPluginErrorMessage
msg2 ]
    go ( TcPluginErrorMessage
msg1 :-: TcPluginErrorMessage
msg2 ) =
      TyCon -> [TcType] -> TcType
GHC.mkTyConApp TyCon
vcatTyCon [ TcPluginErrorMessage -> TcType
go TcPluginErrorMessage
msg1, TcPluginErrorMessage -> TcType
go TcPluginErrorMessage
msg2 ]