Rework effectful-plugin, add support for GHC 9.4 and 9.6 (#130)

This commit is contained in:
Andrzej Rybczak 2023-01-22 22:11:53 +01:00 committed by GitHub
parent 0eeaf136b5
commit 3f425be2c2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 302 additions and 22 deletions

View File

@ -133,7 +133,7 @@ jobs:
- name: cache (tools)
uses: actions/cache@v2
with:
key: ${{ runner.os }}-${{ matrix.compiler }}-tools-67f405ea
key: ${{ runner.os }}-${{ matrix.compiler }}-tools-87e8ffab
path: ~/.haskell-ci-tools
- name: install cabal-plan
run: |
@ -156,7 +156,7 @@ jobs:
run: |
touch cabal.project
echo "packages: $GITHUB_WORKSPACE/source/effectful-core" >> cabal.project
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then echo "packages: $GITHUB_WORKSPACE/source/effectful-plugin" >> cabal.project ; fi
echo "packages: $GITHUB_WORKSPACE/source/effectful-plugin" >> cabal.project
echo "packages: $GITHUB_WORKSPACE/source/effectful-th" >> cabal.project
echo "packages: $GITHUB_WORKSPACE/source/effectful" >> cabal.project
cat cabal.project
@ -182,13 +182,13 @@ jobs:
touch cabal.project
touch cabal.project.local
echo "packages: ${PKGDIR_effectful_core}" >> cabal.project
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then echo "packages: ${PKGDIR_effectful_plugin}" >> cabal.project ; fi
echo "packages: ${PKGDIR_effectful_plugin}" >> cabal.project
echo "packages: ${PKGDIR_effectful_th}" >> cabal.project
echo "packages: ${PKGDIR_effectful}" >> cabal.project
echo "package effectful-core" >> cabal.project
echo " ghc-options: -Werror=missing-methods" >> cabal.project
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then echo "package effectful-plugin" >> cabal.project ; fi
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then echo " ghc-options: -Werror=missing-methods" >> cabal.project ; fi
echo "package effectful-plugin" >> cabal.project
echo " ghc-options: -Werror=missing-methods" >> cabal.project
echo "package effectful-th" >> cabal.project
echo " ghc-options: -Werror=missing-methods" >> cabal.project
echo "package effectful" >> cabal.project
@ -231,8 +231,6 @@ jobs:
run: |
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then cd ${PKGDIR_effectful_core} || false ; fi
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then doctest -XHaskell2010 -XBangPatterns -XConstraintKinds -XDataKinds -XDeriveFunctor -XDeriveGeneric -XFlexibleContexts -XFlexibleInstances -XGADTs -XGeneralizedNewtypeDeriving -XLambdaCase -XMultiParamTypeClasses -XNoStarIsType -XRankNTypes -XRoleAnnotations -XScopedTypeVariables -XStandaloneDeriving -XTupleSections -XTypeApplications -XTypeFamilies -XTypeOperators src ; fi
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then cd ${PKGDIR_effectful_plugin} || false ; fi
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then doctest -XHaskell2010 -XBangPatterns -XConstraintKinds -XDataKinds -XDeriveFunctor -XDeriveGeneric -XFlexibleContexts -XFlexibleInstances -XGADTs -XGeneralizedNewtypeDeriving -XLambdaCase -XMultiParamTypeClasses -XNoStarIsType -XRankNTypes -XRecordWildCards -XRoleAnnotations -XScopedTypeVariables -XStandaloneDeriving -XTupleSections -XTypeApplications -XTypeFamilies -XTypeOperators src ; fi
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then cd ${PKGDIR_effectful_th} || false ; fi
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then doctest -XHaskell2010 -XBangPatterns -XConstraintKinds -XDataKinds -XDeriveFunctor -XDeriveGeneric -XFlexibleContexts -XFlexibleInstances -XGADTs -XGeneralizedNewtypeDeriving -XLambdaCase -XMultiParamTypeClasses -XNoStarIsType -XRankNTypes -XRecordWildCards -XRoleAnnotations -XScopedTypeVariables -XStandaloneDeriving -XTupleSections -XTypeApplications -XTypeFamilies -XTypeOperators src ; fi
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then cd ${PKGDIR_effectful} || false ; fi
@ -241,8 +239,8 @@ jobs:
run: |
cd ${PKGDIR_effectful_core} || false
${CABAL} -vnormal check
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then cd ${PKGDIR_effectful_plugin} || false ; fi
if [ $((HCNUMVER < 90400)) -ne 0 ] ; then ${CABAL} -vnormal check ; fi
cd ${PKGDIR_effectful_plugin} || false
${CABAL} -vnormal check
cd ${PKGDIR_effectful_th} || false
${CABAL} -vnormal check
cd ${PKGDIR_effectful} || false

View File

@ -1,6 +1,8 @@
branches: master
doctest: <9.3
doctest-skip: effectful-plugin
tests: True
benchmarks: True

View File

@ -1,2 +1,5 @@
# effectful-plugin-1.1.0.0 (2023-??-??)
* Add support for GHC 9.4 and 9.6.
# effectful-plugin-1.0.0.0 (2022-07-13)
* Initial release.

View File

@ -1,7 +1,7 @@
cabal-version: 2.4
build-type: Simple
name: effectful-plugin
version: 1.0.0.0
version: 1.1.0.0
license: BSD-3-Clause
license-file: LICENSE
category: Control
@ -17,7 +17,7 @@ description:
extra-source-files: CHANGELOG.md
README.md
tested-with: GHC ==8.8.4 || ==8.10.7 || ==9.0.2 || ==9.2.5
tested-with: GHC ==8.8.4 || ==8.10.7 || ==9.0.2 || ==9.2.5 || ==9.4.4
bug-reports: https://github.com/haskell-effectful/effectful/issues
source-repository head
@ -27,10 +27,6 @@ source-repository head
common language
ghc-options: -Wall -Wcompat -Wno-unticked-promoted-constructors
-- The plugin doesn't build with GHC 9.4 yet.
if !impl(ghc < 9.3)
buildable: False
default-language: Haskell2010
default-extensions: BangPatterns
@ -61,13 +57,17 @@ library
build-depends: base >= 4.13 && < 5
, effectful-core >= 1.0.0.0 && < 3.0.0.0
, containers >= 0.5
, ghc >= 8.6 && < 9.3
, ghc-tcplugins-extra >= 0.3 && < 0.5
, ghc >= 8.6 && < 9.7
hs-source-dirs: src
if impl(ghc < 9.4)
build-depends: ghc-tcplugins-extra >= 0.3 && < 0.5
if impl(ghc < 9.4)
hs-source-dirs: src-legacy
else
hs-source-dirs: src
exposed-modules: Effectful.Plugin
Effectful.Plugin.Internal
test-suite plugin-tests
import: language

View File

@ -1,6 +1,6 @@
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
module Effectful.Plugin.Internal (Plugin, Names, makePlugin) where
module Effectful.Plugin (plugin) where
import Data.Function (on)
import Data.IORef (IORef, modifyIORef, newIORef, readIORef)
@ -44,6 +44,9 @@ import TcType (tcSplitTyConApp)
import Unify (tcUnifyTy)
#endif
plugin :: Plugin
plugin = makePlugin [("effectful", "Effectful.Internal.Effect", ":>")]
-- | A list of unique, unambiguous Haskell names in the format of @(packageName, moduleName, identifier)@.
type Names = [(String, String, String)]

View File

@ -1,6 +1,280 @@
{-# LANGUAGE CPP #-}
module Effectful.Plugin (plugin) where
import Effectful.Plugin.Internal (Plugin, makePlugin)
import Data.Either
import Data.Function
import Data.IORef
import Data.Maybe
import Data.Set (Set)
import Data.Traversable
import qualified Data.Set as Set
import GHC.Core.Class (Class)
import GHC.Core.InstEnv (InstEnvs, lookupInstEnv)
import GHC.Core.TyCo.Rep (PredType, Type)
import GHC.Core.TyCo.Subst
import GHC.Core.TyCon (tyConClass_maybe)
import GHC.Core.Type (splitAppTys)
import GHC.Core.Unify (tcUnifyTy)
import GHC.Driver.Config.Finder (initFinderOpts)
import GHC.Driver.Env (hsc_home_unit, hsc_units)
import GHC.Driver.Env.Types (HscEnv (..))
import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
import GHC.Tc.Plugin (getTopEnv, lookupOrig, tcLookupClass, tcPluginIO)
import GHC.Tc.Solver.Monad (newWantedEq, runTcSEarlyAbort)
import GHC.Tc.Types
( TcPlugin (..)
, TcPluginM
, TcPluginSolveResult (..)
, unsafeTcPluginTcM
)
import GHC.Tc.Types.Constraint
( Ct (..)
, CtEvidence (..)
, CtLoc
, ctPred
, emptyRewriterSet
)
import GHC.Tc.Types.Evidence (EvBindsVar, Role (..))
import GHC.Tc.Utils.Env (tcGetInstEnvs)
import GHC.Tc.Utils.TcType (tcSplitTyConApp, eqType, nonDetCmpType)
import GHC.Types.Name (mkTcOcc)
import GHC.Types.Unique.FM (emptyUFM)
import GHC.Unit.Finder (FindResult (..), findPluginModule)
import GHC.Unit.Module (Module, ModuleName, mkModuleName)
import GHC.Utils.Outputable (Outputable (..), showSDocUnsafe)
import GHC.Utils.Panic (panicDoc)
#if __GLASGOW_HASKELL__ >= 906
type TCvSubst = Subst
#endif
plugin :: Plugin
plugin = makePlugin [("effectful", "Effectful.Internal.Effect", ":>")]
plugin = defaultPlugin
{ tcPlugin = \_ -> Just TcPlugin
{ tcPluginInit = initPlugin "Effectful.Internal.Effect" ":>"
, tcPluginRewrite = \_ -> emptyUFM
, tcPluginSolve = solveFakedep
, tcPluginStop = \_ -> pure ()
}
, pluginRecompile = purePlugin
}
----------------------------------------
data EffGiven = EffGiven
{ givenEffHead :: Type
, givenEff :: Type
, givenEs :: Type
}
instance Show EffGiven where
show (EffGiven _ e es) =
"[G] " ++ showSDocUnsafe (ppr e) <> " :> " <> showSDocUnsafe (ppr es)
data EffWanted = EffWanted
{ wantedEffHead :: Type
, wantedEff :: Type
, wantedEs :: Type
, wantedLoc :: CtLoc
}
instance Show EffWanted where
show (EffWanted _ e es _) =
"[W] " <> showSDocUnsafe (ppr e) <> " :> " <> showSDocUnsafe (ppr es)
newtype OrdType = OrdType {unOrdType :: Type}
instance Eq OrdType where
(==) = eqType `on` unOrdType
instance Ord OrdType where
compare = nonDetCmpType `on` unOrdType
----------------------------------------
type VisitedSet = Set (OrdType, OrdType)
initPlugin :: String -> String -> TcPluginM (Class, IORef VisitedSet)
initPlugin modName clsName = do
recMod <- lookupModule (mkModuleName modName)
cls <- tcLookupClass =<< lookupOrig recMod (mkTcOcc clsName)
visited <- tcPluginIO $ newIORef Set.empty
pure (cls, visited)
where
lookupModule :: ModuleName -> TcPluginM Module
lookupModule mod_nm = do
hsc_env <- getTopEnv
let dflags = hsc_dflags hsc_env
fopts = initFinderOpts dflags
fc = hsc_FC hsc_env
units = hsc_units hsc_env
home_unit = hsc_home_unit hsc_env
tcPluginIO (findPluginModule fc fopts units (Just home_unit) mod_nm) >>= \case
Found _ md -> pure md
_ -> panicDoc "Couldn't find module" (ppr mod_nm)
solveFakedep
:: (Class, IORef VisitedSet)
-> EvBindsVar
-> [Ct]
-> [Ct]
-> TcPluginM TcPluginSolveResult
solveFakedep (elemCls, visitedRef) _ allGivens allWanteds = do
-- We're given two lists of constraints here:
--
-- - 'allGivens' are constraints already in our context,
--
-- - 'allWanteds' are constraints that need to be solved.
--
-- In the following notes, the words "give/given" and "want/wanted" all refer
-- to this specific technical concept: given constraints are those that we can
-- use, and wanted constraints are those that we need to solve.
--tcPluginIO $ do
-- putStrLn $ "Givens: " <> show (showSDocUnsafe . ppr <$> allGivens)
-- putStrLn $ "Wanteds: " <> show (showSDocUnsafe . ppr <$> allWanteds)
-- For each 'e :> es' we /want/ to solve (the "goal"), we need to eventually
-- correspond it to another unique /given/ 'e :> es' that will make the
-- program typecheck (the "solution").
globals <- unsafeTcPluginTcM tcGetInstEnvs
let solns = mapMaybe (solve globals) effWanteds
-- Now we need to tell GHC the solutions. The way we do this is to generate a
-- new equality constraint, like 'State e ~ State Int', so that GHC's
-- constraint solver will know that 'e' must be 'Int'.
eqns <- for solns $ \(goal, soln) -> do
let wantedEq = newWantedEq (wantedLoc goal) emptyRewriterSet Nominal
(wantedEff goal) (givenEff soln)
(eqn, _) <- unsafeTcPluginTcM $ runTcSEarlyAbort wantedEq
pure (CNonCanonical eqn, (OrdType $ wantedEff goal, OrdType $ givenEff soln))
-- For any solution we've generated, we need to be careful not to generate it
-- again, or we might end up generating infinitely many solutions. So, we
-- record any already generated solution in a set.
visitedSolnPairs <- tcPluginIO $ readIORef visitedRef
let solnEqns = fmap fst . flip filter eqns $ \(_, pair) -> Set.notMember pair visitedSolnPairs
tcPluginIO $ do
modifyIORef visitedRef (Set.union $ Set.fromList $ map snd eqns)
--putStrLn $ "Emitting: " <> showSDocUnsafe (ppr solnEqns)
pure $ TcPluginSolveResult [] [] solnEqns
where
-- The only type of constraint we're interested in solving are 'e :> es'
-- constraints. Therefore, we extract these constraints out of the
-- 'allGivens' and 'allWanted's.
effGivens = mapMaybe maybeEffGiven allGivens
(otherWantedTys, effWanteds) = partitionEithers $ map splitWanteds allWanteds
-- We store a list of the types of all given constraints, which will be
-- useful later.
allGivenTys = ctPred <$> allGivens
-- Determine if there is a unique solution to a goal from a set of
-- candidates.
solve
:: InstEnvs
-> EffWanted
-> Maybe (EffWanted, EffGiven)
solve globals goal = case unifiableCands of
-- If there's already only one unique solution, commit to it; in the worst
-- case where it doesn't actually match, we get a cleaner error message
-- like "Unable to match (State String) to (State Int)" instead of a type
-- ambiguity error.
[(soln, _)] -> Just (goal, soln)
_ ->
-- Otherwise, the second criteria comes in: the candidate must satisfy
-- all other constraints we /want/ to solve. For example, when we want
-- to solve '(State a :> es, Num a)`, the candidate 'State Int :> es'
-- will do the job, because it satisfied 'Num a'; however 'State String
-- :> es' will be excluded.
let satisfiableCands = filter (satisfiable globals) unifiableCands
in -- Finally, if there is a unique candidate remaining, we use it as
-- the solution; otherwise we don't solve anything.
case satisfiableCands of
[(soln, _)] -> Just (goal, soln)
_ -> Nothing
where
-- Apart from ':>' constraints in the context, the effects already
-- hardwired into the effect stack type, like those in 'A : B : C : es'
-- also need to be considered. So here we extract that for them to be
-- considered simultaneously with regular ':>' constraints.
cands = extractExtraGivens (wantedEs goal) (wantedEs goal) <> effGivens
-- The first criteria is that the candidate constraint must /unify/ with
-- the goal. This means that the type variables in the goal can be
-- instantiated in a way so that the goal becomes equal to the
-- candidate. For example, the candidates 'State Int :> es' and 'State
-- String :> es' both unify with the goal 'State s :> es'.
unifiableCands = mapMaybe (unifiableWith goal) cands
-- Extract the heads of a type like 'A : B : C : es' into 'FakedepGiven's.
extractExtraGivens :: Type -> Type -> [EffGiven]
extractExtraGivens fullEs es = case splitAppTys es of
(_colon, [_kind, e, es']) ->
let (dtHead, _tyArgs) = splitAppTys e
in EffGiven { givenEffHead = dtHead
, givenEff = e
, givenEs = fullEs
} : extractExtraGivens fullEs es'
_ -> []
-- Determine whether a given constraint is of form 'e :> es'.
maybeEffGiven :: Ct -> Maybe EffGiven
maybeEffGiven = \case
CDictCan { cc_class = cls
, cc_tyargs = [eff, es]
} ->
if cls == elemCls
then Just EffGiven { givenEffHead = fst $ splitAppTys eff
, givenEff = eff
, givenEs = es
}
else Nothing
_ -> Nothing
-- Determine whether a wanted constraint is of form 'e :> es'.
splitWanteds :: Ct -> Either PredType EffWanted
splitWanteds = \case
ct@CDictCan { cc_ev = CtWanted { ctev_loc = loc }
, cc_class = cls
, cc_tyargs = [eff, es]
} ->
if cls == elemCls
then Right EffWanted { wantedEffHead = fst $ splitAppTys eff
, wantedEff = eff
, wantedEs = es
, wantedLoc = loc
}
else Left $ ctPred ct
ct -> Left $ ctPred ct
-- Given a wanted constraint and a given constraint, unify them and give
-- back a substitution that can be applied to the wanted to make it equal to
-- the given.
unifiableWith :: EffWanted -> EffGiven -> Maybe (EffGiven, TCvSubst)
unifiableWith goal cand =
if wantedEs goal `eqType` givenEs cand
&& wantedEffHead goal `eqType` givenEffHead cand
then (cand, ) <$> tcUnifyTy (wantedEff goal) (givenEff cand)
else Nothing
-- Check whether a candidate can satisfy all the wanted constraints.
satisfiable :: InstEnvs -> (EffGiven, TCvSubst) -> Bool
satisfiable globals (_, subst) = flip all wantedsInst $ \wanted ->
if Set.member (OrdType wanted) givensInst
then True -- Can we find this constraint in our local context?
else case tcSplitTyConApp wanted of
(con, args) ->
-- If not, lookup the global environment.
case tyConClass_maybe con of
Nothing -> False
Just cls ->
let (res, _, _) = lookupInstEnv False globals cls args
in not $ null res
where
-- The wanteds after unification.
wantedsInst = substTys subst otherWantedTys
-- The local given context after unification.
givensInst = Set.fromList (OrdType <$> substTys subst allGivenTys)