Implement typechecker plugins

Summary:
See https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker

This is based on work by Iavor Diatchki and Eric Seidel.

Test Plan: validate

Reviewers: simonpj, austin

Reviewed By: austin

Subscribers: gridaphobe, yav, thomie, carter

Differential Revision: https://phabricator.haskell.org/D489

Conflicts:
	docs/users_guide/7.10.1-notes.xml

17 files changed, 613 insertions, 113 deletions

diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index 46fdb40369..bfc2e9cf7c 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -318,6 +318,8 @@ Library
         PackageConfig
         Packages
         PlatformConstants
+        Plugins
+        TcPluginM
         PprTyThing
         StaticFlags
         SysTools
diff --git a/compiler/main/DynamicLoading.hs b/compiler/main/DynamicLoading.hs
index 046d13cee5..95321cfb79 100644
--- a/compiler/main/DynamicLoading.hs
+++ b/compiler/main/DynamicLoading.hs
@@ -3,6 +3,9 @@
 -- | Dynamically lookup up values from modules and loading them.
 module DynamicLoading (
 #ifdef GHCI
+        -- * Loading plugins
+        loadPlugins,
+
         -- * Force loading information
         forceLoadModuleInterfaces,
         forceLoadNameModuleInterface,
@@ -25,13 +28,17 @@ import Finder           ( findImportedModule, cannotFindModule )
 import TcRnMonad        ( initTcInteractive, initIfaceTcRn )
 import LoadIface        ( loadPluginInterface )
 import RdrName          ( RdrName, Provenance(..), ImportSpec(..), ImpDeclSpec(..)
-                        , ImpItemSpec(..), mkGlobalRdrEnv, lookupGRE_RdrName, gre_name )
+                        , ImpItemSpec(..), mkGlobalRdrEnv, lookupGRE_RdrName
+                        , gre_name, mkRdrQual )
+import OccName          ( mkVarOcc )
 import RnNames          ( gresFromAvails )
 import DynFlags
+import Plugins          ( Plugin, CommandLineOption )
+import PrelNames        ( pluginTyConName )
 
 import HscTypes
 import BasicTypes       ( HValue )
-import TypeRep          ( pprTyThingCategory )
+import TypeRep          ( mkTyConTy, pprTyThingCategory )
 import Type             ( Type, eqType )
 import TyCon            ( TyCon )
 import Name             ( Name, nameModule_maybe )
