Commit e309cb76 authored by sheaf's avatar sheaf
Browse files

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.
parent 41d6cfc4
{-# 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
{-# 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 ()
}
{-# 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 )
{-# 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
{-# 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
{-# OPTIONS_GHC -dcore-lint #-}
{-# OPTIONS_GHC -fplugin NullaryPlugin #-}
module TcPlugin_Nullary where
import Definitions
( Nullary )
foo :: Nullary => ()
foo = ()
bar :: ()
bar = foo
[4 of 4] Compiling TcPlugin_Nullary ( TcPlugin_Nullary.hs, TcPlugin_Nullary.o )
{-# 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
[4 of 4] Compiling TcPlugin_TyFam ( TcPlugin_TyFam.hs, TcPlugin_TyFam.o )
{-# 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
# 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']
)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment