Add nontrivial type-checking plugin tests

  Three new tests for type-checking plugins:

    - TcPlugin_Nullary, solving a nullary class constraint
    - TcPlugin_Args, providing evidence for a (unary) class constraint
      using arguments supplied to the plugin
    - TcPlugin_TyFam, solving an equality constraint to rewrite
      a type-family application

  More extensive descriptions of the plugins can be found in their
  respective defining modules.

12 files changed, 454 insertions, 0 deletions

diff --git a/testsuite/tests/tcplugins/ArgsPlugin.hs b/testsuite/tests/tcplugins/ArgsPlugin.hs
new file mode 100644
index 0000000000..c4ebbb0305
--- /dev/null
+++ b/testsuite/tests/tcplugins/ArgsPlugin.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE RecordWildCards #-}
+
+module ArgsPlugin where
+
+-- base
+import Data.Maybe
+  ( catMaybes )
+
+-- ghc
+import GHC.Builtin.Types
+  ( integerTy )
+import GHC.Core
+  ( Expr(Type) )
+import GHC.Core.Class
+  ( Class(..) )
+import GHC.Core.DataCon
+  ( classDataCon )
+import GHC.Core.Make
+  ( mkCoreConApps, mkIntegerExpr )
+import GHC.Core.Type
+  ( eqType )
+import GHC.Plugins
+  ( Plugin )
+import GHC.Tc.Plugin
+  ( TcPluginM )
+import GHC.Tc.Types
+  ( TcPluginResult(..) )
+import GHC.Tc.Types.Constraint
+  ( Ct(..) )
+import GHC.Tc.Types.Evidence
+  ( EvTerm(EvExpr) )
+
+-- common
+import Common
+  ( PluginDefs(..)
+  , mkPlugin
+  )
+
+--------------------------------------------------------------------------------
+
+-- This plugin solves Wanted constraints of the form "MyClass Integer",
+-- and supplies evidence that depends on the arguments to the plugin.
+--
+-- To find such constraints, we traverse through the Wanteds provided
+-- to the plugin to find those whose name matches that of "MyClass",
+-- and check that it is applied to the type "Integer".
+--
+-- We then construct a dictionary which is the integer that was passed
+-- as an argument to the plugin.
+
+plugin :: Plugin
+plugin = mkPlugin solver
+
+-- Solve "MyClass Integer" with a class dictionary that depends on
+-- a plugin argument.
+solver :: [String]
+       -> PluginDefs -> [Ct] -> [Ct] -> [Ct]
+       -> TcPluginM TcPluginResult
+solver args defs _gs _ds ws = do
+  let
+    argsVal :: Integer
+    argsVal = case args of
+      arg : _ -> read arg
+      _       -> error "ArgsPlugin: expected at least one argument"
+  solved <- catMaybes <$> traverse ( solveCt defs argsVal ) ws
+  pure $ TcPluginOk solved []
+
+solveCt :: PluginDefs -> Integer -> Ct -> TcPluginM ( Maybe (EvTerm, Ct) )
+solveCt ( PluginDefs {..} ) i ct@( CDictCan { cc_class, cc_tyargs } )
+  | className cc_class == className myClass
+  , [tyArg] <- cc_tyargs
+  , tyArg `eqType` integerTy
+  , let
+      evTerm :: EvTerm
+      evTerm = EvExpr $
+        mkCoreConApps ( classDataCon cc_class )
+         [ Type integerTy, mkIntegerExpr i ]
+  = pure $ Just ( evTerm, ct )
+solveCt _ _ ct = pure Nothing
diff --git a/testsuite/tests/tcplugins/Common.hs b/testsuite/tests/tcplugins/Common.hs
new file mode 100644
index 0000000000..615897b910
--- /dev/null
+++ b/testsuite/tests/tcplugins/Common.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Common
+  ( PluginDefs(..)
+  , mkPlugin
+  )
+  where
+
+-- ghc
+import GHC.Core.Class
+  ( Class )
+import GHC.Core.DataCon
+  ( promoteDataCon )
+import GHC.Core.TyCon
+  ( TyCon )
+import GHC.Core.Type
+  ( Type
+  , mkTyConApp
+  )
+import GHC.Plugins
+  ( Plugin(..)
+  , defaultPlugin, purePlugin
+  )
+import GHC.Tc.Plugin
+  ( TcPluginM
+  , findImportedModule, lookupOrig
+  , tcLookupClass, tcLookupDataCon, tcLookupTyCon
+  )
+import GHC.Tc.Types
+  ( TcPlugin(..), TcPluginResult )
+import GHC.Tc.Types.Constraint
+  ( Ct )
+import GHC.Types.Name.Occurrence
+  ( mkClsOcc, mkDataOcc, mkTcOcc )
+import GHC.Unit.Finder
+  ( FindResult(..) )
+import GHC.Unit.Module
+  ( Module
+  , mkModuleName
+  )
+
+--------------------------------------------------------------------------------
+
+-- This module defines some common operations so that each individual plugin
+-- doesn't have to do the same work over again:
+--
+--   - lookup the names of things the plugins will use
+--     (the definitions are shared between most type-checking plugin tests)
+--   - create a type-checking plugin from a solver, taking care of passing
+--     the relevant data to the solver stage.
+
+data PluginDefs =
+  PluginDefs
+    { nullary  :: !Class
+    , myClass  :: !Class
+    , myTyFam  :: !TyCon
+    , nat      :: !Type
+    , zero     :: !TyCon
+    , succ     :: !TyCon
+    , add      :: !TyCon
+    }
+
+definitionsModule :: TcPluginM Module
+definitionsModule = do
+  findResult <- findImportedModule ( mkModuleName "Definitions" ) Nothing
+  case findResult of
+    Found _ res     -> pure res
+    FoundMultiple _ -> error $ "TcPlugin test: found multiple modules named 'Definitions'."
+    _               -> error $ "TcPlugin test: could not find any module named 'Defintiions'."
+
+lookupDefs :: TcPluginM PluginDefs
+lookupDefs = do
+  defs <- definitionsModule
+  nullary                       <- tcLookupClass   =<< lookupOrig defs ( mkClsOcc  "Nullary"  )
+  myClass                       <- tcLookupClass   =<< lookupOrig defs ( mkClsOcc  "MyClass"  )
+  myTyFam                       <- tcLookupTyCon   =<< lookupOrig defs ( mkTcOcc   "MyTyFam"  )
+  ( (`mkTyConApp` []) -> nat  ) <- tcLookupTyCon   =<< lookupOrig defs ( mkTcOcc   "Nat"      )
+  ( promoteDataCon    -> zero ) <- tcLookupDataCon =<< lookupOrig defs ( mkDataOcc "Zero"     )
+  ( promoteDataCon    -> succ ) <- tcLookupDataCon =<< lookupOrig defs ( mkDataOcc "Succ"     )
+  add                           <- tcLookupTyCon   =<< lookupOrig defs ( mkTcOcc   "Add"      )
+  pure ( PluginDefs { .. } )
+
+mkPlugin :: ( [String] -> PluginDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult )
+         -> Plugin
+mkPlugin solve =
+  defaultPlugin
+    { tcPlugin        = \ args -> Just $ mkTcPlugin ( solve args )
+    , pluginRecompile = purePlugin
+    }
+
+mkTcPlugin :: ( PluginDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult )
+           -> TcPlugin
+mkTcPlugin solve =
+  TcPlugin
+    { tcPluginInit  = lookupDefs
+    , tcPluginSolve = solve
+    , tcPluginStop  = \ _ -> pure ()
+    }
diff --git a/testsuite/tests/tcplugins/Definitions.hs b/testsuite/tests/tcplugins/Definitions.hs
new file mode 100644
index 0000000000..5a84967c07
--- /dev/null
+++ b/testsuite/tests/tcplugins/Definitions.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Definitions where
+
+-- base
+import Data.Kind
+  ( Type, Constraint )
+import Numeric.Natural
+  ( Natural )
+
+--------------------------------------------------------------------------------
+
+-- This module defines some common types/classes that the various type-checking
+-- plugins in this test-suite will be interested in manipulating.
+
+type Nullary :: Constraint
+class Nullary where { }
+
+type MyClass :: Type -> Constraint
+class MyClass a where
+  methC :: a
+
+type MyTyFam :: Type -> Type -> Type
+type family MyTyFam a b where
+
+data Nat = Zero | Succ Nat
+
+type Add :: Nat -> Nat -> Nat
+type family Add a b where
+  Add   Zero     b = b
+  Add ( Succ a ) b = Succ ( Add a b )
diff --git a/testsuite/tests/tcplugins/NullaryPlugin.hs b/testsuite/tests/tcplugins/NullaryPlugin.hs
new file mode 100644
index 0000000000..a8176c16b3
--- /dev/null
+++ b/testsuite/tests/tcplugins/NullaryPlugin.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE RecordWildCards #-}
+
+module NullaryPlugin where
+
+-- base
+import Data.Maybe
+  ( catMaybes )
+
+-- ghc
+import GHC.Core.Class
+  ( Class(..) )
+import GHC.Core.DataCon
+  ( classDataCon )
+import GHC.Core.Make
+  ( mkCoreConApps )
+import GHC.Plugins
+  ( Plugin )
+import GHC.Tc.Plugin
+  ( TcPluginM )
+import GHC.Tc.Types
+  ( TcPluginResult(..) )
+import GHC.Tc.Types.Constraint
+  ( Ct(..) )
+import GHC.Tc.Types.Evidence
+  ( EvTerm(EvExpr) )
+
+-- common
+import Common
+  ( PluginDefs(..)
+  , mkPlugin
+  )
+
+--------------------------------------------------------------------------------
+
+-- This plugin solves Wanted 'Nullary' constraints.
+-- To do this, we just look through the Wanteds,
+-- find any constraint whose className matches that of 'Nullary',
+-- in which case we provide evidence (a nullary dictionary).
+
+plugin :: Plugin
+plugin = mkPlugin solver
+
+-- Solve "Nullary".
+solver :: [String]
+       -> PluginDefs -> [Ct] -> [Ct] -> [Ct]
+       -> TcPluginM TcPluginResult
+solver _args defs _gs _ds ws = do
+  solved <- catMaybes <$> traverse ( solveCt defs ) ws
+  pure $ TcPluginOk solved []
+
+solveCt :: PluginDefs -> Ct -> TcPluginM ( Maybe (EvTerm, Ct) )
+solveCt ( PluginDefs {..} ) ct@( CDictCan { cc_class } )
+  | className cc_class == className nullary
+  , let
+      evTerm :: EvTerm
+      evTerm = EvExpr $ mkCoreConApps ( classDataCon cc_class ) []
+  = pure $ Just ( evTerm, ct )
+solveCt _ ct = pure Nothing
diff --git a/testsuite/tests/tcplugins/TcPlugin_Args.hs b/testsuite/tests/tcplugins/TcPlugin_Args.hs
new file mode 100644
index 0000000000..75d478f0e9
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_Args.hs
@@ -0,0 +1,17 @@
+{-# OPTIONS_GHC -dcore-lint #-}
+{-# OPTIONS_GHC -fplugin ArgsPlugin
+                -fplugin-opt ArgsPlugin:17
+ #-}
+
+module Main where
+
+import Definitions
+  ( MyClass(methC) )
+
+foo :: Integer
+foo = methC
+
+main :: IO ()
+main = do
+  putStr "foo = "
+  print foo
diff --git a/testsuite/tests/tcplugins/TcPlugin_Args.stdout b/testsuite/tests/tcplugins/TcPlugin_Args.stdout
new file mode 100644
index 0000000000..7ca681d008
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_Args.stdout
@@ -0,0 +1 @@
+foo = 17
diff --git a/testsuite/tests/tcplugins/TcPlugin_Nullary.hs b/testsuite/tests/tcplugins/TcPlugin_Nullary.hs
new file mode 100644
index 0000000000..a45a326094
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_Nullary.hs
@@ -0,0 +1,13 @@
+{-# OPTIONS_GHC -dcore-lint #-}
+{-# OPTIONS_GHC -fplugin NullaryPlugin #-}
+
+module TcPlugin_Nullary where
+
+import Definitions
+  ( Nullary )
+
+foo :: Nullary => ()
+foo = ()
+
+bar :: ()
+bar = foo
diff --git a/testsuite/tests/tcplugins/TcPlugin_Nullary.stderr b/testsuite/tests/tcplugins/TcPlugin_Nullary.stderr
new file mode 100644
index 0000000000..b09af8d727
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_Nullary.stderr
@@ -0,0 +1 @@
+[4 of 4] Compiling TcPlugin_Nullary ( TcPlugin_Nullary.hs, TcPlugin_Nullary.o )
diff --git a/testsuite/tests/tcplugins/TcPlugin_TyFam.hs b/testsuite/tests/tcplugins/TcPlugin_TyFam.hs
new file mode 100644
index 0000000000..a562796a6b
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_TyFam.hs
@@ -0,0 +1,14 @@
+{-# OPTIONS_GHC -dcore-lint #-}
+{-# OPTIONS_GHC -fplugin TyFamPlugin #-}
+
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE DataKinds, GADTs, ScopedTypeVariables #-}
+
+module TcPlugin_TyFam where
+
+import Definitions
+  ( MyTyFam )
+
+foo :: proxy a -> proxy b -> MyTyFam a a -> ()
+foo _ _ x = x
+
diff --git a/testsuite/tests/tcplugins/TcPlugin_TyFam.stderr b/testsuite/tests/tcplugins/TcPlugin_TyFam.stderr
new file mode 100644
index 0000000000..3b87222521
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_TyFam.stderr
@@ -0,0 +1 @@
+[4 of 4] Compiling TcPlugin_TyFam   ( TcPlugin_TyFam.hs, TcPlugin_TyFam.o )
diff --git a/testsuite/tests/tcplugins/TyFamPlugin.hs b/testsuite/tests/tcplugins/TyFamPlugin.hs
new file mode 100644
index 0000000000..523bdc10c1
--- /dev/null
+++ b/testsuite/tests/tcplugins/TyFamPlugin.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module TyFamPlugin where
+-- Solving an equality constraint involving type families.
+
+-- base
+import Data.Maybe
+  ( catMaybes )
+
+-- ghc
+import GHC.Builtin.Types
+  ( unitTy )
+import GHC.Core
+  ( Expr(Coercion) )
+import GHC.Core.Coercion
+  ( mkUnivCo )
+import GHC.Core.Predicate
+  ( EqRel(NomEq), Pred(EqPred)
+  , classifyPredType
+  )
+import GHC.Core.TyCo.Rep
+  ( Type, UnivCoProvenance(PluginProv) )
+import GHC.Core.Type
+  ( eqType, mkTyConApp, splitTyConApp_maybe )
+import GHC.Plugins
+  ( Plugin )
+import GHC.Tc.Plugin
+  ( TcPluginM
+  , unsafeTcPluginTcM
+  )
+import GHC.Tc.Types
+  ( TcPluginResult(..) )
+import GHC.Tc.Types.Constraint
+  ( Ct(..), CanEqLHS(..)
+  , ctPred
+  )
+import GHC.Tc.Types.Evidence
+  ( EvTerm(EvExpr), Role(Nominal) )
+
+-- common
+import Common
+  ( PluginDefs(..)
+  , mkPlugin
+  )
+
+--------------------------------------------------------------------------------
+
+-- This plugin solves Wanted constraints of the form "MyTyFam a a ~ ()".
+--
+-- It does so by looking through the Wanted constraints for equality constraints
+-- whose left hand side is a type-family application "MyTyFam arg1 arg2",
+-- such that "arg1 `eqType` arg2" returns "True",
+-- and whose left hand side is the unit type "()".
+--
+-- In such a case, the plugin creates a universal coercion
+-- with Plugin provenance to prove the equality constraint.
+
+plugin :: Plugin
+plugin = mkPlugin solver
+
+solver :: [String]
+       -> PluginDefs -> [Ct] -> [Ct] -> [Ct]
+       -> TcPluginM TcPluginResult
+solver _args defs _gs _ds ws = do
+  solved <- catMaybes <$> traverse ( solveCt defs ) ws
+  pure $ TcPluginOk solved []
+
+-- Solve `MyTyFam a a ~ ()`.
+solveCt :: PluginDefs -> Ct -> TcPluginM ( Maybe (EvTerm, Ct) )
+solveCt ( PluginDefs {..} ) ct@( classifyPredType . ctPred -> EqPred NomEq lhs rhs )
+  | Just ( tyFam, [arg1, arg2] ) <- splitTyConApp_maybe lhs
+  , tyFam == myTyFam
+  , arg1 `eqType` arg2
+  , rhs `eqType` unitTy
+  , let
+      evTerm :: EvTerm
+      evTerm = EvExpr . Coercion
+             $ mkUnivCo ( PluginProv "TyFamPlugin" ) Nominal lhs rhs
+  = pure $ Just ( evTerm, ct )
+solveCt _ ct = pure Nothing
diff --git a/testsuite/tests/tcplugins/all.T b/testsuite/tests/tcplugins/all.T
new file mode 100644
index 0000000000..1fe0727e0d
--- /dev/null
+++ b/testsuite/tests/tcplugins/all.T
@@ -0,0 +1,54 @@
+
+# See NullaryPlugin.hs for a description of this plugin.
+test('TcPlugin_Nullary'
+    , [ extra_files(
+        [ 'Definitions.hs'
+        , 'Common.hs'
+        , 'NullaryPlugin.hs'
+        , 'TcPlugin_Nullary.hs'
+        ])
+      ]
+    , multi_compile
+    , [ 'TcPlugin_Nullary.hs'
+      , [ ('Definitions.hs', '')
+        , ('Common.hs', '')
+        , ('NullaryPlugin.hs', '')
+        ]
+      ,'-dynamic -package ghc' if have_dynamic() else '-package ghc']
+    )
+
+# See ArgsPlugin.hs for a description of this plugin.
+test('TcPlugin_Args'
+    , [ extra_files(
+        [ 'Definitions.hs'
+        , 'Common.hs'
+        , 'ArgsPlugin.hs'
+        , 'TcPlugin_Args.hs'
+        ])
+      ]
+    , multi_compile_and_run
+    , [ 'TcPlugin_Args.hs'
+      , [ ('Definitions.hs', '')
+        , ('Common.hs', '')
+        , ('ArgsPlugin.hs', '')
+        ]
+      ,'-dynamic -package ghc' if have_dynamic() else '-package ghc']
+    )
+
+# See TyFamPlugin.hs for a description of this plugin.
+test('TcPlugin_TyFam'
+    , [ extra_files(
+        [ 'Definitions.hs'
+        , 'Common.hs'
+        , 'TyFamPlugin.hs'
+        , 'TcPlugin_TyFam.hs'
+        ])
+      ]
+    , multi_compile
+    , [ 'TcPlugin_TyFam.hs'
+      , [ ('Definitions.hs', '')
+        , ('Common.hs', '')
+        , ('TyFamPlugin.hs', '')
+        ]
+      ,'-dynamic -package ghc' if have_dynamic() else '-package ghc']
+    )