@@ -48,6 +55,44 @@ import Data.Maybe        ( mapMaybe )
 import GHC.Exts          ( unsafeCoerce# )
 
 
+loadPlugins :: HscEnv -> IO [(ModuleName, Plugin, [CommandLineOption])]
+loadPlugins hsc_env
+  = do { plugins <- mapM (loadPlugin hsc_env) to_load
+       ; return $ map attachOptions $ to_load `zip` plugins }
+  where
+    dflags  = hsc_dflags hsc_env
+    to_load = pluginModNames dflags
+
+    attachOptions (mod_nm, plug) = (mod_nm, plug, options)
+      where
+        options = [ option | (opt_mod_nm, option) <- pluginModNameOpts dflags
+                            , opt_mod_nm == mod_nm ]
+
+loadPlugin :: HscEnv -> ModuleName -> IO Plugin
+loadPlugin hsc_env mod_name
+  = do { let plugin_rdr_name = mkRdrQual mod_name (mkVarOcc "plugin")
+             dflags = hsc_dflags hsc_env
+       ; mb_name <- lookupRdrNameInModuleForPlugins hsc_env mod_name
+                        plugin_rdr_name
+       ; case mb_name of {
+            Nothing ->
+                throwGhcExceptionIO (CmdLineError $ showSDoc dflags $ hsep
+                          [ ptext (sLit "The module"), ppr mod_name
+                          , ptext (sLit "did not export the plugin name")
+                          , ppr plugin_rdr_name ]) ;
+            Just name ->
+
+     do { plugin_tycon <- forceLoadTyCon hsc_env pluginTyConName
+        ; mb_plugin <- getValueSafely hsc_env name (mkTyConTy plugin_tycon)
+        ; case mb_plugin of
+            Nothing ->
+                throwGhcExceptionIO (CmdLineError $ showSDoc dflags $ hsep
+                          [ ptext (sLit "The value"), ppr name
+                          , ptext (sLit "did not have the type")
+                          , ppr pluginTyConName, ptext (sLit "as required")])
+            Just plugin -> return plugin } } }
+
+
 -- | Force the interfaces for the given modules to be loaded. The 'SDoc' parameter is used
 -- for debugging (@-ddump-if-trace@) only: it is shown as the reason why the module is being loaded.
 forceLoadModuleInterfaces :: HscEnv -> SDoc -> [Module] -> IO ()
diff --git a/compiler/main/GhcPlugins.hs b/compiler/main/GhcPlugins.hs
index 0fc87f0fd0..2b7746c6ce 100644
--- a/compiler/main/GhcPlugins.hs
+++ b/compiler/main/GhcPlugins.hs
@@ -8,9 +8,9 @@
 -- Particularly interesting modules for plugin writers include
 -- "CoreSyn" and "CoreMonad".
 module GhcPlugins(
-        module CoreMonad,
+        module Plugins,
         module RdrName, module OccName, module Name, module Var, module Id, module IdInfo,
-        module CoreSyn, module Literal, module DataCon, 
+        module CoreMonad, module CoreSyn, module Literal, module DataCon,
         module CoreUtils, module MkCore, module CoreFVs, module CoreSubst,
         module Rules, module Annotations,
         module DynFlags, module Packages,
@@ -23,7 +23,7 @@ module GhcPlugins(
     ) where
 
 -- Plugin stuff itself
-import CoreMonad
+import Plugins
 
 -- Variable naming
 import RdrName
@@ -34,6 +34,7 @@ import Id       hiding  ( lazySetIdInfo, setIdExported, setIdNotExported {- all
 import IdInfo
 
 -- Core
+import CoreMonad
 import CoreSyn
 import Literal
 import DataCon
diff --git a/compiler/main/Plugins.hs b/compiler/main/Plugins.hs
new file mode 100644
index 0000000000..d936e288b4
--- /dev/null
+++ b/compiler/main/Plugins.hs
@@ -0,0 +1,38 @@
+module Plugins (
+    Plugin(..), CommandLineOption,
+    defaultPlugin
+    ) where
+
+import CoreMonad ( CoreToDo, CoreM )
+import TcRnTypes ( TcPlugin )
+
+
+-- | Command line options gathered from the -PModule.Name:stuff syntax
+-- are given to you as this type
+type CommandLineOption = String
+
+-- | 'Plugin' is the core compiler plugin data type. Try to avoid
+-- constructing one of these directly, and just modify some fields of
+-- 'defaultPlugin' instead: this is to try and preserve source-code
+-- compatability when we add fields to this.
+--
+-- Nonetheless, this API is preliminary and highly likely to change in
+-- the future.
+data Plugin = Plugin {
+    installCoreToDos :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
+    -- ^ Modify the Core pipeline that will be used for compilation.
+    -- This is called as the Core pipeline is built for every module
+    -- being compiled, and plugins get the opportunity to modify the
+    -- pipeline in a nondeterministic order.
+  , tcPlugin :: [CommandLineOption] -> Maybe TcPlugin
+    -- ^ An optional typechecker plugin, which may modify the
+    -- behaviour of the constraint solver.
+  }
+
+-- | Default plugin: does nothing at all! For compatability reasons
+-- you should base all your plugin definitions on this default value.
+defaultPlugin :: Plugin
+defaultPlugin = Plugin {
+        installCoreToDos = const return
+      , tcPlugin         = const Nothing
+    }
diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs
index 6e40546d2c..e0a5890619 100644
--- a/compiler/prelude/PrelNames.lhs
+++ b/compiler/prelude/PrelNames.lhs
@@ -1161,10 +1161,10 @@ ipClassName :: Name
 ipClassName         = clsQual gHC_IP (fsLit "IP")      ipClassNameKey
 
 -- plugins
-cORE_MONAD :: Module
-cORE_MONAD = mkThisGhcModule (fsLit "CoreMonad")
+pLUGINS :: Module
+pLUGINS = mkThisGhcModule (fsLit "Plugins")
 pluginTyConName :: Name
-pluginTyConName = tcQual cORE_MONAD (fsLit "Plugin") pluginTyConKey
+pluginTyConName = tcQual pLUGINS (fsLit "Plugin") pluginTyConKey
 \end{code}
 
 %************************************************************************
diff --git a/compiler/simplCore/CoreMonad.lhs b/compiler/simplCore/CoreMonad.lhs
index 0d41d5ef07..c175b07384 100644
--- a/compiler/simplCore/CoreMonad.lhs
+++ b/compiler/simplCore/CoreMonad.lhs
@@ -14,8 +14,7 @@ module CoreMonad (
     pprPassDetails,
 
     -- * Plugins
-    PluginPass, Plugin(..), CommandLineOption,
-    defaultPlugin, bindsOnlyPass,
+    PluginPass, bindsOnlyPass,
 
     -- * Counting
     SimplCount, doSimplTick, doFreeSimplTick, simplCountN,
@@ -478,30 +477,6 @@ to switch off those rules until after floating.
 %************************************************************************
 
 \begin{code}
--- | Command line options gathered from the -PModule.Name:stuff syntax are given to you as this type
-type CommandLineOption = String
-
--- | 'Plugin' is the core compiler plugin data type. Try to avoid
--- constructing one of these directly, and just modify some fields of
--- 'defaultPlugin' instead: this is to try and preserve source-code
--- compatability when we add fields to this.
---
--- Nonetheless, this API is preliminary and highly likely to change in the future.
-data Plugin = Plugin {
-        installCoreToDos :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
-                -- ^ Modify the Core pipeline that will be used for compilation.
-                -- This is called as the Core pipeline is built for every module
-                --  being compiled, and plugins get the opportunity to modify
-                -- the pipeline in a nondeterministic order.
-     }
-
--- | Default plugin: does nothing at all! For compatability reasons you should base all your
--- plugin definitions on this default value.
-defaultPlugin :: Plugin
-defaultPlugin = Plugin {
-        installCoreToDos = const return
-    }
-
 -- | A description of the plugin pass itself
 type PluginPass = ModGuts -> CoreM ModGuts
 
diff --git a/compiler/simplCore/SimplCore.lhs b/compiler/simplCore/SimplCore.lhs
index 1d3b233b1a..883f2ef7f9 100644
--- a/compiler/simplCore/SimplCore.lhs
+++ b/compiler/simplCore/SimplCore.lhs
@@ -52,13 +52,8 @@ import Outputable
 import Control.Monad
 
 #ifdef GHCI
-import Type             ( mkTyConTy )
-import RdrName          ( mkRdrQual )
-import OccName          ( mkVarOcc )
-import PrelNames        ( pluginTyConName )
-import DynamicLoading   ( forceLoadTyCon, lookupRdrNameInModuleForPlugins, getValueSafely )
-import Module           ( ModuleName )
-import Panic
+import DynamicLoading   ( loadPlugins )
+import Plugins          ( installCoreToDos )
 #endif
 \end{code}
 
@@ -77,7 +72,7 @@ core2core hsc_env guts
        ; let builtin_passes = getCoreToDo dflags
        ;
        ; (guts2, stats) <- runCoreM hsc_env hpt_rule_base us mod print_unqual $
-                           do { all_passes <- addPluginPasses dflags builtin_passes
+                           do { all_passes <- addPluginPasses builtin_passes
                               ; runCorePasses all_passes guts }
 
        ; Err.dumpIfSet_dyn dflags Opt_D_dump_simpl_stats
@@ -321,49 +316,16 @@ getCoreToDo dflags
 Loading plugins
 
 \begin{code}
-addPluginPasses :: DynFlags -> [CoreToDo] -> CoreM [CoreToDo]
+addPluginPasses :: [CoreToDo] -> CoreM [CoreToDo]
 #ifndef GHCI
-addPluginPasses _ builtin_passes = return builtin_passes
+addPluginPasses builtin_passes = return builtin_passes
 #else
-addPluginPasses dflags builtin_passes
+addPluginPasses builtin_passes
   = do { hsc_env <- getHscEnv
        ; named_plugins <- liftIO (loadPlugins hsc_env)
        ; foldM query_plug builtin_passes named_plugins }
   where
-    query_plug todos (mod_nm, plug)
-       = installCoreToDos plug options todos
-       where
-         options = [ option | (opt_mod_nm, option) <- pluginModNameOpts dflags
-                            , opt_mod_nm == mod_nm ]
-
-loadPlugins :: HscEnv -> IO [(ModuleName, Plugin)]
-loadPlugins hsc_env
-  = do { let to_load = pluginModNames (hsc_dflags hsc_env)
-       ; plugins <- mapM (loadPlugin hsc_env) to_load
-       ; return $ to_load `zip` plugins }
-
-loadPlugin :: HscEnv -> ModuleName -> IO Plugin
-loadPlugin hsc_env mod_name
-  = do { let plugin_rdr_name = mkRdrQual mod_name (mkVarOcc "plugin")
-             dflags = hsc_dflags hsc_env
-       ; mb_name <- lookupRdrNameInModuleForPlugins hsc_env mod_name plugin_rdr_name
-       ; case mb_name of {
-            Nothing ->
-                throwGhcExceptionIO (CmdLineError $ showSDoc dflags $ hsep
-                          [ ptext (sLit "The module"), ppr mod_name
-                          , ptext (sLit "did not export the plugin name")
-                          , ppr plugin_rdr_name ]) ;
-            Just name ->
-
-     do { plugin_tycon <- forceLoadTyCon hsc_env pluginTyConName
-        ; mb_plugin <- getValueSafely hsc_env name (mkTyConTy plugin_tycon)
-        ; case mb_plugin of
-            Nothing ->
-                throwGhcExceptionIO (CmdLineError $ showSDoc dflags $ hsep
-                          [ ptext (sLit "The value"), ppr name
-                          , ptext (sLit "did not have the type")
-                          , ppr pluginTyConName, ptext (sLit "as required")])
-            Just plugin -> return plugin } } }
+    query_plug todos (_, plug, options) = installCoreToDos plug options todos
 #endif
 \end{code}
 
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 6a3eca42f9..1cb3c453be 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -39,11 +39,11 @@ import TcErrors
 import TcSMonad
 import Bag
 
-import Data.List( partition )
+import Data.List( partition, foldl', deleteFirstsBy )
 
 import VarEnv
 
-import Control.Monad( when, unless, forM )
+import Control.Monad( when, unless, forM, foldM )
 import Pair (Pair(..))
 import Unique( hasKey )
 import FastString ( sLit )
@@ -119,11 +119,15 @@ solveFlatGivens loc givens
   | null givens  -- Shortcut for common case
   = return ()
   | otherwise
-  = solveFlats (listToBag (map mk_given_ct givens))
+  = go (map mk_given_ct givens)
   where
     mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evtm = EvId ev_id
                                                 , ctev_pred = evVarPred ev_id
                                                 , ctev_loc  = loc })
+    go givens = do { solveFlats (listToBag givens)
+                   ; new_givens <- runTcPluginsGiven
+                   ; when (notNull new_givens) (go new_givens)
+                   }
 
 solveFlatWanteds :: Cts -> TcS WantedConstraints
 solveFlatWanteds wanteds
@@ -134,9 +138,14 @@ solveFlatWanteds wanteds
 
        ; zonked <- zonkFlats (others `andCts` unflattened_eqs)
             -- Postcondition is that the wl_flats are zonked
-       ; return (WC { wc_flat  = zonked
-                    , wc_insol = insols
-                    , wc_impl  = implics }) }
+
+       ; (wanteds', insols', rerun) <- runTcPluginsWanted zonked
+       ; if rerun then do { updInertTcS prepareInertsForImplications
+                          ; solveFlatWanteds wanteds' }
+                  else return (WC { wc_flat  = wanteds'
+                                  , wc_insol = insols' `unionBags` insols
+                                  , wc_impl  = implics }) }
+
 
 -- The main solver loop implements Note [Basic Simplifier Plan]
 ---------------------------------------------------------------
@@ -162,6 +171,127 @@ solveFlats cts
               NextWorkItem ct     -- More work, loop around!
                 -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
 
+
+-- | Extract the (inert) givens and invoke the plugins on them.
+-- Remove solved givens from the inert set and emit insolubles, but
+-- return new work produced so that 'solveFlatGivens' can feed it back
+-- into the main solver.
+runTcPluginsGiven :: TcS [Ct]
+runTcPluginsGiven = do
+  (givens,_,_) <- fmap splitInertCans getInertCans
+  if null givens
+    then return []
+    else do
+      p <- runTcPlugins (givens,[],[])
+      let (solved_givens, _, _) = pluginSolvedCts p
+      updInertCans (removeInertCts solved_givens)
+      mapM_ emitInsoluble (pluginBadCts p)
+      return (pluginNewCts p)
+
+-- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
+-- them and produce an updated bag of wanteds (possibly with some new
+-- work) and a bag of insolubles.  The boolean indicates whether
+-- 'solveFlatWanteds' should feed the updated wanteds back into the
+-- main solver.
+runTcPluginsWanted :: Cts -> TcS (Cts, Cts, Bool)
+runTcPluginsWanted zonked_wanteds
+  | isEmptyBag zonked_wanteds = return (zonked_wanteds, emptyBag, False)
+  | otherwise                 = do
+    (given,derived,_) <- fmap splitInertCans getInertCans
+    p <- runTcPlugins (given, derived, bagToList zonked_wanteds)
+    let (solved_givens, solved_deriveds, solved_wanteds) = pluginSolvedCts p
+        (_, _, wanteds) = pluginInputCts p
+    updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
+    mapM_ setEv solved_wanteds
+    return ( listToBag $ pluginNewCts p ++ wanteds
+           , listToBag $ pluginBadCts p
+           , notNull (pluginNewCts p) )
+  where
+    setEv :: (EvTerm,Ct) -> TcS ()
+    setEv (ev,ct) = case ctEvidence ct of
+      CtWanted {ctev_evar = evar} -> setEvBind evar ev
+      _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
+
+-- | A triple of (given, derived, wanted) constraints to pass to plugins
+type SplitCts  = ([Ct], [Ct], [Ct])
+
+-- | A solved triple of constraints, with evidence for wanteds
+type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)])
+
+-- | Represents collections of constraints generated by typechecker
+-- plugins
+data TcPluginProgress = TcPluginProgress
+    { pluginInputCts  :: SplitCts
+      -- ^ Original inputs to the plugins with solved/bad constraints
+      -- removed, but otherwise unmodified
+    , pluginSolvedCts :: SolvedCts
+      -- ^ Constraints solved by plugins
+    , pluginBadCts    :: [Ct]
+      -- ^ Constraints reported as insoluble by plugins
+    , pluginNewCts    :: [Ct]
+      -- ^ New constraints emitted by plugins
+    }
+
+-- | Starting from a triple of (given, derived, wanted) constraints,
+-- invoke each of the typechecker plugins in turn and return
+--
+--  * the remaining unmodified constraints,
+--  * constraints that have been solved,
+--  * constraints that are insoluble, and
+--  * new work.
+--
+-- Note that new work generated by one plugin will not be seen by
+-- other plugins on this pass (but the main constraint solver will be
+-- re-invoked and they will see it later).  There is no check that new
+-- work differs from the original constraints supplied to the plugin:
+-- the plugin itself should perform this check if necessary.
+runTcPlugins :: SplitCts -> TcS TcPluginProgress
+runTcPlugins all_cts = do
+    gblEnv <- getGblEnv
+    foldM do_plugin initialProgress (tcg_tc_plugins gblEnv)
+  where
+    do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
+    do_plugin p solver = do
+        result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
+        return $ progress p result
+
+    progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress
+    progress p (TcPluginContradiction bad_cts) =
+       p { pluginInputCts = discard bad_cts (pluginInputCts p)
+         , pluginBadCts   = bad_cts ++ pluginBadCts p
+         }
+    progress p (TcPluginOk solved_cts new_cts) =
+      p { pluginInputCts  = discard (map snd solved_cts) (pluginInputCts p)
+        , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
+        , pluginNewCts    = new_cts ++ pluginNewCts p
+        }
+
+    initialProgress = TcPluginProgress all_cts ([], [], []) [] []
+
+    discard :: [Ct] -> SplitCts -> SplitCts
+    discard cts (xs, ys, zs) =
+        (xs `without` cts, ys `without` cts, zs `without` cts)
+
+    without :: [Ct] -> [Ct] -> [Ct]
+    without = deleteFirstsBy eqCt
+
+    eqCt :: Ct -> Ct -> Bool
+    eqCt c c' = case (ctEvidence c, ctEvidence c') of
+      (CtGiven   pred _ _, CtGiven   pred' _ _) -> pred `eqType` pred'
+      (CtWanted  pred _ _, CtWanted  pred' _ _) -> pred `eqType` pred'
+      (CtDerived pred _  , CtDerived pred' _  ) -> pred `eqType` pred'
+      (_                 , _                  ) -> False
+
+    add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
+    add xs scs = foldl' addOne scs xs
+
+    addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
+    addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of
+      CtGiven  {} -> (ct:givens, deriveds, wanteds)
+      CtDerived{} -> (givens, ct:deriveds, wanteds)
+      CtWanted {} -> (givens, deriveds, (ev,ct):wanteds)
+
+
 type WorkItem = Ct
 type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
 
diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs
new file mode 100644
index 0000000000..a59206eb00
--- /dev/null
+++ b/compiler/typecheck/TcPluginM.hs
@@ -0,0 +1,123 @@
+{-# LANGUAGE CPP #-}
+-- | This module provides an interface for typechecker plugins to
+-- access select functions of the 'TcM', principally those to do with
+-- reading parts of the state.
+module TcPluginM (
+#ifdef GHCI
+        -- * Basic TcPluginM functionality
+        TcPluginM,
+        tcPluginIO,
+        tcPluginTrace,
+        unsafeTcPluginTcM,
+
+        -- * Lookup
+        lookupRdrName,
+        tcLookupGlobal,
+        tcLookupTyCon,
+        tcLookupDataCon,
+        tcLookupClass,
+        tcLookup,
+        tcLookupId,
+
+        -- * Getting the TcM state
+        getTopEnv,
+        getEnvs,
+        getInstEnvs,
+        getFamInstEnvs,
+
+        -- * Type variables
+        newFlexiTyVar,
+        isTouchableTcPluginM,
+
+        -- * Zonking
+        zonkTcType,
+        zonkCt
+#endif
+    ) where
+
+#ifdef GHCI
+import qualified TcRnMonad
+import qualified TcEnv
+import qualified TcMType
+import qualified Inst
+import qualified FamInst
+
+import FamInstEnv ( FamInstEnv )
+import TcRnMonad  ( TcGblEnv, TcLclEnv, Ct, TcPluginM
+                  , unsafeTcPluginTcM, liftIO, traceTc )
+import TcMType    ( TcTyVar, TcType )
+import TcEnv      ( TcTyThing )
+
+import Module
+import Name
+import RdrName
+import TyCon
+import DataCon
+import Class
+import HscTypes
+import Outputable
+import Type
+import DynamicLoading
+import Id
+import InstEnv
+
+
+-- | Perform some IO, typically to interact with an external tool.
+tcPluginIO :: IO a -> TcPluginM a
+tcPluginIO a = unsafeTcPluginTcM (liftIO a)
+
+-- | Output useful for debugging the compiler.
+tcPluginTrace :: String -> SDoc -> TcPluginM ()
+tcPluginTrace a b = unsafeTcPluginTcM (traceTc a b)
+
+
+lookupRdrName :: ModuleName -> RdrName -> TcPluginM (Maybe Name)
+lookupRdrName mod rdr = do
+  hsc_env <- getTopEnv
+  tcPluginIO $ lookupRdrNameInModuleForPlugins hsc_env mod rdr
+
+tcLookupGlobal :: Name -> TcPluginM TyThing
+tcLookupGlobal = unsafeTcPluginTcM . TcEnv.tcLookupGlobal
+
+tcLookupTyCon :: Name -> TcPluginM TyCon
+tcLookupTyCon = unsafeTcPluginTcM . TcEnv.tcLookupTyCon
+
+tcLookupDataCon :: Name -> TcPluginM DataCon
+tcLookupDataCon = unsafeTcPluginTcM . TcEnv.tcLookupDataCon
+
+tcLookupClass :: Name -> TcPluginM Class
+tcLookupClass = unsafeTcPluginTcM . TcEnv.tcLookupClass
+
+tcLookup :: Name -> TcPluginM TcTyThing
+tcLookup = unsafeTcPluginTcM . TcEnv.tcLookup
+
+tcLookupId :: Name -> TcPluginM Id
+tcLookupId = unsafeTcPluginTcM . TcEnv.tcLookupId
+
+
+getTopEnv :: TcPluginM HscEnv
+getTopEnv = unsafeTcPluginTcM TcRnMonad.getTopEnv
+
+getEnvs :: TcPluginM (TcGblEnv, TcLclEnv)
+getEnvs = unsafeTcPluginTcM TcRnMonad.getEnvs
+
+getInstEnvs :: TcPluginM (InstEnv, InstEnv)
+getInstEnvs = unsafeTcPluginTcM Inst.tcGetInstEnvs
+
+getFamInstEnvs :: TcPluginM (FamInstEnv, FamInstEnv)
+getFamInstEnvs = unsafeTcPluginTcM FamInst.tcGetFamInstEnvs
+
+
+newFlexiTyVar :: Kind -> TcPluginM TcTyVar
+newFlexiTyVar = unsafeTcPluginTcM . TcMType.newFlexiTyVar
+
+isTouchableTcPluginM :: TcTyVar -> TcPluginM Bool
+isTouchableTcPluginM = unsafeTcPluginTcM . TcRnMonad.isTouchableTcM
+
+
+zonkTcType :: TcType -> TcPluginM TcType
+zonkTcType = unsafeTcPluginTcM . TcMType.zonkTcType
+
+zonkCt :: Ct -> TcPluginM Ct
+zonkCt = unsafeTcPluginTcM . TcMType.zonkCt
+#endif
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index 32113bb976..0b1601bc3a 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -20,7 +20,7 @@ module TcRnDriver (
         tcRnLookupName,
         tcRnGetInfo,
         tcRnModule, tcRnModuleTcRnM,
-        tcTopSrcDecls
+        tcTopSrcDecls,
     ) where
 
 #ifdef GHCI
@@ -93,6 +93,8 @@ import RnExpr
 import MkId
 import TidyPgm    ( globaliseAndTidyId )
 import TysWiredIn ( unitTy, mkListTy )
+import DynamicLoading ( loadPlugins )
+import Plugins ( tcPlugin )
 #endif
 import TidyPgm    ( mkBootModDetailsTc )
 
@@ -134,8 +136,11 @@ tcRnModule hsc_env hsc_src save_rn_syntax
                     Just (L mod_loc mod)  -- The normal case
                         -> (mkModule this_pkg mod, mod_loc) } ;
 
-      ; initTc hsc_env hsc_src save_rn_syntax this_mod $
-        tcRnModuleTcRnM hsc_env hsc_src parsedModule pair }
+      ; res <- initTc hsc_env hsc_src save_rn_syntax this_mod $
+               withTcPlugins hsc_env $
+        tcRnModuleTcRnM hsc_env hsc_src parsedModule pair
+      ; return res
+      }
 
 -- To be called at the beginning of renaming hsig files.
 -- If we're processing a signature, load up the RdrEnv
@@ -1380,7 +1385,7 @@ runTcInteractive :: HscEnv -> TcRn a -> IO (Messages, Maybe a)
 -- Initialise the tcg_inst_env with instances from all home modules.
 -- This mimics the more selective call to hptInstances in tcRnImports
 runTcInteractive hsc_env thing_inside
-  = initTcInteractive hsc_env $
+  = initTcInteractive hsc_env $ withTcPlugins hsc_env $
     do { traceTc "setInteractiveContext" $
             vcat [ text "ic_tythings:" <+> vcat (map ppr (ic_tythings icxt))
                  , text "ic_insts:" <+> vcat (map (pprBndr LetBind . instanceDFunId) ic_insts)
@@ -2090,3 +2095,38 @@ ppr_tydecls tycons
   where
     ppr_tycon tycon = vcat [ ppr (tyThingToIfaceDecl (ATyCon tycon)) ]
 \end{code}
+
+
+********************************************************************************
+
+Type Checker Plugins
+
+********************************************************************************
+
+
+\begin{code}
+withTcPlugins :: HscEnv -> TcM a -> TcM a
+withTcPlugins hsc_env m =
+  do plugins <- liftIO (loadTcPlugins hsc_env)
+     case plugins of
+       [] -> m  -- Common fast case
+       _  -> do (solvers,stops) <- unzip `fmap` mapM startPlugin plugins
+                res <- updGblEnv (\e -> e { tcg_tc_plugins = solvers }) m
+                mapM_ runTcPluginM stops
+                return res
+  where
+  startPlugin (TcPlugin start solve stop) =
+    do s <- runTcPluginM start
+       return (solve s, stop s)
+
+loadTcPlugins :: HscEnv -> IO [TcPlugin]
+#ifndef GHCI
+loadTcPlugins _ = return []
+#else
+loadTcPlugins hsc_env =
+ do named_plugins <- loadPlugins hsc_env
+    return $ catMaybes $ map load_plugin named_plugins
+  where
+    load_plugin (_, plug, opts) = tcPlugin plug opts
+#endif
+\end{code}
diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs
index 41f861c02c..b73b525b4d 100644
--- a/compiler/typecheck/TcRnMonad.lhs
+++ b/compiler/typecheck/TcRnMonad.lhs
@@ -162,7 +162,8 @@ initTc hsc_env hsc_src keep_rn_syntax mod do_this
                 tcg_hpc            = False,
                 tcg_main           = Nothing,
                 tcg_safeInfer      = infer_var,
-                tcg_dependent_files = dependent_files_var
+                tcg_dependent_files = dependent_files_var,
+                tcg_tc_plugins     = []
              } ;
              lcl_env = TcLclEnv {
                 tcl_errs       = errs_var,
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 2634aa852f..15be2a6212 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -16,7 +16,7 @@ For state that is global and should be returned at the end (e.g not part
 of the stack mechanism), you should use an TcRef (= IORef) to store them.
 
 \begin{code}
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, ExistentialQuantification #-}
 
 module TcRnTypes(
         TcRnIf, TcRn, TcM, RnM, IfM, IfL, IfG, -- The monad is opaque outside this module
@@ -74,6 +74,10 @@ module TcRnTypes(
         mkGivenLoc,
         isWanted, isGiven, isDerived,
 
+        -- Constraint solver plugins
+        TcPlugin(..), TcPluginResult(..), TcPluginSolver,
+        TcPluginM, runTcPluginM, unsafeTcPluginTcM,
+
         -- Pretty printing
         pprEvVarTheta, 
         pprEvVars, pprEvVarWithType,
@@ -122,6 +126,7 @@ import ListSetOps
 import FastString
 
 import Data.Set (Set)
+import Control.Monad (ap, liftM)
 
 #ifdef GHCI
 import Data.Map      ( Map )
@@ -367,9 +372,12 @@ data TcGblEnv
         tcg_main      :: Maybe Name,         -- ^ The Name of the main
                                              -- function, if this module is
                                              -- the main module.
-        tcg_safeInfer :: TcRef Bool          -- Has the typechecker
+        tcg_safeInfer :: TcRef Bool,         -- Has the typechecker
                                              -- inferred this module
                                              -- as -XSafe (Safe Haskell)
+
+        -- | A list of user-defined plugins for the constraint solver.
+        tcg_tc_plugins :: [TcPluginSolver]
     }
 
 -- Note [Signature parameters in TcGblEnv and DynFlags]
@@ -1968,3 +1976,71 @@ pprCtO HoleOrigin            = ptext (sLit "a use of") <+> quotes (ptext $ sLit
 pprCtO ListOrigin            = ptext (sLit "an overloaded list")
 pprCtO _                     = panic "pprCtOrigin"
 \end{code}
+
+
+
+
+
+Constraint Solver Plugins
+-------------------------
+
+
+\begin{code}
+
+type TcPluginSolver = [Ct]    -- given
+                   -> [Ct]    -- derived
+                   -> [Ct]    -- wanted
+                   -> TcPluginM TcPluginResult
+
+newtype TcPluginM a = TcPluginM (TcM a)
+
+instance Functor     TcPluginM where
+  fmap = liftM
+
+instance Applicative TcPluginM where
+  pure  = return
+  (<*>) = ap
+
+instance Monad TcPluginM where
+  return x = TcPluginM (return x)
+  fail x   = TcPluginM (fail x)
+  TcPluginM m >>= k =
+    TcPluginM (do a <- m
+                  let TcPluginM m1 = k a
+                  m1)
+
+runTcPluginM :: TcPluginM a -> TcM a
+runTcPluginM (TcPluginM m) = m
+
+-- | This function provides an escape for direct access to
+-- the 'TcM` monad.  It should not be used lightly, and
+-- the provided 'TcPluginM' API should be favoured instead.
+unsafeTcPluginTcM :: TcM a -> TcPluginM a
+unsafeTcPluginTcM = TcPluginM
+
+data TcPlugin = forall s. TcPlugin
+  { tcPluginInit  :: TcPluginM s
+    -- ^ Initialize plugin, when entering type-checker.
+
+  , tcPluginSolve :: s -> TcPluginSolver
+    -- ^ Solve some constraints.
+    -- TODO: WRITE MORE DETAILS ON HOW THIS WORKS.
+
+  , tcPluginStop  :: s -> TcPluginM ()
+   -- ^ Clean up after the plugin, when exiting the type-checker.
+  }
+
+data TcPluginResult
+  = TcPluginContradiction [Ct]
+    -- ^ The plugin found a contradiction.
+    -- The returned constraints are removed from the inert set,
+    -- and recorded as insoluable.
+
+  | TcPluginOk [(EvTerm,Ct)] [Ct]
+    -- ^ The first field is for constraints that were solved.
+    -- These are removed from the inert set,
+    -- and the evidence for them is recorded.
+    -- The second field contains new work, that should be processed by
+    -- the constraint solver.
+
+\end{code}
diff --git a/compiler/typecheck/TcRnTypes.lhs-boot b/compiler/typecheck/TcRnTypes.lhs-boot
deleted file mode 100644
index 36c43fc496..0000000000
--- a/compiler/typecheck/TcRnTypes.lhs-boot
+++ /dev/null
@@ -1,13 +0,0 @@
-\begin{code}
-module TcRnTypes where
-
-import IOEnv 
-
-type TcM a = TcRn a
-type TcRn a = TcRnIf TcGblEnv TcLclEnv a
-type TcRnIf a b c = IOEnv (Env a b) c
-
-data Env a b
-data TcGblEnv
-data TcLclEnv
-\end{code}
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index d4a5a9a8ca..decbb4ff2b 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -12,9 +12,9 @@ module TcSMonad (
     extendWorkListCts, appendWorkList, selectWorkItem,
     workListSize,
 
-    updWorkListTcS, updWorkListTcS_return, 
+    updWorkListTcS, updWorkListTcS_return,
 
-    updInertCans, updInertDicts, updInertIrreds, updInertFunEqs,
+    updInertTcS, updInertCans, updInertDicts, updInertIrreds, updInertFunEqs,
 
     Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
     emitInsoluble, emitWorkNC,
@@ -28,6 +28,7 @@ module TcSMonad (
     traceFireTcS, bumpStepCountTcS, csTraceTcS,
     tryTcS, nestTcS, nestImplicTcS, recoverTcS,
     wrapErrTcS, wrapWarnTcS,
+    runTcPluginTcS,
 
     -- Getting and setting the flattening cache
     addSolvedDict, 
@@ -70,6 +71,7 @@ module TcSMonad (
     getNoGivenEqs, setInertCans, getInertEqs, getInertCans,
     emptyInert, getTcSInerts, setTcSInerts, 
     getUnsolvedInerts, checkAllSolved,
+    splitInertCans, removeInertCts,
     prepareInertsForImplications,
     addInertCan, insertInertItemTcS, insertFunEq,
     EqualCtList,
@@ -77,7 +79,7 @@ module TcSMonad (
 
     lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
 
-    findFunEq, findTyEqs, 
+    findFunEq, findTyEqs,
     findFunEqsByTyCon, findFunEqs, partitionFunEqs,
     sizeFunEqMap,
 
@@ -147,6 +149,7 @@ import TrieMap
 import Control.Monad( ap, when, unless )
 import MonadUtils
 import Data.IORef
+import Data.List ( partition, foldl' )
 import Pair
 
 #ifdef DEBUG
@@ -734,6 +737,40 @@ b) 'a' will have been completely substituted out in the inert set,
 For an example, see Trac #9211.
 
 \begin{code}
+splitInertCans :: InertCans -> ([Ct], [Ct], [Ct])
+-- ^ Extract the (given, derived, wanted) inert constraints
+splitInertCans iCans = (given,derived,wanted)
+  where
+    allCts   = foldDicts  (:) (inert_dicts iCans)
+             $ foldFunEqs (:) (inert_funeqs iCans)
+             $ concat (varEnvElts (inert_eqs iCans))
+
+    (derived,other) = partition isDerivedCt allCts
+    (wanted,given)  = partition isWantedCt  other
+
+removeInertCts :: [Ct] -> InertCans -> InertCans
+-- ^ Remove inert constraints from the 'InertCans', for use when a
+-- typechecker plugin wishes to discard a given.
+removeInertCts cts icans = foldl' removeInertCt icans cts
+
+removeInertCt :: InertCans -> Ct -> InertCans
+removeInertCt is ct =
+  case ct of
+
+    CDictCan  { cc_class = cl, cc_tyargs = tys } ->
+      is { inert_dicts = delDict (inert_dicts is) cl tys }
+
+    CFunEqCan { cc_fun  = tf,  cc_tyargs = tys } ->
+      is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
+
+    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty  } ->
+      is { inert_eqs = delTyEq (inert_eqs is) x ty }
+
+    CIrredEvCan {}   -> panic "removeInertCt: CIrredEvCan"
+    CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
+    CHoleCan {}      -> panic "removeInertCt: CHoleCan"
+
+
 checkAllSolved :: TcS Bool
 -- True if there are no unsolved wanteds
 -- Ignore Derived for this purpose, unless in insolubles
@@ -808,6 +845,11 @@ type TyEqMap a = TyVarEnv a
 
 findTyEqs :: TyEqMap EqualCtList -> TyVar -> EqualCtList
 findTyEqs m tv = lookupVarEnv m tv `orElse` []
+
+delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList
+delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
+  where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
+        isThisOne _                          = False
 \end{code}
 
 
@@ -961,6 +1003,9 @@ partitionFunEqs f m = foldTcAppMap k m (emptyBag, emptyFunEqs)
     k ct (yeses, noes)
       | f ct      = (yeses `snocBag` ct, noes)
       | otherwise = (yeses, insertFunEqCt noes ct)
+
+delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
+delFunEq m tc tys = delTcApp m (getUnique tc) tys
 \end{code}
 
 
@@ -1044,6 +1089,9 @@ panicTcS doc = pprPanic "TcCanonical" doc
 traceTcS :: String -> SDoc -> TcS ()
 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 
+runTcPluginTcS :: TcPluginM a -> TcS a
+runTcPluginTcS = wrapTcS . runTcPluginM
+
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
 
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index 37fc6e0cdb..8f02c9abca 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -2,6 +2,14 @@ module TcTypeNats
   ( typeNatTyCons
   , typeNatCoAxiomRules
   , BuiltInSynFamily(..)
+
+  , typeNatAddTyCon
+  , typeNatMulTyCon
+  , typeNatExpTyCon
+  , typeNatLeqTyCon
+  , typeNatSubTyCon
+  , typeNatCmpTyCon
+  , typeSymbolCmpTyCon
   ) where
 
 import Type
diff --git a/docs/users_guide/7.10.1-notes.xml b/docs/users_guide/7.10.1-notes.xml
index 2db72b1187..5a75cc2b04 100644
--- a/docs/users_guide/7.10.1-notes.xml
+++ b/docs/users_guide/7.10.1-notes.xml
@@ -136,6 +136,15 @@
                     than having everything being dumped to stdout.
                 </para>
            </listitem>
+           <listitem>
+             <para>
+               Compiler plugins (with the <option>-fplugin</option>
+               flag) may now modify the behaviour of the constraint
+               solver, to add new functionality to GHC's
+               typechecker. See <xref linkend="typechecker-plugins"/>
+               for more details.
+             </para>
+           </listitem>
        </itemizedlist>
     </sect3>
 
diff --git a/docs/users_guide/extending_ghc.xml b/docs/users_guide/extending_ghc.xml
index 12e598b58e..90e091a533 100644
--- a/docs/users_guide/extending_ghc.xml
+++ b/docs/users_guide/extending_ghc.xml
@@ -124,9 +124,9 @@ $
   <sect1 id="compiler-plugins">
     <title>Compiler Plugins</title>
 
-    <para>GHC has the ability to load compiler plugins at compile time. The feature is similar to the one provided by <ulink url="http://gcc.gnu.org/wiki/plugins">GCC</ulink>, and allows users to write plugins that can inspect and modify the compilation pipeline, as well as transform and inspect GHC's intermediate language, Core. Plugins are suitable for experimental analysis or optimization, and require no changes to GHC's source code to use.</para>
+    <para>GHC has the ability to load compiler plugins at compile time. The feature is similar to the one provided by <ulink url="http://gcc.gnu.org/wiki/plugins">GCC</ulink>, and allows users to write plugins that can adjust the behaviour of the constraint solver, inspect and modify the compilation pipeline, as well as transform and inspect GHC's intermediate language, Core. Plugins are suitable for experimental analysis or optimization, and require no changes to GHC's source code to use.</para>
 
-    <para>Plugins cannot optimize/inspect C--, nor can they implement things like parser/front-end modifications like GCC. If you feel strongly that any of these restrictions are too onerous, <ulink url="http://ghc.haskell.org/trac/ghc/wiki/MailingListsAndIRC"> please give the GHC team a shout</ulink>.</para>
+    <para>Plugins cannot optimize/inspect C--, nor can they implement things like parser/front-end modifications like GCC, apart from limited changes to the constraint solver. If you feel strongly that any of these restrictions are too onerous, <ulink url="http://ghc.haskell.org/trac/ghc/wiki/MailingListsAndIRC"> please give the GHC team a shout</ulink>.</para>
 
     <sect2 id="using-compiler-plugins">
       <title>Using compiler plugins</title>
@@ -183,8 +183,10 @@ install _ todo = do
       <para>Note carefully the <literal>reinitializeGlobals</literal> call at the beginning of the installation function. Due to bugs in the windows linker dealing with <literal>libghc</literal>, this call is necessary to properly ensure compiler plugins have the same global state as GHC at the time of invocation. Without <literal>reinitializeGlobals</literal>, compiler plugins can crash at runtime because they may require state that hasn't otherwise been initialized.</para>
 
       <para>In the future, when the linking bugs are fixed, <literal>reinitializeGlobals</literal> will be deprecated with a warning, and changed to do nothing.</para>
-      <sect3 id="coretodo-in-more-detail">
-        <title><literal>CoreToDo</literal> in more detail</title>
+    </sect2>
+
+    <sect2 id="core-plugins-in-more-detail">
+        <title>Core plugins in more detail</title>
 
         <para><literal>CoreToDo</literal> is effectively a data type that describes all the kinds of optimization passes GHC does on Core. There are passes for simplification, CSE, vectorisation, etc. There is a specific case for plugins, <literal>CoreDoPluginPass :: String -> PluginPass -> CoreToDo</literal> which should be what you always use when inserting your own pass into the pipeline. The first parameter is the name of the plugin, and the second is the pass you wish to insert.</para>
 
@@ -200,7 +202,6 @@ install _ _ = return []
 </programlisting>
 
         <para>is certainly valid, but also certainly not what anyone really wants.</para>
-      </sect3>
 
       <sect3 id="manipulating-bindings">
         <title>Manipulating bindings</title>
@@ -283,6 +284,60 @@ annotationsOn guts bndr = do
       </sect3>
     </sect2>
 
+    <sect2 id="typechecker-plugins">
+      <title>Typechecker plugins</title>
+
+      <para>In addition to Core plugins, GHC has experimental support for typechecker plugins, which allow the behaviour of the constraint solver to be modified. For example, they make it possible to interface the compiler to an SMT solver, in order to support a richer theory of type-level arithmetic expressions than the theory built into GHC (see <xref linkend="typelit-tyfuns"/>).</para>
+
+      <para>The <literal>Plugin</literal> type has a field <literal>tcPlugin</literal> of type <literal>[CommandLineOption] -> Maybe TcPlugin</literal>, where the <literal>TcPlugin</literal> type is defined thus:</para>
+
+<programlisting>
+data TcPlugin = forall s . TcPlugin
+  { tcPluginInit  :: TcPluginM s
+  , tcPluginSolve :: s -> TcPluginSolver
+  , tcPluginStop  :: s -> TcPluginM ()
+  }
+
+type TcPluginSolver = [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
+
+data TcPluginResult = TcPluginContradiction [Ct] | TcPluginOk [(EvTerm,Ct)] [Ct]
+</programlisting>
+
+      <para>(The details of this representation are subject to change as we gain more experience writing typechecker plugins. It should not be assumed to be stable between GHC releases.)</para>
+
+      <para>The basic idea is as follows:
+      <itemizedlist>
+        <listitem><para>When type checking a module, GHC calls <literal>tcPluginInit</literal> once before constraint solving starts. This allows the plugin to look things up in the context, initialise mutable state or open a connection to an external process (e.g. an external SMT solver). The plugin can return a result of any type it likes, and the result will be passed to the other two fields.</para></listitem>
+        <listitem><para>During constraint solving, GHC repeatedly calls <literal>tcPluginSolve</literal>. This function is provided with the current set of constraints, and should return a <literal>TcPluginResult</literal> that indicates whether a contradiction was found or progress was made. If the plugin solver makes progress, GHC will re-start the constraint solving pipeline, looping until a fixed point is reached.</para></listitem>
+        <listitem><para>Finally, GHC calls <literal>tcPluginStop</literal> after constraint solving is finished, allowing the plugin to dispose of any resources it has allocated (e.g. terminating the SMT solver process).</para></listitem>
+      </itemizedlist>
+      </para>
+
+      <para>Plugin code runs in the <literal>TcPluginM</literal> monad, which provides a restricted interface to GHC API functionality that is relevant for typechecker plugins, including <literal>IO</literal> and reading the environment. If you need functionality that is not exposed in the <literal>TcPluginM</literal> module, you can use <literal>unsafeTcPluginTcM :: TcM a -> TcPluginM a</literal>, but are encouraged to contact the GHC team to suggest additions to the interface. Note that <literal>TcPluginM</literal> can perform arbitrary IO via <literal>tcPluginIO :: IO a -> TcPluginM a</literal>, although some care must be taken with side effects (particularly in <literal>tcPluginSolve</literal>). In general, it is up to the plugin author to make sure that any IO they do is safe.</para>
+
+      <sect3 id="constraint-solving-with-plugins">
+
+        <title>Constraint solving with plugins</title>
+
+        <para>The key component of a typechecker plugin is a function of type <literal>TcPluginSolver</literal>, like this:</para>
+
+<programlisting>
+solve :: [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
+solve givens deriveds wanteds = ...
+</programlisting>
+
+        <para>This function will be invoked at two points in the constraint solving process: after simplification of given constraints, and after unflattening of wanted constraints. The two phases can be distinguished because the deriveds and wanteds will be empty in the first case. In each case, the plugin should either
+        <itemizedlist>
+          <listitem><para>return <literal>TcPluginContradiction</literal> with a list of impossible constraints (which must be a subset of those passed in), so they can be turned into errors; or</para></listitem>
+          <listitem><para>return <literal>TcPluginOk</literal> with lists of solved and new constraints (the former must be a subset of those passed in and must be supplied with corresponding evidence terms).</para></listitem>
+        </itemizedlist>
+        If the plugin cannot make any progress, it should return <literal>TcPluginOk [] []</literal>. Otherwise, if there were any new constraints, the main constraint solver will be re-invoked to simplify them, then the plugin will be invoked again. The plugin is responsible for making sure that this process eventually terminates.</para>
+
+        <para>Plugins are provided with all available constraints (including equalities and typeclass constraints), but it is easy for them to discard those that are not relevant to their domain, because they need return only those constraints for which they have made progress (either by solving or contradicting them).</para>
+
+        <para>Constraints that have been solved by the plugin must be provided with evidence in the form of an <literal>EvTerm</literal> of the type of the constraint. This evidence is ignored for given and derived constraints, which GHC "solves" simply by discarding them; typically this is used when they are uninformative (e.g. reflexive equations). For wanted constraints, the evidence will form part of the Core term that is generated after typechecking, and can be checked by <option>-dcore-lint</option>. It is possible for the plugin to create equality axioms for use in evidence terms, but GHC does not check their consistency, and inconsistent axiom sets may lead to segfaults or other runtime misbehaviour.</para>
+      </sect3>
+    </sect2>
   </sect1>
 
 </chapter>