{-# 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
(
MonadTcPlugin(..), MonadTcPluginWork
, unsafeLiftThroughTcM
, TcPlugin(..), TcPluginStage(..)
, TcPluginSolver
, TcPluginM(..)
, TcPluginErrorMessage(..)
, TcPluginRewriter
, MonadThings(..)
, askRewriteEnv
, askDeriveds
, askEvBinds
, mkTcPlugin
, mkTcPluginErrorTy
)
where
import Data.Coerce
( Coercible )
import Data.Kind
( Type )
import GHC.TypeLits
( TypeError, ErrorMessage(..) )
import Control.Monad.Trans.Reader
( ReaderT(..) )
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
#ifndef HAS_REWRITING
import GHC.TcPlugin.API.Internal.Shim
( TcPluginSolveResult, TcPluginRewriteResult(..)
, RewriteEnv
, shimRewriter
)
#endif
data TcPluginStage
= Init
| Solve
| Rewrite
| Stop
type TcPluginSolver
= [GHC.Ct]
-> [GHC.Ct]
-> TcPluginM Solve TcPluginSolveResult
type TcPluginRewriter
= [GHC.Ct]
-> [GHC.Type]
-> TcPluginM Rewrite TcPluginRewriteResult
data TcPlugin = forall s. TcPlugin
{ ()
tcPluginInit :: TcPluginM Init s
, ()
tcPluginSolve :: s -> TcPluginSolver
, ()
tcPluginRewrite
:: s -> GHC.UniqFM
#if MIN_VERSION_ghc(9,0,0)
GHC.TyCon
#endif
TcPluginRewriter
, ()
tcPluginStop :: s -> TcPluginM Stop ()
}
data family TcPluginM (s :: TcPluginStage) :: Type -> Type
newtype instance TcPluginM Init a =
TcPluginInitM { forall a. TcPluginM 'Init a -> TcPluginM a
tcPluginInitM :: GHC.TcPluginM a }
deriving newtype ( forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a
forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a
$c<$ :: forall a b. a -> TcPluginM 'Init b -> TcPluginM 'Init a
fmap :: forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
Functor, Functor (TcPluginM 'Init)
forall a. a -> TcPluginM 'Init a
forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall a b c.
(a -> b -> c)
-> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
$c<* :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a
*> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
$c*> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c
<*> :: forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
$c<*> :: forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
pure :: forall a. a -> TcPluginM 'Init a
$cpure :: forall a. a -> TcPluginM 'Init a
Applicative, Applicative (TcPluginM 'Init)
forall a. a -> TcPluginM 'Init a
forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TcPluginM 'Init a
$creturn :: forall a. a -> TcPluginM 'Init a
>> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
$c>> :: forall a b.
TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b
>>= :: forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
$c>>= :: forall a b.
TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b
Monad )
#ifdef HAS_DERIVEDS
newtype instance TcPluginM Solve a =
TcPluginSolveM { forall a.
TcPluginM 'Solve a
-> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> [GHC.Ct] -> GHC.TcPluginM a }
deriving ( forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
$c<$ :: forall a b. a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
fmap :: forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b
Functor, Functor (TcPluginM 'Solve)
forall a. a -> TcPluginM 'Solve a
forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
forall a b.
TcPluginM 'Solve (a -> b)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b
forall a b c.
(a -> b -> c)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
$c<* :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a
*> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
$c*> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c
<*> :: forall a b.
TcPluginM 'Solve (a -> b)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b
$c<*> :: forall a b.
TcPluginM 'Solve (a -> b)
-> TcPluginM 'Solve a -> TcPluginM 'Solve b
pure :: forall a. a -> TcPluginM 'Solve a
$cpure :: forall a. a -> TcPluginM 'Solve a
Applicative, Applicative (TcPluginM 'Solve)
forall a. a -> TcPluginM 'Solve a
forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
forall a b.
TcPluginM 'Solve a
-> (a -> TcPluginM 'Solve b) -> TcPluginM 'Solve b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TcPluginM 'Solve a
$creturn :: forall a. a -> TcPluginM 'Solve a
>> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
$c>> :: forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
>>= :: forall a b.
TcPluginM 'Solve a
-> (a -> TcPluginM 'Solve b) -> TcPluginM 'Solve b
$c>>= :: forall a b.
TcPluginM 'Solve a
-> (a -> TcPluginM 'Solve b) -> TcPluginM 'Solve b
Monad )
via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar ( ReaderT [GHC.Ct] GHC.TcPluginM ) ) )
#else
newtype instance TcPluginM Solve a =
TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> GHC.TcPluginM a }
deriving ( Functor, Applicative, Monad )
via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar GHC.TcPluginM ) )
#endif
newtype instance TcPluginM Rewrite a =
TcPluginRewriteM { forall a.
TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM :: BuiltinDefs -> RewriteEnv -> GHC.TcPluginM a }
deriving ( forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
forall a b.
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
$c<$ :: forall a b. a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
fmap :: forall a b.
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
$cfmap :: forall a b.
(a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
Functor, Functor (TcPluginM 'Rewrite)
forall a. a -> TcPluginM 'Rewrite a
forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
forall a b.
TcPluginM 'Rewrite (a -> b)
-> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
forall a b c.
(a -> b -> c)
-> TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b
-> TcPluginM 'Rewrite c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
$c<* :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a
*> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
$c*> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b
-> TcPluginM 'Rewrite c
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b
-> TcPluginM 'Rewrite c
<*> :: forall a b.
TcPluginM 'Rewrite (a -> b)
-> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
$c<*> :: forall a b.
TcPluginM 'Rewrite (a -> b)
-> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b
pure :: forall a. a -> TcPluginM 'Rewrite a
$cpure :: forall a. a -> TcPluginM 'Rewrite a
Applicative, Applicative (TcPluginM 'Rewrite)
forall a. a -> TcPluginM 'Rewrite a
forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
forall a b.
TcPluginM 'Rewrite a
-> (a -> TcPluginM 'Rewrite b) -> TcPluginM 'Rewrite b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TcPluginM 'Rewrite a
$creturn :: forall a. a -> TcPluginM 'Rewrite a
>> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
$c>> :: forall a b.
TcPluginM 'Rewrite a
-> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b
>>= :: forall a b.
TcPluginM 'Rewrite a
-> (a -> TcPluginM 'Rewrite b) -> TcPluginM 'Rewrite b
$c>>= :: forall a b.
TcPluginM 'Rewrite a
-> (a -> TcPluginM 'Rewrite b) -> TcPluginM 'Rewrite b
Monad )
via ( ReaderT BuiltinDefs ( ReaderT RewriteEnv GHC.TcPluginM ) )
newtype instance TcPluginM Stop a =
TcPluginStopM { forall a. TcPluginM 'Stop a -> TcPluginM a
tcPluginStopM :: GHC.TcPluginM a }
deriving newtype ( forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
$c<$ :: forall a b. a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
fmap :: forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
$cfmap :: forall a b. (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
Functor, Functor (TcPluginM 'Stop)
forall a. a -> TcPluginM 'Stop a
forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
forall a b.
TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
forall a b c.
(a -> b -> c)
-> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
$c<* :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a
*> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
$c*> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
liftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c
$cliftA2 :: forall a b c.
(a -> b -> c)
-> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c
<*> :: forall a b.
TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
$c<*> :: forall a b.
TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b
pure :: forall a. a -> TcPluginM 'Stop a
$cpure :: forall a. a -> TcPluginM 'Stop a
Applicative, Applicative (TcPluginM 'Stop)
forall a. a -> TcPluginM 'Stop a
forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
forall a b.
TcPluginM 'Stop a -> (a -> TcPluginM 'Stop b) -> TcPluginM 'Stop b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TcPluginM 'Stop a
$creturn :: forall a. a -> TcPluginM 'Stop a
>> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
$c>> :: forall a b.
TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b
>>= :: forall a b.
TcPluginM 'Stop a -> (a -> TcPluginM 'Stop b) -> TcPluginM 'Stop b
$c>>= :: forall a b.
TcPluginM 'Stop a -> (a -> TcPluginM 'Stop b) -> TcPluginM 'Stop b
Monad )
askEvBinds :: TcPluginM Solve GHC.EvBindsVar
askEvBinds :: TcPluginM 'Solve EvBindsVar
askEvBinds = forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
\ BuiltinDefs
_defs
EvBindsVar
evBinds
#ifdef HAS_DERIVEDS
[Ct]
_deriveds
#endif
-> forall (f :: * -> *) a. Applicative f => a -> f a
pure EvBindsVar
evBinds
askDeriveds :: TcPluginM Solve [GHC.Ct]
askDeriveds :: TcPluginM 'Solve [Ct]
askDeriveds =
#ifdef HAS_DERIVEDS
forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM \ BuiltinDefs
_defs EvBindsVar
_evBinds [Ct]
deriveds -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Ct]
deriveds
#else
pure []
#endif
askRewriteEnv :: TcPluginM Rewrite RewriteEnv
askRewriteEnv :: TcPluginM 'Rewrite RewriteEnv
askRewriteEnv = forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM ( \ BuiltinDefs
_ RewriteEnv
rewriteEnv -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RewriteEnv
rewriteEnv )
class ( Monad m, ( forall x y. Coercible x y => Coercible (m x) (m y) ) ) => MonadTcPlugin (m :: Type -> Type) where
{-# MINIMAL liftTcPluginM, unsafeWithRunInTcM #-}
liftTcPluginM :: GHC.TcPluginM a -> m a
unsafeLiftTcM :: GHC.TcM a -> m a
unsafeLiftTcM = forall (m :: * -> *) a. MonadTcPlugin m => TcPluginM a -> m a
liftTcPluginM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM
unsafeWithRunInTcM :: ( ( forall a. m a -> GHC.TcM a ) -> GHC.TcM b ) -> m b
instance MonadTcPlugin ( TcPluginM Init ) where
liftTcPluginM :: forall a. TcPluginM a -> TcPluginM 'Init a
liftTcPluginM = forall a. TcPluginM a -> TcPluginM 'Init a
TcPluginInitM
unsafeWithRunInTcM :: forall b.
((forall a. TcPluginM 'Init a -> TcM a) -> TcM b)
-> TcPluginM 'Init b
unsafeWithRunInTcM (forall a. TcPluginM 'Init a -> TcM a) -> TcM b
runInTcM
= forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Init a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
( GHC.runTcPluginM . tcPluginInitM )
#else
( ( forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` ( forall a. HasCallStack => [Char] -> a
error [Char]
"tcPluginInit: cannot access EvBindsVar" ) ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TcPluginM 'Init a -> TcPluginM a
tcPluginInitM )
#endif
instance MonadTcPlugin ( TcPluginM Solve ) where
liftTcPluginM :: forall a. TcPluginM a -> TcPluginM 'Solve a
liftTcPluginM = forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
#ifdef HAS_DERIVEDS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ TcPluginM a
ma BuiltinDefs
_defs EvBindsVar
_evBinds [Ct]
_deriveds -> TcPluginM a
ma )
#else
. ( \ ma _defs _evBinds -> ma )
#endif
unsafeWithRunInTcM :: forall b.
((forall a. TcPluginM 'Solve a -> TcM a) -> TcM b)
-> TcPluginM 'Solve b
unsafeWithRunInTcM (forall a. TcPluginM 'Solve a -> TcM a) -> TcM b
runInTcM
= forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
\ BuiltinDefs
builtinDefs
EvBindsVar
evBinds
#ifdef HAS_DERIVEDS
[Ct]
deriveds
#endif
->
forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Solve a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
( GHC.runTcPluginM
. ( \ f -> f builtinDefs evBinds )
. tcPluginSolveM )
#else
( ( forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` EvBindsVar
evBinds )
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
f -> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
f BuiltinDefs
builtinDefs EvBindsVar
evBinds [Ct]
deriveds )
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
TcPluginM 'Solve a
-> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
tcPluginSolveM
)
#endif
instance MonadTcPlugin ( TcPluginM Rewrite ) where
liftTcPluginM :: forall a. TcPluginM a -> TcPluginM 'Rewrite a
liftTcPluginM = forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ TcPluginM a
ma BuiltinDefs
_ RewriteEnv
_ -> TcPluginM a
ma )
unsafeWithRunInTcM :: forall b.
((forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b)
-> TcPluginM 'Rewrite b
unsafeWithRunInTcM (forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b
runInTcM
= forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM \ BuiltinDefs
builtinDefs RewriteEnv
rewriteEnv ->
forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
( GHC.runTcPluginM
#else
( ( forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` ( forall a. HasCallStack => [Char] -> a
error [Char]
"tcPluginRewrite: cannot access EvBindsVar" ) )
#endif
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ BuiltinDefs -> RewriteEnv -> TcPluginM a
f -> BuiltinDefs -> RewriteEnv -> TcPluginM a
f BuiltinDefs
builtinDefs RewriteEnv
rewriteEnv )
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM )
instance MonadTcPlugin ( TcPluginM Stop ) where
liftTcPluginM :: forall a. TcPluginM a -> TcPluginM 'Stop a
liftTcPluginM = forall a. TcPluginM a -> TcPluginM 'Stop a
TcPluginStopM
unsafeWithRunInTcM :: forall b.
((forall a. TcPluginM 'Stop a -> TcM a) -> TcM b)
-> TcPluginM 'Stop b
unsafeWithRunInTcM (forall a. TcPluginM 'Stop a -> TcM a) -> TcM b
runInTcM
= forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM forall a b. (a -> b) -> a -> b
$ (forall a. TcPluginM 'Stop a -> TcM a) -> TcM b
runInTcM
#ifdef HAS_REWRITING
( GHC.runTcPluginM . tcPluginStopM )
#else
( ( forall a. TcPluginM a -> EvBindsVar -> TcM a
`GHC.runTcPluginM` ( forall a. HasCallStack => [Char] -> a
error [Char]
"tcPluginStop: cannot access EvBindsVar" ) ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TcPluginM 'Stop a -> TcPluginM a
tcPluginStopM )
#endif
unsafeLiftThroughTcM :: MonadTcPlugin m => ( GHC.TcM a -> GHC.TcM b ) -> m a -> m b
unsafeLiftThroughTcM :: forall (m :: * -> *) a b.
MonadTcPlugin m =>
(TcM a -> TcM b) -> m a -> m b
unsafeLiftThroughTcM TcM a -> TcM b
f m a
ma = forall (m :: * -> *) b.
MonadTcPlugin m =>
((forall a. m a -> TcM a) -> TcM b) -> m b
unsafeWithRunInTcM \ forall a. m a -> TcM a
runInTcM -> TcM a -> TcM b
f ( forall a. m a -> TcM a
runInTcM m a
ma )
mkTcPlugin
:: TcPlugin
-> GHC.TcPlugin
mkTcPlugin :: TcPlugin -> TcPlugin
mkTcPlugin ( TcPlugin
{ tcPluginInit :: ()
tcPluginInit = TcPluginM 'Init s
tcPluginInit :: TcPluginM Init userDefs
, s -> TcPluginSolver
tcPluginSolve :: s -> TcPluginSolver
tcPluginSolve :: ()
tcPluginSolve
, s -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite :: ()
tcPluginRewrite
, s -> TcPluginM 'Stop ()
tcPluginStop :: s -> TcPluginM 'Stop ()
tcPluginStop :: ()
tcPluginStop
}
) =
GHC.TcPlugin
{ tcPluginInit :: TcPluginM (TcPluginDefs s)
GHC.tcPluginInit = TcPluginM 'Init s -> TcPluginM (TcPluginDefs s)
adaptUserInit TcPluginM 'Init s
tcPluginInit
#ifdef HAS_REWRITING
, GHC.tcPluginSolve = adaptUserSolve tcPluginSolve
, GHC.tcPluginRewrite = adaptUserRewrite tcPluginRewrite
#else
, tcPluginSolve :: TcPluginDefs s -> TcPluginSolver
GHC.tcPluginSolve = (s -> TcPluginSolver)
-> (s -> UniqFM TyCon TcPluginRewriter)
-> TcPluginDefs s
-> TcPluginSolver
adaptUserSolveAndRewrite
s -> TcPluginSolver
tcPluginSolve s -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite
#endif
, tcPluginStop :: TcPluginDefs s -> TcPluginM ()
GHC.tcPluginStop = (s -> TcPluginM 'Stop ()) -> TcPluginDefs s -> TcPluginM ()
adaptUserStop s -> TcPluginM 'Stop ()
tcPluginStop
}
where
adaptUserInit :: TcPluginM Init userDefs -> GHC.TcPluginM ( TcPluginDefs userDefs )
adaptUserInit :: TcPluginM 'Init s -> TcPluginM (TcPluginDefs s)
adaptUserInit TcPluginM 'Init s
userInit = do
BuiltinDefs
tcPluginBuiltinDefs <- TcPluginM BuiltinDefs
initBuiltinDefs
s
tcPluginUserDefs <- forall a. TcPluginM 'Init a -> TcPluginM a
tcPluginInitM TcPluginM 'Init s
userInit
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( TcPluginDefs { BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs, s
tcPluginUserDefs :: s
tcPluginUserDefs :: s
tcPluginUserDefs })
#ifdef HAS_REWRITING
adaptUserSolve :: ( userDefs -> TcPluginSolver )
-> TcPluginDefs userDefs
-> GHC.TcPluginSolver
adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )
= \ evBindsVar givens wanteds -> do
tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds )
tcPluginBuiltinDefs evBindsVar
adaptUserRewrite :: ( userDefs -> GHC.UniqFM GHC.TyCon TcPluginRewriter )
-> TcPluginDefs userDefs -> GHC.UniqFM GHC.TyCon GHC.TcPluginRewriter
adaptUserRewrite userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs })
= fmap
( \ userRewriter rewriteEnv givens tys ->
tcPluginRewriteM ( userRewriter givens tys ) tcPluginBuiltinDefs rewriteEnv
)
( userRewrite tcPluginUserDefs )
#else
adaptUserSolveAndRewrite
:: ( userDefs -> TcPluginSolver )
-> ( userDefs -> GHC.UniqFM
#if MIN_VERSION_ghc(9,0,0)
GHC.TyCon
#endif
TcPluginRewriter
)
-> TcPluginDefs userDefs
-> GHC.TcPluginSolver
adaptUserSolveAndRewrite :: (s -> TcPluginSolver)
-> (s -> UniqFM TyCon TcPluginRewriter)
-> TcPluginDefs s
-> TcPluginSolver
adaptUserSolveAndRewrite s -> TcPluginSolver
userSolve s -> UniqFM TyCon TcPluginRewriter
userRewrite ( TcPluginDefs { s
tcPluginUserDefs :: s
tcPluginUserDefs :: forall s. TcPluginDefs s -> s
tcPluginUserDefs, BuiltinDefs
tcPluginBuiltinDefs :: BuiltinDefs
tcPluginBuiltinDefs :: forall s. TcPluginDefs s -> BuiltinDefs
tcPluginBuiltinDefs } )
= \ [Ct]
givens [Ct]
deriveds [Ct]
wanteds -> do
EvBindsVar
evBindsVar <- TcPluginM EvBindsVar
GHC.getEvBindsTcPluginM
[Ct]
-> [Ct]
-> [Ct]
-> Rewriters
-> ([Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult)
-> TcPluginM TcPluginResult
shimRewriter
[Ct]
givens [Ct]
deriveds [Ct]
wanteds
( forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
( \ TcPluginRewriter
userRewriter RewriteEnv
rewriteEnv [Ct]
gs [Type]
tys ->
forall a.
TcPluginM 'Rewrite a -> BuiltinDefs -> RewriteEnv -> TcPluginM a
tcPluginRewriteM ( TcPluginRewriter
userRewriter [Ct]
gs [Type]
tys )
BuiltinDefs
tcPluginBuiltinDefs RewriteEnv
rewriteEnv
)
( s -> UniqFM TyCon TcPluginRewriter
userRewrite s
tcPluginUserDefs )
)
( \ [Ct]
gs [Ct]
ds [Ct]
ws ->
forall a.
TcPluginM 'Solve a
-> BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a
tcPluginSolveM ( s -> TcPluginSolver
userSolve s
tcPluginUserDefs [Ct]
gs [Ct]
ws )
BuiltinDefs
tcPluginBuiltinDefs EvBindsVar
evBindsVar [Ct]
ds
)
#endif
adaptUserStop :: ( userDefs -> TcPluginM Stop () ) -> TcPluginDefs userDefs -> GHC.TcPluginM ()
adaptUserStop :: (s -> TcPluginM 'Stop ()) -> TcPluginDefs s -> TcPluginM ()
adaptUserStop s -> TcPluginM 'Stop ()
userStop ( TcPluginDefs { s
tcPluginUserDefs :: s
tcPluginUserDefs :: forall s. TcPluginDefs s -> s
tcPluginUserDefs } ) =
forall a. TcPluginM 'Stop a -> TcPluginM a
tcPluginStopM forall a b. (a -> b) -> a -> b
$ s -> TcPluginM 'Stop ()
userStop s
tcPluginUserDefs
class MonadTcPlugin m => MonadTcPluginWork m where
{-# MINIMAL #-}
askBuiltins :: m BuiltinDefs
askBuiltins = forall a. HasCallStack => [Char] -> a
error [Char]
"askBuiltins: no default implementation"
instance MonadTcPluginWork ( TcPluginM Solve ) where
askBuiltins :: TcPluginM 'Solve BuiltinDefs
askBuiltins = forall a.
(BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a)
-> TcPluginM 'Solve a
TcPluginSolveM
\ BuiltinDefs
builtinDefs
EvBindsVar
_evBinds
#ifdef HAS_DERIVEDS
[Ct]
_deriveds
#endif
-> forall (f :: * -> *) a. Applicative f => a -> f a
pure BuiltinDefs
builtinDefs
instance MonadTcPluginWork ( TcPluginM Rewrite ) where
askBuiltins :: TcPluginM 'Rewrite BuiltinDefs
askBuiltins = forall a.
(BuiltinDefs -> RewriteEnv -> TcPluginM a) -> TcPluginM 'Rewrite a
TcPluginRewriteM \ BuiltinDefs
builtinDefs RewriteEnv
_evBinds -> forall (f :: * -> *) a. Applicative f => a -> f a
pure BuiltinDefs
builtinDefs
instance TypeError ( 'Text "Cannot emit new work in 'tcPluginInit'." )
=> MonadTcPluginWork ( TcPluginM Init ) where
askBuiltins :: TcPluginM 'Init BuiltinDefs
askBuiltins = forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot emit new work in 'tcPluginInit'."
instance TypeError ( 'Text "Cannot emit new work in 'tcPluginStop'." )
=> MonadTcPluginWork ( TcPluginM Stop ) where
askBuiltins :: TcPluginM 'Stop BuiltinDefs
askBuiltins = forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot emit new work in 'tcPluginStop'."
data TcPluginErrorMessage
= Txt !String
| PrintType !GHC.Type
| (:|:) !TcPluginErrorMessage !TcPluginErrorMessage
| (:-:) !TcPluginErrorMessage !TcPluginErrorMessage
infixl 5 :|:
infixl 6 :-:
mkTcPluginErrorTy :: MonadTcPluginWork m => TcPluginErrorMessage -> m GHC.PredType
mkTcPluginErrorTy :: forall (m :: * -> *).
MonadTcPluginWork m =>
TcPluginErrorMessage -> m Type
mkTcPluginErrorTy TcPluginErrorMessage
msg = do
builtinDefs :: BuiltinDefs
builtinDefs@( BuiltinDefs { TyCon
typeErrorTyCon :: BuiltinDefs -> TyCon
typeErrorTyCon :: TyCon
typeErrorTyCon } ) <- forall (m :: * -> *). MonadTcPluginWork m => m BuiltinDefs
askBuiltins
let
errorMsgTy :: GHC.PredType
errorMsgTy :: Type
errorMsgTy = BuiltinDefs -> TcPluginErrorMessage -> Type
interpretErrorMessage BuiltinDefs
builtinDefs TcPluginErrorMessage
msg
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
typeErrorTyCon [ Type
GHC.constraintKind, Type
errorMsgTy ]
instance ( Monad (TcPluginM s), MonadTcPlugin (TcPluginM s) )
=> MonadThings (TcPluginM s) where
lookupThing :: Name -> TcPluginM s TyThing
lookupThing = forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadThings m => Name -> m TyThing
lookupThing
data BuiltinDefs =
BuiltinDefs
{ BuiltinDefs -> TyCon
typeErrorTyCon :: !GHC.TyCon
, BuiltinDefs -> TyCon
textTyCon :: !GHC.TyCon
, BuiltinDefs -> TyCon
showTypeTyCon :: !GHC.TyCon
, BuiltinDefs -> TyCon
concatTyCon :: !GHC.TyCon
, BuiltinDefs -> TyCon
vcatTyCon :: !GHC.TyCon
}
data TcPluginDefs s
= TcPluginDefs
{ forall s. TcPluginDefs s -> BuiltinDefs
tcPluginBuiltinDefs :: !BuiltinDefs
, forall s. TcPluginDefs s -> s
tcPluginUserDefs :: !s
}
initBuiltinDefs :: GHC.TcPluginM BuiltinDefs
initBuiltinDefs :: TcPluginM BuiltinDefs
initBuiltinDefs = do
TyCon
typeErrorTyCon <- Name -> TcPluginM TyCon
GHC.tcLookupTyCon Name
GHC.TypeLits.errorMessageTypeErrorFamName
TyCon
textTyCon <- DataCon -> TyCon
GHC.promoteDataCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM DataCon
GHC.tcLookupDataCon Name
GHC.TypeLits.typeErrorTextDataConName
TyCon
showTypeTyCon <- DataCon -> TyCon
GHC.promoteDataCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM DataCon
GHC.tcLookupDataCon Name
GHC.TypeLits.typeErrorShowTypeDataConName
TyCon
concatTyCon <- DataCon -> TyCon
GHC.promoteDataCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM DataCon
GHC.tcLookupDataCon Name
GHC.TypeLits.typeErrorAppendDataConName
TyCon
vcatTyCon <- DataCon -> TyCon
GHC.promoteDataCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM DataCon
GHC.tcLookupDataCon Name
GHC.TypeLits.typeErrorVAppendDataConName
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( BuiltinDefs { TyCon
vcatTyCon :: TyCon
concatTyCon :: TyCon
showTypeTyCon :: TyCon
textTyCon :: TyCon
typeErrorTyCon :: TyCon
vcatTyCon :: TyCon
concatTyCon :: TyCon
showTypeTyCon :: TyCon
textTyCon :: TyCon
typeErrorTyCon :: TyCon
.. } )
interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> GHC.PredType
interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> Type
interpretErrorMessage ( BuiltinDefs { TyCon
vcatTyCon :: TyCon
concatTyCon :: TyCon
showTypeTyCon :: TyCon
textTyCon :: TyCon
typeErrorTyCon :: TyCon
vcatTyCon :: BuiltinDefs -> TyCon
concatTyCon :: BuiltinDefs -> TyCon
showTypeTyCon :: BuiltinDefs -> TyCon
textTyCon :: BuiltinDefs -> TyCon
typeErrorTyCon :: BuiltinDefs -> TyCon
.. } ) = TcPluginErrorMessage -> Type
go
where
go :: TcPluginErrorMessage -> GHC.PredType
go :: TcPluginErrorMessage -> Type
go ( Txt [Char]
str ) =
TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
textTyCon [ TyLit -> Type
GHC.LitTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. FastString -> TyLit
GHC.StrTyLit forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> FastString
GHC.fsLit forall a b. (a -> b) -> a -> b
$ [Char]
str ]
go ( PrintType Type
ty ) =
TyCon -> [Type] -> Type
GHC.mkTyConApp TyCon
showTypeTyCon [ HasDebugCallStack => Type -> Type
GHC.typeKind Type
ty, Type
ty ]
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 ]