{-# LANGUAGE CPP #-}
{-# LANGUAGE RecordWildCards #-}
module Unsatisfiable.Plugin (
plugin,
) where
import Control.Monad (forM_)
import Control.Monad.IO.Class (MonadIO (..))
import Data.Functor ((<&>))
import Data.Maybe (listToMaybe)
import qualified GHC
import qualified GHC.Builtin.Types as GHC
import qualified GHC.Core as GHC
import qualified GHC.Core.Class as GHC
import qualified GHC.Core.Make as GHC
import qualified GHC.Core.TyCon as GHC
import qualified GHC.Core.Type as GHC
import qualified GHC.Driver.Session as GHC
import qualified GHC.Tc.Types as GHC
import qualified GHC.Tc.Types.Constraint as GHC
import qualified GHC.Tc.Types.Evidence as GHC
import qualified GHC.Tc.Utils.Monad as GHC
import qualified GHC.Types.Id as GHC
import qualified GHC.Types.Literal as GHC
import qualified GHC.Types.Name as GHC
import qualified GHC.Types.Var as GHC
import qualified GHC.Utils.Outputable as GHC
#if MIN_VERSION_ghc(9,0,0)
import qualified GHC.Plugins as Plugins
import qualified GHC.Tc.Plugin as Plugins
#else
import qualified GhcPlugins as Plugins
import qualified TcPluginM as Plugins
#endif
plugin :: Plugins.Plugin
plugin :: Plugin
plugin = Plugin
Plugins.defaultPlugin
{ tcPlugin :: TcPlugin
Plugins.tcPlugin = \[CommandLineOption]
_args -> TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
Just TcPlugin
tcPlugin
, pluginRecompile :: [CommandLineOption] -> IO PluginRecompile
Plugins.pluginRecompile = [CommandLineOption] -> IO PluginRecompile
Plugins.purePlugin
}
tcPlugin :: GHC.TcPlugin
tcPlugin :: TcPlugin
tcPlugin = TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
GHC.TcPlugin
{ tcPluginInit :: TcPluginM PluginCtx
GHC.tcPluginInit = TcPluginM PluginCtx
tcPluginInit
, tcPluginSolve :: PluginCtx -> TcPluginSolver
GHC.tcPluginSolve = PluginCtx -> TcPluginSolver
tcPluginSolve
, tcPluginStop :: PluginCtx -> TcPluginM ()
GHC.tcPluginStop = TcPluginM () -> PluginCtx -> TcPluginM ()
forall a b. a -> b -> a
const (() -> TcPluginM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
}
data PluginCtx = PluginCtx
{ PluginCtx -> Class
unsatisfiableCls :: GHC.Class
, PluginCtx -> Id
unsatisfiableExpr :: GHC.Var
}
tcPluginInit :: GHC.TcPluginM PluginCtx
tcPluginInit :: TcPluginM PluginCtx
tcPluginInit = do
TcPluginM () -> TcPluginM ()
forall (m :: * -> *). Monad m => m () -> m ()
debug (TcPluginM () -> TcPluginM ()) -> TcPluginM () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn CommandLineOption
"INITIALIZING UNSATISFIABLE PLUGIN"
DynFlags
dflags <- TcM DynFlags -> TcPluginM DynFlags
forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM TcM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
GHC.getDynFlags
let findModule :: GHC.ModuleName -> Plugins.TcPluginM GHC.Module
findModule :: ModuleName -> TcPluginM Module
findModule ModuleName
m = do
FindResult
im <- ModuleName -> Maybe FastString -> TcPluginM FindResult
Plugins.findImportedModule ModuleName
m Maybe FastString
forall a. Maybe a
Nothing
case FindResult
im of
Plugins.Found ModLocation
_ Module
md -> Module -> TcPluginM Module
forall (m :: * -> *) a. Monad m => a -> m a
return Module
md
FindResult
_ -> do
IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> SrcSpan -> SDoc -> IO ()
forall (m :: * -> *).
MonadIO m =>
DynFlags -> SrcSpan -> SDoc -> m ()
putError DynFlags
dflags SrcSpan
GHC.noSrcSpan (SDoc -> IO ()) -> SDoc -> IO ()
forall a b. (a -> b) -> a -> b
$
CommandLineOption -> SDoc
GHC.text CommandLineOption
"Cannot find module" SDoc -> SDoc -> SDoc
GHC.<+> ModuleName -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr ModuleName
m
CommandLineOption -> TcPluginM Module
forall (m :: * -> *) a. MonadFail m => CommandLineOption -> m a
fail CommandLineOption
"panic!"
Module
md <- ModuleName -> TcPluginM Module
findModule ModuleName
unsatisfiableClassMN
Class
unsatisfiableCls <- do
Name
name <- Module -> OccName -> TcPluginM Name
Plugins.lookupOrig Module
md (CommandLineOption -> OccName
GHC.mkTcOcc CommandLineOption
"Unsatisfiable")
Name -> TcPluginM Class
Plugins.tcLookupClass Name
name
Id
unsatisfiableExpr <- do
Name
name <- Module -> OccName -> TcPluginM Name
Plugins.lookupOrig Module
md (CommandLineOption -> OccName
GHC.mkVarOcc CommandLineOption
"unsatisfiable_")
Name -> TcPluginM Id
Plugins.tcLookupId Name
name
TcPluginM () -> TcPluginM ()
forall (m :: * -> *). Monad m => m () -> m ()
debug (TcPluginM () -> TcPluginM ()) -> TcPluginM () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ do
IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
GHC.showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ Class -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Class
unsatisfiableCls
IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
GHC.showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ Id -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Id
unsatisfiableExpr
IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
GHC.showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ Scaled Type -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr (Scaled Type -> SDoc) -> Scaled Type -> SDoc
forall a b. (a -> b) -> a -> b
$ Id -> Scaled Type
GHC.idScaledType Id
unsatisfiableExpr
PluginCtx -> TcPluginM PluginCtx
forall (m :: * -> *) a. Monad m => a -> m a
return PluginCtx :: Class -> Id -> PluginCtx
PluginCtx {Class
Id
unsatisfiableExpr :: Id
unsatisfiableCls :: Class
unsatisfiableExpr :: Id
unsatisfiableCls :: Class
..}
tcPluginSolve :: PluginCtx -> GHC.TcPluginSolver
tcPluginSolve :: PluginCtx -> TcPluginSolver
tcPluginSolve PluginCtx
ctx [Ct]
givens [Ct]
_deriveds [Ct]
wanteds = do
DynFlags
dflags <- TcM DynFlags -> TcPluginM DynFlags
forall a. TcM a -> TcPluginM a
Plugins.unsafeTcPluginTcM TcM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
GHC.getDynFlags
let defer_errors :: Bool
defer_errors = GeneralFlag -> DynFlags -> Bool
GHC.gopt GeneralFlag
GHC.Opt_DeferTypeErrors DynFlags
dflags
let givenUnsatisfiable :: Maybe (GHC.Ct, GHC.Type)
givenUnsatisfiable :: Maybe (Ct, Type)
givenUnsatisfiable = [(Ct, Type)] -> Maybe (Ct, Type)
forall a. [a] -> Maybe a
listToMaybe
[ (Ct
ct, Type
ty)
| Ct
ct <- [Ct]
givens
, Just Type
ty <- Maybe Type -> [Maybe Type]
forall (m :: * -> *) a. Monad m => a -> m a
return (PluginCtx -> Ct -> Maybe Type
isUnsatisfiable PluginCtx
ctx Ct
ct)
]
TcPluginM () -> TcPluginM ()
forall (m :: * -> *). Monad m => m () -> m ()
debug (TcPluginM () -> TcPluginM ()) -> TcPluginM () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
GHC.showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> SDoc
GHC.text CommandLineOption
"givenUnsatisfiable =" SDoc -> SDoc -> SDoc
GHC.<+> Maybe (Ct, Type) -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Maybe (Ct, Type)
givenUnsatisfiable
case Maybe (Ct, Type)
givenUnsatisfiable of
Just (Ct
ctUnsatisfiable, Type
msg) -> do
let expr :: GHC.Type -> GHC.EvTerm
expr :: Type -> EvTerm
expr = PluginCtx -> Type -> Ct -> Type -> EvTerm
evUnsatisfiable PluginCtx
ctx Type
msg Ct
ctUnsatisfiable
let solved :: [(GHC.EvTerm, GHC.Ct)]
solved :: [(EvTerm, Ct)]
solved =
[ (Type -> EvTerm
expr (CtEvidence -> Type
GHC.ctev_pred (Ct -> CtEvidence
GHC.ctEvidence Ct
ct)), Ct
ct)
| Ct
ct <- [Ct]
wanteds
]
TcPluginM () -> TcPluginM ()
forall (m :: * -> *). Monad m => m () -> m ()
debug (TcPluginM () -> TcPluginM ()) -> TcPluginM () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ do
[Ct] -> (Ct -> TcPluginM ()) -> TcPluginM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Ct]
wanteds ((Ct -> TcPluginM ()) -> TcPluginM ())
-> (Ct -> TcPluginM ()) -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ \Ct
ct -> IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ do
CommandLineOption -> IO ()
putStrLn (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
GHC.showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ Ct -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Ct
ct
CommandLineOption -> IO ()
putStrLn (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
GHC.showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ Type -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr (Type -> SDoc) -> Type -> SDoc
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
GHC.ctev_pred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
GHC.ctEvidence Ct
ct
[(EvTerm, Ct)] -> ((EvTerm, Ct) -> TcPluginM ()) -> TcPluginM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(EvTerm, Ct)]
solved (((EvTerm, Ct) -> TcPluginM ()) -> TcPluginM ())
-> ((EvTerm, Ct) -> TcPluginM ()) -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ \(EvTerm
t, Ct
_) -> IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ do
CommandLineOption -> IO ()
putStrLn (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
GHC.showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr EvTerm
t
TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
GHC.TcPluginOk [(EvTerm, Ct)]
solved []
Maybe (Ct, Type)
Nothing
| Bool
defer_errors -> do
let solved' :: [(Plugins.TcPluginM GHC.EvTerm, GHC.Ct)]
solved' :: [(TcPluginM EvTerm, Ct)]
solved' =
[ (PluginCtx -> DynFlags -> Type -> RealSrcSpan -> TcPluginM EvTerm
evDeferredUnsatisfiable PluginCtx
ctx DynFlags
dflags Type
msg (CtLoc -> RealSrcSpan
GHC.ctLocSpan (CtLoc -> RealSrcSpan) -> CtLoc -> RealSrcSpan
forall a b. (a -> b) -> a -> b
$ Ct -> CtLoc
GHC.ctLoc Ct
ct), Ct
ct)
| Ct
ct <- [Ct]
wanteds
, Just Type
msg <- Maybe Type -> [Maybe Type]
forall (m :: * -> *) a. Monad m => a -> m a
return (PluginCtx -> Ct -> Maybe Type
isUnsatisfiable PluginCtx
ctx Ct
ct)
]
[(EvTerm, Ct)]
solved <- (((TcPluginM EvTerm, Ct) -> TcPluginM (EvTerm, Ct))
-> [(TcPluginM EvTerm, Ct)] -> TcPluginM [(EvTerm, Ct)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (((TcPluginM EvTerm, Ct) -> TcPluginM (EvTerm, Ct))
-> [(TcPluginM EvTerm, Ct)] -> TcPluginM [(EvTerm, Ct)])
-> ((TcPluginM EvTerm -> TcPluginM EvTerm)
-> (TcPluginM EvTerm, Ct) -> TcPluginM (EvTerm, Ct))
-> (TcPluginM EvTerm -> TcPluginM EvTerm)
-> [(TcPluginM EvTerm, Ct)]
-> TcPluginM [(EvTerm, Ct)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TcPluginM EvTerm -> TcPluginM EvTerm)
-> (TcPluginM EvTerm, Ct) -> TcPluginM (EvTerm, Ct)
forall (f :: * -> *) a c b.
Functor f =>
(a -> f c) -> (a, b) -> f (c, b)
_1) TcPluginM EvTerm -> TcPluginM EvTerm
forall a. a -> a
id [(TcPluginM EvTerm, Ct)]
solved'
TcPluginM () -> TcPluginM ()
forall (m :: * -> *). Monad m => m () -> m ()
debug (TcPluginM () -> TcPluginM ()) -> TcPluginM () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ do
[(EvTerm, Ct)] -> ((EvTerm, Ct) -> TcPluginM ()) -> TcPluginM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(EvTerm, Ct)]
solved (((EvTerm, Ct) -> TcPluginM ()) -> TcPluginM ())
-> ((EvTerm, Ct) -> TcPluginM ()) -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ \(EvTerm
t, Ct
_) -> IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ do
CommandLineOption -> IO ()
putStrLn (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
GHC.showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr EvTerm
t
TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
GHC.TcPluginOk [(EvTerm, Ct)]
solved []
| Bool
otherwise -> do
[Ct] -> (Ct -> TcPluginM ()) -> TcPluginM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Ct]
wanteds ((Ct -> TcPluginM ()) -> TcPluginM ())
-> (Ct -> TcPluginM ()) -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ \Ct
ct -> Maybe Type -> (Type -> TcPluginM ()) -> TcPluginM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (PluginCtx -> Ct -> Maybe Type
isUnsatisfiable PluginCtx
ctx Ct
ct) ((Type -> TcPluginM ()) -> TcPluginM ())
-> (Type -> TcPluginM ()) -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ \Type
ty -> IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
Plugins.tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ do
DynFlags -> SrcSpan -> SDoc -> IO ()
forall (m :: * -> *).
MonadIO m =>
DynFlags -> SrcSpan -> SDoc -> m ()
putError DynFlags
dflags (RealSrcSpan -> Maybe BufSpan -> SrcSpan
GHC.RealSrcSpan (CtLoc -> RealSrcSpan
GHC.ctLocSpan (CtLoc -> RealSrcSpan) -> CtLoc -> RealSrcSpan
forall a b. (a -> b) -> a -> b
$ Ct -> CtLoc
GHC.ctLoc Ct
ct) Maybe BufSpan
forall a. Maybe a
Nothing) (SDoc -> IO ()) -> SDoc -> IO ()
forall a b. (a -> b) -> a -> b
$
CommandLineOption -> SDoc
GHC.text CommandLineOption
"Unsatisfiable:" SDoc -> SDoc -> SDoc
GHC.$$
Type -> SDoc
GHC.pprUserTypeErrorTy Type
ty
TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
GHC.TcPluginOk [] []
evUnsatisfiable :: PluginCtx -> GHC.Type -> GHC.Ct -> GHC.Type -> GHC.EvTerm
evUnsatisfiable :: PluginCtx -> Type -> Ct -> Type -> EvTerm
evUnsatisfiable PluginCtx
ctx Type
msg Ct
ct Type
ty =
EvExpr -> EvTerm
GHC.EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ EvExpr -> Scaled Type -> Type -> [CoreAlt] -> EvExpr
GHC.mkWildCase EvExpr
forall {b}. Expr b
expr (Type -> Scaled Type
forall a. a -> Scaled a
GHC.unrestricted Type
GHC.unitTy) Type
ty []
where
expr :: Expr b
expr = Id -> Expr b
forall b. Id -> Expr b
GHC.Var (PluginCtx -> Id
unsatisfiableExpr PluginCtx
ctx)
Expr b -> [Type] -> Expr b
forall b. Expr b -> [Type] -> Expr b
`GHC.mkTyApps` [Type
msg]
Expr b -> [Expr b] -> Expr b
forall b. Expr b -> [Expr b] -> Expr b
`GHC.mkApps` [ Id -> Expr b
forall b. Id -> Expr b
GHC.Var (Ct -> Id
GHC.ctEvId Ct
ct) ]
Expr b -> [Type] -> Expr b
forall b. Expr b -> [Type] -> Expr b
`GHC.mkTyApps` [Type
GHC.unitTy]
evDeferredUnsatisfiable :: PluginCtx -> GHC.DynFlags -> GHC.Type -> Plugins.RealSrcSpan -> Plugins.TcPluginM GHC.EvTerm
evDeferredUnsatisfiable :: PluginCtx -> DynFlags -> Type -> RealSrcSpan -> TcPluginM EvTerm
evDeferredUnsatisfiable PluginCtx
ctx DynFlags
dflags Type
msg RealSrcSpan
loc = do
Id
v <- CommandLineOption -> Type -> TcPluginM Id
makeTyVar CommandLineOption
"a" Type
GHC.liftedTypeKind
EvTerm -> TcPluginM EvTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (EvTerm -> TcPluginM EvTerm) -> EvTerm -> TcPluginM EvTerm
forall a b. (a -> b) -> a -> b
$ EvExpr -> EvTerm
GHC.EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ Id -> EvExpr
appDc Id
v
where
cls :: Class
cls = PluginCtx -> Class
unsatisfiableCls PluginCtx
ctx
tyCon :: TyCon
tyCon = Class -> TyCon
GHC.classTyCon Class
cls
dc :: DataCon
dc = TyCon -> DataCon
GHC.tyConSingleDataCon TyCon
tyCon
appDc :: Id -> EvExpr
appDc Id
v = DataCon -> [EvExpr] -> EvExpr
GHC.mkCoreConApps DataCon
dc
[ Type -> EvExpr
forall b. Type -> Expr b
GHC.Type Type
msg
, [Id] -> EvExpr -> EvExpr
GHC.mkCoreLams [Id
v] (Type -> EvExpr
forall b. Type -> Expr b
err (Type -> EvExpr) -> Type -> EvExpr
forall a b. (a -> b) -> a -> b
$ Id -> Type
GHC.mkTyVarTy Id
v)
]
err :: Type -> Expr b
err Type
ty = Id -> Expr b
forall b. Id -> Expr b
GHC.Var Id
GHC.tYPE_ERROR_ID
Expr b -> [Type] -> Expr b
forall b. Expr b -> [Type] -> Expr b
`GHC.mkTyApps` [HasDebugCallStack => Type -> Type
Type -> Type
GHC.getRuntimeRep Type
ty, Type
ty]
Expr b -> [Expr b] -> Expr b
forall b. Expr b -> [Expr b] -> Expr b
`GHC.mkApps` [Expr b
forall {b}. Expr b
litMsg]
litMsg :: Expr b
litMsg = Literal -> Expr b
forall b. Literal -> Expr b
GHC.Lit (Literal -> Expr b) -> Literal -> Expr b
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> Literal
GHC.mkLitString (CommandLineOption -> Literal) -> CommandLineOption -> Literal
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
GHC.showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$
CommandLineOption -> SDoc
GHC.text CommandLineOption
"Unsatisfiable at " SDoc -> SDoc -> SDoc
GHC.<+> RealSrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr RealSrcSpan
loc SDoc -> SDoc -> SDoc
GHC.$$
Type -> SDoc
GHC.pprUserTypeErrorTy Type
msg SDoc -> SDoc -> SDoc
GHC.$$
CommandLineOption -> SDoc
GHC.text CommandLineOption
"(deferred unsatisfiable type error)"
isUnsatisfiable :: PluginCtx -> GHC.Ct -> Maybe GHC.Type
isUnsatisfiable :: PluginCtx -> Ct -> Maybe Type
isUnsatisfiable PluginCtx
ctx (GHC.CDictCan CtEvidence
_ev Class
cls [Type
ty] Bool
_pend_sc)
| Class
cls Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== PluginCtx -> Class
unsatisfiableCls PluginCtx
ctx
= Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
isUnsatisfiable PluginCtx
_ Ct
_ = Maybe Type
forall a. Maybe a
Nothing
#if MIN_VERSION_ghc(9,0,0)
#define ERR_STYLE
#else
#define ERR_STYLE (GHC.defaultErrStyle dflags)
#endif
debug :: Monad m => m () -> m ()
debug :: forall (m :: * -> *). Monad m => m () -> m ()
debug m ()
_ = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
putError :: MonadIO m => GHC.DynFlags -> GHC.SrcSpan -> GHC.SDoc -> m ()
putError :: forall (m :: * -> *).
MonadIO m =>
DynFlags -> SrcSpan -> SDoc -> m ()
putError DynFlags
dflags SrcSpan
l SDoc
doc =
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> WarnReason -> Severity -> SrcSpan -> SDoc -> IO ()
GHC.putLogMsg DynFlags
dflags WarnReason
GHC.NoReason Severity
GHC.SevError SrcSpan
l ERR_STYLE doc
unsatisfiableClassMN :: GHC.ModuleName
unsatisfiableClassMN :: ModuleName
unsatisfiableClassMN = CommandLineOption -> ModuleName
GHC.mkModuleName CommandLineOption
"Unsatisfiable.Class"
makeTyVar :: String -> GHC.Kind -> Plugins.TcPluginM GHC.TyVar
makeTyVar :: CommandLineOption -> Type -> TcPluginM Id
makeTyVar CommandLineOption
n Type
ki = do
Name
name <- TcM Name -> TcPluginM Name
forall a. TcM a -> TcPluginM a
GHC.unsafeTcPluginTcM (TcM Name -> TcPluginM Name) -> TcM Name -> TcPluginM Name
forall a b. (a -> b) -> a -> b
$ OccName -> TcM Name
GHC.newName (CommandLineOption -> OccName
GHC.mkTyVarOcc CommandLineOption
n)
Id -> TcPluginM Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> Id
GHC.mkTyVar Name
name Type
ki)
_1 :: Functor f => (a -> f c) -> (a, b) -> f (c, b)
_1 :: forall (f :: * -> *) a c b.
Functor f =>
(a -> f c) -> (a, b) -> f (c, b)
_1 a -> f c
f (a
x, b
y) = a -> f c
f a
x f c -> (c -> (c, b)) -> f (c, b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \c
x' -> (c
x', b
y)