polysemy-plugin 0.2.5.2 → 0.4.5.3
raw patch · 11 files changed
Files
- ChangeLog.md +39/−0
- polysemy-plugin.cabal +113/−90
- src/Polysemy/Plugin.hs +4/−0
- src/Polysemy/Plugin/Fundep.hs +214/−62
- src/Polysemy/Plugin/Fundep/Stuff.hs +55/−13
- src/Polysemy/Plugin/Fundep/Unification.hs +60/−69
- test/AmbiguousSpec.hs +67/−0
- test/BadSpec.hs +0/−38
- test/ExampleSpec.hs +0/−1
- test/InsertSpec.hs +22/−0
- test/TypeErrors.hs +55/−2
ChangeLog.md view
@@ -1,5 +1,44 @@ # Changelog for polysemy-plugin +## Unreleased++## 0.4.5.0 (2023-04-09)++### Other Changes++* Support GHC 9.6++## 0.4.4.0 (2022-12-27)++* Support GHC 9.4++## 0.4.3.1 (2022-07-11)++* Add a missing pattern match that was hit by a user.++## 0.4.3.0 (2021-11-23)++* Support GHC 9.2.1+* Fix a regression that prevented disambiguation in some cases.++## 0.4.2.0 (2021-11-16)++- Support for `polysemy-1.7.0.0`++## 0.4.1.0 (2021-10-22)++- The plugin can now use instances in scope to help solve ambiguous type+ variables.++## 0.4.0.0 (2021-07-12)++* Support GHC 9.0.1++## 0.3.0.0 (2021-03-30)++### Breaking Changes+* Dropped support for GHC 8.4+ ## 0.2.5.2 (2020-11-01) - Fixed crashes stemming from unused optimization passes
polysemy-plugin.cabal view
@@ -1,104 +1,127 @@-cabal-version: 2.0-name: polysemy-plugin-version: 0.2.5.2-license: BSD3-license-file: LICENSE-copyright: 2019 Sandy Maguire-maintainer: sandy@sandymaguire.me-author: Sandy Maguire-homepage: https://github.com/isovector/polysemy#readme-bug-reports: https://github.com/isovector/polysemy/issues-synopsis: Disambiguate obvious uses of effects.-description:- Please see the README on GitHub at <https://github.com/isovector/polysemy/tree/master/polysemy-plugin#readme>+cabal-version: 2.0 -category: Polysemy-build-type: Custom+-- This file has been generated from package.yaml by hpack version 0.36.1.+--+-- see: https://github.com/sol/hpack++name: polysemy-plugin+version: 0.4.5.3+synopsis: Disambiguate obvious uses of effects.+description: Please see the README on GitHub at <https://github.com/polysemy-research/polysemy/tree/master/polysemy-plugin#readme>+category: Polysemy+homepage: https://github.com/polysemy-research/polysemy#readme+bug-reports: https://github.com/polysemy-research/polysemy/issues+author: Sandy Maguire+maintainer: sandy@sandymaguire.me+copyright: 2019 Sandy Maguire+license: BSD3+license-file: LICENSE+build-type: Custom extra-source-files: README.md ChangeLog.md source-repository head- type: git- location: https://github.com/isovector/polysemy+ type: git+ location: https://github.com/polysemy-research/polysemy custom-setup- setup-depends:- Cabal >=3.0.1.0 && <3.1,- base >=4.9 && <5,- cabal-doctest >=1.0.6 && <1.1+ setup-depends:+ Cabal <3.13+ , base >=4.9 && <5+ , cabal-doctest >=1.0.6 && <1.1 flag corelint- description: Perform the corelint tests- default: False- manual: True+ description: Perform the corelint tests+ manual: True+ default: False library- exposed-modules:- Polysemy.Plugin- Polysemy.Plugin.Fundep- Polysemy.Plugin.Fundep.Stuff- Polysemy.Plugin.Fundep.Unification- Polysemy.Plugin.Fundep.Utils-- hs-source-dirs: src- other-modules: Paths_polysemy_plugin- autogen-modules: Paths_polysemy_plugin- default-language: Haskell2010- default-extensions:- DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds- RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications- TypeOperators TypeFamilies UnicodeSyntax-- build-depends:- base >=4.9 && <5,- containers >=0.5 && <0.7,- ghc >=8.4.4 && <9,- ghc-tcplugins-extra >=0.3 && <0.5,- polysemy >=1.3 && <1.5,- syb ==0.7.*,- transformers >=0.5.2.0 && <0.6+ exposed-modules:+ Polysemy.Plugin+ Polysemy.Plugin.Fundep+ Polysemy.Plugin.Fundep.Stuff+ Polysemy.Plugin.Fundep.Unification+ Polysemy.Plugin.Fundep.Utils+ other-modules:+ Paths_polysemy_plugin+ autogen-modules:+ Paths_polysemy_plugin+ hs-source-dirs:+ src+ default-extensions:+ DataKinds+ DeriveFunctor+ FlexibleContexts+ GADTs+ LambdaCase+ PolyKinds+ RankNTypes+ ScopedTypeVariables+ StandaloneDeriving+ TypeApplications+ TypeOperators+ TypeFamilies+ UnicodeSyntax+ build-depends:+ base >=4.9 && <5+ , containers >=0.5 && <0.8+ , ghc >=8.6.5 && <10+ , ghc-tcplugins-extra >=0.3 && <0.6+ , polysemy >=1.7+ , syb ==0.7.*+ , transformers >=0.5.2.0 && <0.7+ default-language: Haskell2010 test-suite polysemy-plugin-test- type: exitcode-stdio-1.0- main-is: Main.hs- build-tool-depends: hspec-discover:hspec-discover -any- hs-source-dirs: test- other-modules:- BadSpec- DoctestSpec- ExampleSpec- LegitimateTypeErrorSpec- MultipleVarsSpec- PluginSpec- TypeErrors- VDQSpec- Paths_polysemy_plugin- Build_doctests-- autogen-modules: Build_doctests- default-language: Haskell2010- default-extensions:- DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds- RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications- TypeOperators TypeFamilies UnicodeSyntax-- ghc-options:- -threaded -rtsopts -with-rtsopts=-N -fplugin=Polysemy.Plugin-- build-depends:- base >=4.9 && <5,- containers >=0.5 && <0.7,- doctest >=0.16.0.1 && <0.17,- ghc >=8.4.4 && <9,- ghc-tcplugins-extra >=0.3 && <0.5,- hspec >=2.6.0 && <3,- inspection-testing >=0.4.2 && <0.5,- polysemy >=1.3.0.0 && <1.5,- polysemy-plugin -any,- should-not-typecheck >=2.1.0 && <3,- syb ==0.7.*,- transformers >=0.5.2.0 && <0.6-- if flag(corelint)- ghc-options: -dcore-lint -dsuppress-all+ type: exitcode-stdio-1.0+ main-is: Main.hs+ other-modules:+ AmbiguousSpec+ DoctestSpec+ ExampleSpec+ InsertSpec+ LegitimateTypeErrorSpec+ MultipleVarsSpec+ PluginSpec+ TypeErrors+ VDQSpec+ Paths_polysemy_plugin+ Build_doctests+ autogen-modules:+ Paths_polysemy_plugin+ Build_doctests+ hs-source-dirs:+ test+ default-extensions:+ DataKinds+ DeriveFunctor+ FlexibleContexts+ GADTs+ LambdaCase+ PolyKinds+ RankNTypes+ ScopedTypeVariables+ StandaloneDeriving+ TypeApplications+ TypeOperators+ TypeFamilies+ UnicodeSyntax+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -fplugin=Polysemy.Plugin+ build-depends:+ base >=4.9 && <5+ , containers >=0.5 && <0.8+ , doctest >=0.16.0.1 && <0.25+ , ghc >=8.6.5 && <10+ , ghc-tcplugins-extra >=0.3 && <0.6+ , hspec >=2.6.0 && <3+ , hspec-discover+ , inspection-testing >=0.4.2 && <0.7+ , polysemy >=1.3.0.0+ , polysemy-plugin+ , should-not-typecheck >=2.1.0 && <3+ , syb ==0.7.*+ , transformers >=0.5.2.0 && <0.7+ default-language: Haskell2010+ if flag(corelint)+ ghc-options: -dcore-lint -dsuppress-all
src/Polysemy/Plugin.hs view
@@ -63,7 +63,11 @@ import Polysemy.Plugin.Fundep +#if __GLASGOW_HASKELL__ >= 900+import GHC.Plugins+#else import GhcPlugins+#endif ------------------------------------------------------------------------------ plugin :: Plugin
src/Polysemy/Plugin/Fundep.hs view
@@ -1,6 +1,8 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE CPP #-} ------------------------------------------------------------------------------ -- The MIT License (MIT)@@ -35,25 +37,68 @@ module Polysemy.Plugin.Fundep (fundepPlugin) where import Control.Monad+import Control.Monad.Trans.Class (lift)+import Control.Monad.Trans.State import Data.Bifunctor import Data.Coerce+import Data.Function (on) import Data.IORef import qualified Data.Map as M import Data.Maybe+import Data.Set (Set) import qualified Data.Set as S+import Data.Traversable (for) import Polysemy.Plugin.Fundep.Stuff import Polysemy.Plugin.Fundep.Unification import Polysemy.Plugin.Fundep.Utils-import TcEvidence-import TcPluginM (TcPluginM, tcPluginIO)-import TcRnTypes++#if __GLASGOW_HASKELL__ >= 906+#define SUBST Subst+#define GET_TYVAR getTyVar_maybe+import GHC.Core.TyCo.Subst (SUBST)+import GHC.Core.TyCo.Compare (eqType, nonDetCmpType)+#else+#define SUBST TCvSubst+#define GET_TYVAR tcGetTyVar_maybe+#endif++#if __GLASGOW_HASKELL__ >= 912+import GHC.Tc.Types.CtLoc+#endif++#if __GLASGOW_HASKELL__ >= 900+import GHC.Builtin.Types.Prim (alphaTys)+import GHC.Plugins (idType, tyConClass_maybe, ppr, Outputable, sep, text, (<+>), parens, emptyUFM)+import GHC.Tc.Types.Evidence+import GHC.Tc.Plugin (TcPluginM, tcPluginIO)+import GHC.Tc.Types+import GHC.Tc.Types.Constraint+import GHC.Tc.Utils.Env (tcGetInstEnvs)+import GHC.Tc.Utils.TcType (tcSplitPhiTy, tcSplitTyConApp, GET_TYVAR, tcSplitAppTy_maybe)+import GHC.Tc.Solver.Monad hiding (tcLookupClass)+import GHC.Core.Class (classTyCon)+import GHC.Core.InstEnv (lookupInstEnv, is_dfun)+import GHC.Core.Type+import GHC.Utils.Monad (allM, anyM)++#else #if __GLASGOW_HASKELL__ >= 810 import Constraint #endif++import Class (classTyCon)+import GhcPlugins (idType, tyConClass_maybe, ppr, Outputable, sep, text, (<+>), parens)+import Inst (tcGetInstEnvs)+import InstEnv (lookupInstEnv, is_dfun)+import MonadUtils (allM, anyM)+import TcEvidence+import TcPluginM (tcPluginIO)+import TcRnTypes+import TcType (tcSplitPhiTy, tcSplitTyConApp, GET_TYVAR, tcSplitAppTy_maybe) import TcSMonad hiding (tcLookupClass) import Type--+import TysPrim (alphaTys)+#endif fundepPlugin :: TcPlugin fundepPlugin = TcPlugin@@ -62,10 +107,25 @@ <*> polysemyStuff , tcPluginSolve = solveFundep , tcPluginStop = const $ pure ()+#if __GLASGOW_HASKELL__ >= 904+ , tcPluginRewrite = \ _ -> emptyUFM+#endif } ------------------------------------------------------------------------------+-- | Like 'PredType', but has an 'Ord' instance.+newtype PredType' = PredType' { getPredType :: PredType }+ deriving newtype Outputable++instance Eq PredType' where+ (==) = ((== EQ) .) . compare++instance Ord PredType' where+ compare = nonDetCmpType `on` getPredType+++------------------------------------------------------------------------------ -- | Corresponds to a 'Polysemy.Internal.Union.Find' constraint. For example, -- given @Member (State s) r@, we would get: data FindConstraint = FindConstraint@@ -75,12 +135,23 @@ , fcRow :: Type -- ^ @r@ } +instance Outputable FindConstraint where+ ppr FindConstraint{..} = parens $ sep+ [ text "effect name = " <+> ppr fcEffectName+ , text "effect = " <+> ppr fcEffect+ , text "row = " <+> ppr fcRow+ ] + ------------------------------------------------------------------------------ -- | Given a list of constraints, filter out the 'FindConstraint's. getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint] getFindConstraints (findClass -> cls) cts = do- cd@CDictCan{cc_class = cls', cc_tyargs = [_, eff, r]} <- cts+#if MIN_VERSION_GLASGOW_HASKELL(9,8,0,0)+ cd@(CDictCan(DictCt{di_cls = cls', di_tys = [eff, r]})) <- cts+#else+ cd@CDictCan{cc_class = cls', cc_tyargs = [eff, r]} <- cts+#endif guard $ cls == cls' pure $ FindConstraint { fcLoc = ctLoc cd@@ -91,21 +162,69 @@ --------------------------------------------------------------------------------- | If there's only a single @Member@ in the same @r@ whose effect name--- matches and could possibly unify, return its effect (including tyvars.)+-- | Get evidence in scope that aren't the 'FindConstraint's.+getExtraEvidence :: PolysemyStuff 'Things -> [Ct] -> [PredType]+getExtraEvidence things cts = do+#if MIN_VERSION_GLASGOW_HASKELL(9,8,0,0)+ CDictCan(DictCt{di_cls = cls, di_tys = as}) <- cts+#else+ CDictCan{cc_class = cls, cc_tyargs = as} <- cts+#endif+ guard $ cls /= findClass things+ pure $ mkAppTys (mkTyConTy $ classTyCon cls) as+++------------------------------------------------------------------------------+-- | If there's a unique given @Member@ that would cause the program to+-- typecheck, use it. findMatchingEffectIfSingular- :: FindConstraint- -> [FindConstraint]- -> Maybe Type-findMatchingEffectIfSingular (FindConstraint _ eff_name wanted r) ts =- singleListToJust $ do- FindConstraint _ eff_name' eff' r' <- ts- guard $ eqType eff_name eff_name'- guard $ eqType r r'- guard $ canUnifyRecursive FunctionDef wanted eff'- pure eff'+ :: [PredType] -- ^ Extra wanteds+ -> Set PredType' -- ^ Extra givens+ -> FindConstraint -- ^ Goal+ -> [FindConstraint] -- ^ Member constraints+ -> TcM (Maybe Type)+findMatchingEffectIfSingular+ extra_wanted+ extra_given+ (FindConstraint _ eff_name wanted r)+ ts =+ let skolems = S.fromList $ foldMap (tyCoVarsOfTypeWellScoped . fcEffect) ts+ -- Which members unify with our current goal?+ results = do+ FindConstraint _ eff_name' eff' r' <- ts+ guard $ eqType eff_name eff_name'+ guard $ eqType r r'+ subst <- maybeToList $ unify (FunctionDef skolems) wanted eff'+ pure (eff', subst)+ in case results of+ [] -> pure Nothing+ -- If there is a unique member which unifies, return it.+ [(a, _)] -> pure $ Just a+ _ ->+ -- Otherwise, check if the extra wanteds give us enough information+ -- to make a unique choice.+ --+ -- For example, if we're trying to solve @Member (State a) r@, with+ -- candidates @Members (State Int, State String) r@ and can prove+ -- that @Num a@, then we can uniquely choose @State Int@.+ fmap (singleListToJust . join) $ for results $ \(eff, subst) ->+ fmap maybeToList $+ anyM (checkExtraEvidence extra_given subst) extra_wanted >>= \case+ True -> pure $ Just eff+ False -> pure Nothing +------------------------------------------------------------------------------+-- | @checkExtraEvidence givens subst c@ returns 'True' iff we can prove that+-- the constraint @c@ holds under the substitution @subst@ in the context of+-- @givens@.+checkExtraEvidence ::+ Set PredType' ->+ SUBST ->+ PredType ->+ TcM Bool+checkExtraEvidence givens subst = flip evalStateT givens . getInstance . substTy subst + ------------------------------------------------------------------------------ -- | Given an effect, compute its effect name. getEffName :: Type -> Type@@ -120,16 +239,35 @@ -> Type -> TcPluginM (Unification, Ct) mkWantedForce fc given = do+#if __GLASGOW_HASKELL__ >= 904+ ((ev, _), _) <- unsafeTcPluginTcM+ . runTcS+ $ newWantedEq (fcLoc fc) emptyRewriterSet Nominal wanted given+#else (ev, _) <- unsafeTcPluginTcM . runTcSDeriveds $ newWantedEq (fcLoc fc) Nominal wanted given+#endif pure ( Unification (OrdType wanted) (OrdType given) , CNonCanonical ev ) where wanted = fcEffect fc + ------------------------------------------------------------------------------+-- | It's very important that we don't try to unify entire effects when we're+-- in interpreter mode. It's OK to unify @T x ~ T y@, but never @e ~ T y@. This+-- function takes then "given" of an interpreter, and produces a singleton+-- skolem set iff the outermost effect to be unified is a tyvar.+skolemsForInterpreter :: Type -> Set TyVar+skolemsForInterpreter ty =+ case tcSplitAppTy_maybe ty of+ Just (GET_TYVAR -> Just skolem, _) -> S.singleton skolem+ _ -> maybe mempty S.singleton $ GET_TYVAR ty+++------------------------------------------------------------------------------ -- | Generate a wanted unification for the effect described by the -- 'FindConstraint' and the given effect --- if they can be unified in this -- context.@@ -138,51 +276,14 @@ -> SolveContext -> Type -- ^ The given effect. -> TcPluginM (Maybe (Unification, Ct))-mkWanted fc solve_ctx given =- whenA (not (mustUnify solve_ctx) || canUnifyRecursive solve_ctx wanted given) $+mkWanted fc solve_ctx given = do+ whenA (not (mustUnify solve_ctx) || isJust (unify solve_ctx wanted given)) $ mkWantedForce fc given where wanted = fcEffect fc --------------------------------------------------------------------------------- | Given a list of 'Ct's, find any that are of the form--- @[Irred] Sem r a ~ Something@, and return their @r@s.-getBogusRs :: PolysemyStuff 'Things -> [Ct] -> [Type]-getBogusRs stuff wanteds = do- CIrredCan ct _ <- wanteds- (_, [_, _, a, b]) <- pure . splitAppTys $ ctev_pred ct- maybeToList (extractRowFromSem stuff a)- ++ maybeToList (extractRowFromSem stuff b)------------------------------------------------------------------------------------ | Take the @r@ out of @Sem r a@.-extractRowFromSem :: PolysemyStuff 'Things -> Type -> Maybe Type-extractRowFromSem (semTyCon -> sem) ty = do- (tycon, [r, _]) <- splitTyConApp_maybe ty- guard $ tycon == sem- pure r------------------------------------------------------------------------------------ | Given a list of bogus @r@s, and the wanted constraints, produce bogus--- evidence terms that will prevent @IfStuck (LocateEffect _ r) _ _@ error messsages.-solveBogusError :: PolysemyStuff 'Things -> [Ct] -> [(EvTerm, Ct)]-solveBogusError stuff wanteds = do- let splitTyConApp_list = maybeToList . splitTyConApp_maybe-- let bogus = getBogusRs stuff wanteds- ct@(CIrredCan ce _) <- wanteds- (stuck, [_, _, expr, _, _]) <- splitTyConApp_list $ ctev_pred ce- guard $ stuck == ifStuckTyCon stuff- (idx, [_, _, r]) <- splitTyConApp_list expr- guard $ idx == locateEffectTyCon stuff- guard $ elem @[] (OrdType r) $ coerce bogus- pure (error "bogus proof for stuck type family", ct)--------------------------------------------------------------------------------- -- | Determine if there is exactly one wanted find for the @r@ in question. exactlyOneWantedForR :: [FindConstraint] -- ^ Wanted finds@@ -202,22 +303,70 @@ $ OrdType . fcRow <$> wanteds +------------------------------------------------------------------------------+-- | Returns 'True' if we can prove the given 'PredType' has a (fully+-- instantiated) instance. Uses 'StateT' to cache the results of any instances+-- it needs to prove in service of the original goal.+getInstance :: PredType -> StateT (Set PredType') TcM Bool+getInstance predty = do+ givens <- get+ case S.member (PredType' predty) givens of+ True -> pure True+ False ->+ let (con, apps) = tcSplitTyConApp predty+ in case tyConClass_maybe con of+ Nothing -> pure False+ Just cls -> do+ env <- lift tcGetInstEnvs+ let (mres, _, _) = lookupInstEnv False env cls apps+ case mres of+ ((inst, mapps) : _) -> do+ -- Get the instantiated type of the dictionary+ let df = piResultTys (idType $ is_dfun inst)+ $ zipWith fromMaybe alphaTys mapps+ -- pull off its resulting arguments+ let (theta, _) = tcSplitPhiTy df+ allM getInstance theta >>= \case+ True -> do+ -- Record that we can solve this instance, in case it's used+ -- elsewhere+ modify $ S.insert $ coerce predty+ pure True+ False -> pure False+ _ -> pure False++ solveFundep :: ( IORef (S.Set Unification) , PolysemyStuff 'Things )+#if __GLASGOW_HASKELL__ >= 904+ -> EvBindsVar -> [Ct] -> [Ct]+ -> TcPluginM TcPluginSolveResult+#else -> [Ct]+ -> [Ct]+ -> [Ct] -> TcPluginM TcPluginResult+#endif solveFundep _ _ _ [] = pure $ TcPluginOk [] []+#if __GLASGOW_HASKELL__ >= 904+solveFundep (ref, stuff) _ given wanted = do+#else solveFundep (ref, stuff) given _ wanted = do+#endif let wanted_finds = getFindConstraints stuff wanted given_finds = getFindConstraints stuff given+ extra_wanted = getExtraEvidence stuff wanted+ extra_given = S.fromList $ coerce $ getExtraEvidence stuff given eqs <- forM wanted_finds $ \fc -> do let r = fcRow fc- case findMatchingEffectIfSingular fc given_finds of+ res <- unsafeTcPluginTcM+ $ findMatchingEffectIfSingular extra_wanted extra_given fc given_finds+ case res of -- We found a real given, therefore we are in the context of a function -- with an explicit @Member e r@ constraint. We also know it can -- be unified (although it may generate unsatisfiable constraints).@@ -230,8 +379,10 @@ case splitAppTys r of (_, [_, eff', _]) -> mkWanted fc- (InterpreterUse $ exactlyOneWantedForR wanted_finds r)- eff'+ (InterpreterUse+ (exactlyOneWantedForR wanted_finds r)+ (skolemsForInterpreter eff'))+ eff' _ -> pure Nothing -- We only want to emit a unification wanted once, otherwise a type error can@@ -240,4 +391,5 @@ let (unifications, new_wanteds) = unzipNewWanteds already_emitted $ catMaybes eqs tcPluginIO $ modifyIORef ref $ S.union $ S.fromList unifications - pure $ TcPluginOk (solveBogusError stuff wanted) new_wanteds+ pure $ TcPluginOk [] new_wanteds+
src/Polysemy/Plugin/Fundep/Stuff.hs view
@@ -7,14 +7,34 @@ ) where import Data.Kind (Type)-import FastString (fsLit) import GHC (Name, Class, TyCon, mkModuleName) import GHC.TcPluginM.Extra (lookupModule, lookupName)+#if __GLASGOW_HASKELL__ >= 900+import GHC.Data.FastString (fsLit)+import GHC.Types.Name.Occurrence (mkTcOcc)+import GHC.Tc.Plugin (TcPluginM, tcLookupClass, tcLookupTyCon, unsafeTcPluginTcM)+import GHC.Plugins (getDynFlags)+import GHC.Unit.State (lookupModuleWithSuggestions, LookupResult (..), UnitState)+import GHC.Utils.Outputable (text, (<+>), ($$))+#if __GLASGOW_HASKELL__ >= 902+import GHC.Tc.Plugin (getTopEnv)+import GHC.Utils.Panic (pprPanic)+import GHC.Driver.Env (hsc_units)+#if __GLASGOW_HASKELL__ >= 904+import GHC.Types.PkgQual (PkgQual(NoPkgQual))+#endif+#else+import GHC.Plugins (unitState)+import GHC.Utils.Outputable(pprPanic)+#endif+#else+import FastString (fsLit) import OccName (mkTcOcc) import TcPluginM (TcPluginM, tcLookupClass, tcLookupTyCon, unsafeTcPluginTcM) import GhcPlugins (getDynFlags) import Packages (lookupModuleWithSuggestions, LookupResult (..))-import Outputable (pprPanic, empty, text, (<+>), ($$))+import Outputable (pprPanic, text, (<+>), ($$))+#endif @@ -25,8 +45,6 @@ data PolysemyStuff (l :: LookupState) = PolysemyStuff { findClass :: ThingOf l Class , semTyCon :: ThingOf l TyCon- , ifStuckTyCon :: ThingOf l TyCon- , locateEffectTyCon :: ThingOf l TyCon } @@ -34,19 +52,33 @@ -- | All of the things we need to lookup. polysemyStuffLocations :: PolysemyStuff 'Locations polysemyStuffLocations = PolysemyStuff- { findClass = ("Polysemy.Internal.Union", "Find")- , semTyCon = ("Polysemy.Internal", "Sem")- , ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")- , locateEffectTyCon = ("Polysemy.Internal.Union", "LocateEffect")+ { findClass = ("Polysemy.Internal.Union", "Member")+ , semTyCon = ("Polysemy.Internal", "Sem") } +#if __GLASGOW_HASKELL__ >= 900+------------------------------------------------------------------------------+-- | GHC-version-dependent access of the UnitState+getUnitState :: TcPluginM UnitState+getUnitState = do+#if __GLASGOW_HASKELL__ >= 902+ topState <- getTopEnv+ return (hsc_units topState)+#else+ dflags <- unsafeTcPluginTcM getDynFlags+ return (unitState dflags)+#endif+#endif ------------------------------------------------------------------------------ -- | Lookup all of the 'PolysemyStuff'. polysemyStuff :: TcPluginM (PolysemyStuff 'Things) polysemyStuff = do+#if __GLASGOW_HASKELL__ >= 900+ theUnitState <- getUnitState+#else dflags <- unsafeTcPluginTcM getDynFlags-+#endif let error_msg = pprPanic "polysemy-plugin" $ text "" $$ text "--------------------------------------------------------------------------------"@@ -55,7 +87,19 @@ $$ text "Probable fix: add `polysemy` to your cabal `build-depends`" $$ text "--------------------------------------------------------------------------------" $$ text ""- case lookupModuleWithSuggestions dflags (mkModuleName "Polysemy") Nothing of+ case lookupModuleWithSuggestions+#if __GLASGOW_HASKELL__ >= 900+ theUnitState+#else+ dflags+#endif+ (mkModuleName "Polysemy")+#if __GLASGOW_HASKELL__ >= 904 + NoPkgQual+#else+ Nothing +#endif+ of LookupHidden _ _ -> error_msg LookupNotFound _ -> error_msg #if __GLASGOW_HASKELL__ >= 806@@ -63,11 +107,9 @@ #endif _ -> pure () - let PolysemyStuff a b c d = polysemyStuffLocations+ let PolysemyStuff a b = polysemyStuffLocations PolysemyStuff <$> doLookup a <*> doLookup b- <*> doLookup c- <*> doLookup d ------------------------------------------------------------------------------
src/Polysemy/Plugin/Fundep/Unification.hs view
@@ -1,111 +1,102 @@-{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP #-} module Polysemy.Plugin.Fundep.Unification where import Data.Bool import Data.Function (on)+import Data.Set (Set) import qualified Data.Set as S-#if __GLASGOW_HASKELL__ >= 810++#if __GLASGOW_HASKELL__ >= 900+import GHC.Tc.Types.Constraint+#elif __GLASGOW_HASKELL__ >= 810 import Constraint #else import TcRnTypes #endif +#if __GLASGOW_HASKELL__ >= 900+import GHC.Core.Type+import GHC.Core.Unify+import GHC.Plugins (Outputable, ppr, parens, text, (<+>))+#else import Type+import Unify+import GhcPlugins (Outputable, ppr, parens, text, (<+>))+#endif +#if __GLASGOW_HASKELL__ >= 906+#define SUBST Subst+import GHC.Core.TyCo.Subst (SUBST)+import GHC.Core.TyCo.Compare (eqType, nonDetCmpType)+#else+#define SUBST TCvSubst+#endif + ------------------------------------------------------------------------------ -- | The context in which we're attempting to solve a constraint. data SolveContext- = -- | In the context of a function definition.- FunctionDef+ = -- | In the context of a function definition. The @Set TyVar@ is all of the+ -- skolems that exist in the [G] constraints for this function.+ FunctionDef (Set TyVar) -- | In the context of running an interpreter. The 'Bool' corresponds to -- whether we are only trying to solve a single 'Member' constraint right -- now. If so, we *must* produce a unification wanted.- | InterpreterUse Bool- deriving (Eq, Ord, Show)+ | InterpreterUse Bool (Set TyVar)+ deriving (Eq, Ord) +instance Outputable SolveContext where+ ppr (FunctionDef s) = parens $ text "FunctionDef" <+> ppr s+ ppr (InterpreterUse s ty) = parens $ text "InterpreterUse" <+> ppr s <+> ppr ty + ------------------------------------------------------------------------------ -- | Depending on the context in which we're solving a constraint, we may or -- may not want to force a unification of effects. For example, when defining -- user code whose type is @Member (State Int) r => ...@, if we see @get :: Sem -- r s@, we should unify @s ~ Int@. mustUnify :: SolveContext -> Bool-mustUnify FunctionDef = True-mustUnify (InterpreterUse b) = b+mustUnify (FunctionDef _) = True+mustUnify (InterpreterUse b _) = b --------------------------------------------------------------------------------- | Determine whether or not two effects are unifiable. This is nuanced.------ There are several cases:------ 1. [W] ∀ e1. e1 [G] ∀ e2. e2--- Always fails, because we never want to unify two effects if effect names--- are polymorphic.------ 2. [W] State s [G] State Int--- Always succeeds. It's safe to take our given as a fundep annotation.------ 3. [W] State Int [G] State s--- (when the [G] is a given that comes from a type signature)------ This should fail, because it means we wrote the type signature @Member--- (State s) r => ...@, but are trying to use @s@ as an @Int@. Clearly--- bogus!------ 4. [W] State Int [G] State s--- (when the [G] was generated by running an interpreter)------ Sometimes OK, but only if the [G] is the only thing we're trying to solve--- right now. Consider the case:------ runState 5 $ pure @(Sem (State Int ': r)) ()------ Here we have [G] forall a. Num a => State a and [W] State Int. Clearly--- the typechecking should flow "backwards" here, out of the row and into--- the type of 'runState'.+-- | Determine whether or not two effects are unifiable. ----- What happens if there are multiple [G]s in scope for the same @r@? Then--- we'd emit multiple unification constraints for the same effect but with--- different polymorphic variables, which would unify a bunch of effects--- that shouldn't be!-canUnifyRecursive+-- All free variables in [W] constraints are considered skolems, and thus are+-- not allowed to unify with anything but themselves. This properly handles all+-- cases in which we are unifying ambiguous [W] constraints (which are true+-- type variables) against [G] constraints.+unify :: SolveContext -> Type -- ^ wanted -> Type -- ^ given- -> Bool-canUnifyRecursive solve_ctx = go True+ -> Maybe SUBST+unify solve_ctx = tryUnifyUnivarsButNotSkolems skolems where- -- It's only OK to solve a polymorphic "given" if we're in the context of- -- an interpreter, because it's not really a given!- poly_given_ok :: Bool- poly_given_ok =+ skolems :: Set TyVar+ skolems = case solve_ctx of- InterpreterUse _ -> True- FunctionDef -> False-- -- On the first go around, we don't want to unify effects with tyvars, but- -- we _do_ want to unify their arguments, thus 'is_first'.- go :: Bool -> Type -> Type -> Bool- go is_first wanted given =- let (w, ws) = splitAppTys wanted- (g, gs) = splitAppTys given- in (&& bool (canUnify poly_given_ok) eqType is_first w g)- . flip all (zip ws gs)- $ \(wt, gt) -> canUnify poly_given_ok wt gt || go False wt gt-+ InterpreterUse _ s -> s+ FunctionDef s -> s ---------------------------------------------------------------------------------- | A non-recursive version of 'canUnifyRecursive'.-canUnify :: Bool -> Type -> Type -> Bool-canUnify poly_given_ok wt gt =- or [ isTyVarTy wt- , isTyVarTy gt && poly_given_ok- , eqType wt gt- ]+#if __GLASGOW_HASKELL__ >= 902+#define BINDME (const BindMe)+#define APART (const Apart)+#else+#define BINDME BindMe+#define APART Skolem+#endif +tryUnifyUnivarsButNotSkolems :: Set TyVar -> Type -> Type -> Maybe SUBST+tryUnifyUnivarsButNotSkolems skolems goal inst =+ case tcUnifyTysFG+ (bool BINDME APART . flip S.member skolems)+ [inst]+ [goal] of+ Unifiable subst -> pure subst+ _ -> Nothing ------------------------------------------------------------------------------ -- | A wrapper for two types that we want to say have been unified.
+ test/AmbiguousSpec.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module AmbiguousSpec where++import Control.Monad.IO.Class (liftIO)+import Data.Functor.Identity+import Data.Monoid+import Polysemy+import Polysemy.Embed (runEmbedded)+import Polysemy.Error (Error, runError)+import Polysemy.State+import Polysemy.Tagged (Tagged, tag)+import Test.Hspec+import Test.ShouldNotTypecheck++class MPTC a b where+ mptc :: a -> b++instance MPTC Bool Int where+ mptc _ = 1000+++uniquelyInt :: Members '[State Int , State String] r => Sem r ()+uniquelyInt = put 10++uniquelyA :: forall a b r. (Num a, Members '[State a, State b] r) => Sem r ()+uniquelyA = put 10++uniquelyString :: Members '[State Int , State String] r => Sem r ()+uniquelyString = put mempty++uniquelyB :: (MPTC Bool b, Members '[State String, State b] r) => Sem r ()+uniquelyB = put $ mptc False++uniquelyIO :: Members '[Embed IO, Embed Identity] r => Sem r ()+uniquelyIO = embed $ liftIO $ pure ()++uniquelyState' :: ∀ r . Members [Error (), State ()] r => Sem r ()+uniquelyState' = pure ()++uniquelyState :: ∀ r . Member (Tagged () (State ())) r => Sem r (Either () ())+uniquelyState = runError (tag @() uniquelyState')+-- uniquelyState = runError (tag @() (uniquelyState' @(State () : Error () : r)))++spec :: Spec+spec = describe "example" $ do+ it "should run uniquelyInt" $ do+ let z = run . runState 0 . runState "hello" $ uniquelyInt+ z `shouldBe` (10, ("hello", ()))++ it "should run uniquelyA" $ do+ let z = run . runState 0 . runState "hello" $ uniquelyA @Int @String+ z `shouldBe` (10, ("hello", ()))++ it "should run uniquelyB" $ do+ let z = run . runState 0 . runState "hello" $ uniquelyB @Int+ z `shouldBe` (1000, ("hello", ()))++ it "should run uniquelyString" $ do+ let z = run . runState 0 . runState "hello" $ uniquelyString+ z `shouldBe` (0, ("", ()))++ it "should run uniquelyIO" $ do+ z <- runM . runEmbedded @Identity (pure . runIdentity) $ uniquelyIO+ z `shouldBe` ()+
− test/BadSpec.hs
@@ -1,38 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}--{-# OPTIONS_GHC -fdefer-type-errors -fno-warn-deferred-type-errors #-}--module BadSpec where--import Polysemy-import Polysemy.State-import Test.Hspec-import Test.ShouldNotTypecheck--data KVStore k v m a where- GetKV :: k -> KVStore k v m (Maybe v)--makeSem ''KVStore--positivePos :: Member (KVStore k v) r => Sem r (Maybe v)-positivePos = do- getKV "hello"--negativePos :: Member (KVStore String v) r => Sem r (Maybe Bool)-negativePos = do- getKV "hello"--badState :: Member (State a) r => Sem r ()-badState = put ()---spec :: Spec-spec = do- describe "incorrectly polymorphic constraint" $ do- it "should not typecheck in positive position" $ do- shouldNotTypecheck positivePos- it "should not typecheck in negative position" $ do- shouldNotTypecheck negativePos- it "should not typecheck badly polymorphic State" $ do- shouldNotTypecheck badState-
test/ExampleSpec.hs view
@@ -1,5 +1,4 @@ {-# LANGUAGE TemplateHaskell #-}-{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-} module ExampleSpec where
+ test/InsertSpec.hs view
@@ -0,0 +1,22 @@+module InsertSpec where++import Polysemy.State (State)+import Polysemy.Reader (Reader)+import Polysemy.Internal (insertAt)+import Polysemy+import Test.Hspec++insertAtWithIndex :: Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e1 : e2 : Reader i : e3 : e4 : r) a+insertAtWithIndex = insertAt @2++insertAtAndRaiseUnder :: Sem (e1 : r) a -> Sem (e1 : e2 : State s : e3 : Reader i : e4 : r) a+insertAtAndRaiseUnder = raise2Under . insertAt @2 . raiseUnder++insertAtEmpty :: Sem (e1 : e2 : r) a -> Sem (e1 : e2 : r) a+insertAtEmpty = insertAt @2++spec :: Spec+spec = parallel $ do+ describe "insert" $ do+ it "insert" $ do+ 1 `shouldBe` 1
test/TypeErrors.hs view
@@ -1,4 +1,5 @@ {-# OPTIONS_GHC -fno-warn-missing-signatures #-}+{-# LANGUAGE CPP #-} module TypeErrors where @@ -9,6 +10,7 @@ -- >>> :set -fplugin=Polysemy.Plugin -- >>> :m +Polysemy -- >>> :m +Polysemy.State+-- >>> :m +Polysemy.Reader -- >>> :m +Data.Maybe @@ -21,8 +23,59 @@ -- ... -- ... Couldn't match expected type ...Sem r Bool... with actual type ...Bool... -- ...--- ... Couldn't match expected type ...Maybe a0...--- ... with actual type ...Sem r0 s0...+-- ... Couldn't match expected type...Maybe a0...+-- ... with actual type...Sem r0 s0... -- ... missingFmap = () +--------------------------------------------------------------------------------+-- |+-- >>> :{+-- insertSome :: ∀ e1 e2 s r a . Sem (e1 ': e2 ': r) a -> Sem (e1 ': e2 ': State s ': r) a+-- insertSome = insertAt+-- :}+-- ...+-- ... insertAt: You must provide the index ...+-- ...+insertAtUnprovidedIndex = ()++#if __GLASGOW_HASKELL__ < 902++--------------------------------------------------------------------------------+-- |+-- >>> :{+-- insertSome :: Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e1 : e2 : Reader i : e3 : e4 : r) a+-- insertSome = insertAt @1+-- :}+-- ...+-- ...insertAt: Failed to insert effects at index 1+-- ...+-- ... before ...+-- ...'[e1]+-- ... after ...+-- ...e2 : e3 : e4 : r+-- ...Actual ...+-- ...e1 : e2 : Reader i : e3 : e4 : r+-- ...+insertAtWrongIndex = ()++--------------------------------------------------------------------------------+-- |+-- Note: The /Actual/ row doesn't match the return type because of the 'raiseUnder'.+-- >>> :{+-- insertSome :: Sem (e1 : r) a -> Sem (e1 : e2 : State s : e3 : Reader i : e4 : r) a+-- insertSome = raiseUnder . insertAt @2 . raise2Under+-- :}+-- ...+-- ...insertAt: Failed to insert effects at index 2+-- ...+-- ... before ...+-- ...'[e1, State s]+-- ... after ...+-- ...e30 : r0+-- ...Actual ...+-- ...e1 : State s : e3 : Reader i : e4 : r+-- ...+insertAtAndRaiseWrongIndex = ()++#endif