{-# LANGUAGE CPP             #-}
{-# LANGUAGE RecordWildCards #-}
-- | A type-checker plugin for 'Unsatisfiable.Class.Unsatisfiable' type class.
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
-------------------------------------------------------------------------------

-- | To use this plugin add
--
-- @
-- \{-# OPTIONS_GHC -fplugin=Unsatisfiable #-}
-- @
--
-- to your source file.
--
-- This plugin does two things:
--
-- Firstly, when there is /wanted/ 'Unsatisfiable.Class.Unsatisfiable' constraint,
-- we pretty-pring its message.
-- Unfortunately the actual @No instance for (Unsatisfiable msg)@
-- error is also printed, as we don't solve it, except when
-- @-fdefer-type-errors@ is enabled.
-- In that case 'Unsatifiable.Class.unsatisfiable' will throw an error with
-- the rendered message.
--
-- Secondly, when 'Unsatisfiable.Class.Unsatisfiable' constraint is given,
-- all other constraints are solved automatically using 'unsatisfiable'
-- as the evidence. This is useful
--
-- @
-- class C a => D a
-- instance Unsatisfiable Msg => D Int  -- Note absence of C Int in the context
-- @
--
-- The motivation here is that if we use 'Unsatisifable.Class.Unsatisfiable' to
-- ban an instance with a nice error message, we don't want to get extra error
-- messages arising from failure to solve the superclass constraints, which we
-- get if we are obliged to use
--
-- @
-- instance (Unsatisfiable Msg, C Int) => D Int
-- @
--
-- When GHC looks for valid type hole fits this plugin might print some errors.
-- You may disable them with @-fno-show-valid-hole-fits@ ghc option.
--
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 ())
    }

-------------------------------------------------------------------------------
-- Ctx
-------------------------------------------------------------------------------

data PluginCtx = PluginCtx
    { PluginCtx -> Class
unsatisfiableCls  :: GHC.Class
    , PluginCtx -> Id
unsatisfiableExpr :: GHC.Var
    }

-------------------------------------------------------------------------------
-- Plugin functions
-------------------------------------------------------------------------------

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
    -- acquire context
    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 us see if there is Unsatisfiable constraint in givens.
    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
        -- there is given unsatisfiable.
        -- Jackpot, we can conjure everything.
        --
        -- we make evidence using (unexported) unsafistiable_
        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

            -- return solveds
            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 []

        -- ... otherwise
        --
        -- we traverse wanteds, and if there is Unsafistifiable
        -- we pretty-print its message
        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

                -- return solveds
                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

                -- in this case we don't solve anything.
                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 =
    -- same trick as evDelayedError
    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)"


-- | Is the constraint a @Unsatisfiable msg@, if so, return @Just msg@.
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

-------------------------------------------------------------------------------
-- Diagnostics
-------------------------------------------------------------------------------

#if MIN_VERSION_ghc(9,0,0)
#define ERR_STYLE
#else
#define ERR_STYLE (GHC.defaultErrStyle dflags)
#endif

debug :: Monad m => m () -> m ()
-- debug x = x
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

-------------------------------------------------------------------------------
-- Names
-------------------------------------------------------------------------------

unsatisfiableClassMN :: GHC.ModuleName
unsatisfiableClassMN :: ModuleName
unsatisfiableClassMN =  CommandLineOption -> ModuleName
GHC.mkModuleName CommandLineOption
"Unsatisfiable.Class"

-------------------------------------------------------------------------------
-- Utils
-------------------------------------------------------------------------------

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)