diff --git a/polysemy-plugin/polysemy-plugin.cabal b/polysemy-plugin/polysemy-plugin.cabal index b13525d..7ff9ca8 100644 --- a/polysemy-plugin/polysemy-plugin.cabal +++ b/polysemy-plugin/polysemy-plugin.cabal @@ -4,7 +4,7 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: 6aabb881334585f56358446f23bcdff48fa22af05afc52c83a102db79c9ccd06 +-- hash: 01634ce3c7ac101e60c1a02f8ccad7ec499c02a04b66e5d9dd5993f314318097 name: polysemy-plugin version: 0.2.3.0 @@ -57,11 +57,9 @@ test-suite polysemy-plugin-test BadSpec DoctestSpec ExampleSpec - HistorySpec LegitimateTypeErrorSpec MultipleVarsSpec PluginSpec - SpecificitySpec TypeErrors VDQSpec Paths_polysemy_plugin diff --git a/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs b/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs index 2f77e5a..a7403b7 100644 --- a/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs +++ b/polysemy-plugin/src/Polysemy/Plugin/Fundep.hs @@ -1,16 +1,6 @@ -{-# LANGUAGE CPP #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ViewPatterns #-} -#if MIN_VERSION_ghc(8,5,0) -#else -#define EvExpr -#define Coercion EvCoercion --- #if __GLASGOW_HASKELL__ < 711 --- $ TcCoercion --- #endif -#endif - ------------------------------------------------------------------------------ -- The MIT License (MIT) -- @@ -43,31 +33,29 @@ module Polysemy.Plugin.Fundep (fundepPlugin) where -import Control.Applicative (empty) -import Control.Arrow ((&&&)) import Control.Monad -import CoreSyn import Data.Bifunctor import Data.Coerce -import Data.List (sortBy, find) +import Data.IORef import qualified Data.Map as M import Data.Maybe -import Data.Ord (Down (..), comparing) -import GHC.TcPluginM.Extra (evByFiat) -import GhcPlugins hiding (empty) -import Outputable hiding (empty) +import qualified Data.Set as S import Polysemy.Plugin.Fundep.Stuff import Polysemy.Plugin.Fundep.Unification import Polysemy.Plugin.Fundep.Utils import TcEvidence -import TcPluginM (TcPluginM, newGiven) +import TcPluginM (TcPluginM, tcPluginIO) import TcRnTypes +import TcSMonad hiding (tcLookupClass) +import Type fundepPlugin :: TcPlugin fundepPlugin = TcPlugin - { tcPluginInit = polysemyStuff + { tcPluginInit = + (,) <$> tcPluginIO (newIORef S.empty) + <*> polysemyStuff , tcPluginSolve = solveFundep , tcPluginStop = const $ pure () } @@ -114,15 +102,6 @@ findMatchingEffectIfSingular (FindConstraint _ eff_name wanted r) ts = pure eff' -oneMostSpecific :: [Type] -> Maybe Type -oneMostSpecific tys = - let sorted = sortBy (comparing $ Down . fst) $ fmap (specificityMetric &&& id) tys - in case pprTrace "sorted" (ppr sorted) sorted of - ((p1, t1) : (p2, _) : _) | p1 /= p2 -> Just t1 - [(_, t1)] -> Just t1 - _ -> Nothing - - ------------------------------------------------------------------------------ -- | Given an effect, compute its effect name. getEffName :: Type -> Type @@ -132,16 +111,17 @@ getEffName t = fst $ splitAppTys t ------------------------------------------------------------------------------ -- | Generate a wanted unification for the effect described by the -- 'FindConstraint' and the given effect. -mkGivenForce +mkWantedForce :: FindConstraint -> Type - -> TcPluginM Unification -mkGivenForce fc given = do - ev <- newGiven (fcLoc fc) (mkPrimEqPred wanted given) - . Coercion - $ mkTcNomReflCo given - pure . Unification (OrdType wanted) (OrdType given) - $ CNonCanonical ev + -> TcPluginM (Unification, Ct) +mkWantedForce fc given = do + (ev, _) <- unsafeTcPluginTcM + . runTcSDeriveds + $ newWantedEq (fcLoc fc) Nominal wanted given + pure ( Unification (OrdType wanted) (OrdType given) + , CNonCanonical ev + ) where wanted = fcEffect fc @@ -149,14 +129,14 @@ mkGivenForce fc given = do -- | Generate a wanted unification for the effect described by the -- 'FindConstraint' and the given effect --- if they can be unified in this -- context. -mkGiven +mkWanted :: FindConstraint -> SolveContext -> Type -- ^ The given effect. - -> TcPluginM (Maybe Unification) -mkGiven fc solve_ctx given = + -> TcPluginM (Maybe (Unification, Ct)) +mkWanted fc solve_ctx given = whenA (not (mustUnify solve_ctx) || canUnifyRecursive solve_ctx wanted given) $ - mkGivenForce fc given + mkWantedForce fc given where wanted = fcEffect fc @@ -219,13 +199,15 @@ exactlyOneWantedForR wanteds solveFundep - :: PolysemyStuff 'Things + :: ( IORef (S.Set Unification) + , PolysemyStuff 'Things + ) -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult solveFundep _ _ _ [] = pure $ TcPluginOk [] [] -solveFundep stuff given _ wanted = do +solveFundep (ref, stuff) given _ wanted = do let wanted_finds = getFindConstraints stuff wanted given_finds = getFindConstraints stuff given @@ -235,106 +217,24 @@ solveFundep stuff given _ wanted = do -- 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). - Just eff' -> Just <$> mkGivenForce fc eff' + Just eff' -> Just <$> mkWantedForce fc eff' -- Otherwise, check to see if @r ~ (e ': r')@. If so, pretend we're -- trying to solve a given @Member e r@. But this can only happen in the -- context of an interpreter! Nothing -> case splitAppTys r of - (_, [_, eff', _]) -> do - mkGiven fc + (_, [_, eff', _]) -> + mkWanted fc (InterpreterUse $ exactlyOneWantedForR wanted_finds r) eff' _ -> pure Nothing - let unifications = getGoodUnifications $ catMaybes eqs - new_givens = fmap _unifyCt unifications + -- We only want to emit a unification wanted once, otherwise a type error can + -- force the type checker to loop forever. + already_emitted <- tcPluginIO $ readIORef ref + let (unifications, new_wanteds) = unzipNewWanteds already_emitted $ catMaybes eqs + tcPluginIO $ modifyIORef ref $ S.union $ S.fromList unifications - solved_founds <- getFounds stuff wanted - solved_indexofs <- getIndexOfFounds stuff wanted - - pure $ TcPluginOk (solveBogusError stuff wanted) $ - mconcat - [ new_givens - , solved_founds - , solved_indexofs - ] - - ------------------------------------------------------------------------------- --- | Unroll a row into all the types that are consed together in it. -unrollR :: Type -> [Type] -unrollR r = - case splitAppTys r of - (_, [_, eff', r']) -> eff' : unrollR r' - _ -> [r] - - ------------------------------------------------------------------------------- --- | Solves stuck type families of the form @IndexOf row (Found row e) ~ e@. --- This can happen when we're in interpreter mode, searching for effects in the --- row that have type variables that should /stay/ type variables. -getIndexOfFounds :: PolysemyStuff 'Things -> [Ct] -> TcPluginM [Ct] -getIndexOfFounds stuff cts = sequenceA $ do - ct@(CNonCanonical ev) <- cts - let ctpred = ctev_pred ev - Just (_, t1, e) <- pure $ getEqPredTys_maybe ctpred - Just (indexOfTc, [_, r, n]) <- pure $ splitTyConApp_maybe t1 - guard $ indexOfTc == indexOfTyCon stuff - Just (foundTc, [_, r', e']) <- pure $ splitTyConApp_maybe n - guard $ foundTc == foundTyCon stuff - guard $ eqType r r' - guard $ eqType e e' - - let EvExpr evidence = evByFiat "polysemy-plugin" t1 e - pure $ CNonCanonical <$> newGiven (ctLoc ct) (mkPrimEqPred t1 e) evidence - - ------------------------------------------------------------------------------- --- | Solves stuck type families of the form @Found row e ~ nat@, by determining --- whether or not @e@ is actually at @nat@ in @row@. GHC should actually do --- this on its own, but doesn't due to --- https://gitlab.haskell.org/ghc/ghc/issues/17311 -getFounds :: PolysemyStuff 'Things -> [Ct] -> TcPluginM [Ct] -getFounds stuff cts = sequenceA $ do - ct@(CNonCanonical ev) <- cts - let evpred = ctev_pred ev - Just (_, t1, nat) <- pure $ getEqPredTys_maybe evpred - Just (foundTc, [_, r, e]) <- pure $ splitTyConApp_maybe t1 - guard $ foundTc == foundTyCon stuff - - let EvExpr evidence = evByFiat "polysemy-plugin" t1 nat - let unrolled = unrollR r - proof = CNonCanonical <$> newGiven (ctLoc ct) (mkPrimEqPred t1 nat) evidence - - case fmap fst $ find (eqType e . snd) $ zip [0..] unrolled of - Just index -> do - guard $ mkNat stuff index `eqType` nat - pure proof - Nothing -> do - let n = stripS stuff nat - case drop n unrolled of - [t] | isTyVarTy t -> pure proof - _ -> empty - - ------------------------------------------------------------------------------- --- | Turn an 'Int' into a 'Polysemy.Internal.Union.Nat'. -mkNat :: PolysemyStuff 'Things -> Int -> Type -mkNat stuff = go - where - go 0 = mkTyConTy $ promotedZDataCon stuff - go n = mkTyConApp (promotedSDataCon stuff) [go $ n - 1] - - ------------------------------------------------------------------------------- --- | Counts the number of 'Polysemy.Internal.Union.S' constructors in a type. -stripS :: PolysemyStuff 'Things -> Type -> Int -stripS stuff = go - where - go (splitTyConApp_maybe -> Just (tc, [a])) - | tc == promotedSDataCon stuff - = 1 + go a - go _ = 0 + pure $ TcPluginOk (solveBogusError stuff wanted) new_wanteds diff --git a/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs b/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs index 2cb3c13..02c84b8 100644 --- a/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs +++ b/polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} - module Polysemy.Plugin.Fundep.Stuff ( PolysemyStuff (..) , LookupState (..) @@ -8,11 +6,10 @@ module Polysemy.Plugin.Fundep.Stuff import Data.Kind (Type) import FastString (fsLit) -import GHC (Name, Class, TyCon, DataCon, mkModuleName) +import GHC (Name, Class, TyCon, mkModuleName) import GHC.TcPluginM.Extra (lookupModule, lookupName) -import OccName (OccName, mkTcOcc, mkDataOcc) -import TcPluginM (TcPluginM, tcLookupClass, tcLookupTyCon, tcLookupDataCon) -import DataCon (promoteDataCon) +import OccName (mkTcOcc) +import TcPluginM (TcPluginM, tcLookupClass, tcLookupTyCon) @@ -21,13 +18,10 @@ import DataCon (promoteDataCon) -- When @l ~ 'Locations@, each of these is just a pair of strings. When @l -- ~ 'Things@, it's actually references to the stuff. data PolysemyStuff (l :: LookupState) = PolysemyStuff - { findClass :: ThingOf l Class - , foundTyCon :: ThingOf l TyCon - , semTyCon :: ThingOf l TyCon - , ifStuckTyCon :: ThingOf l TyCon - , indexOfTyCon :: ThingOf l TyCon - , promotedSDataCon :: ThingOf l TyCon - , promotedZDataCon :: ThingOf l TyCon + { findClass :: ThingOf l Class + , semTyCon :: ThingOf l TyCon + , ifStuckTyCon :: ThingOf l TyCon + , indexOfTyCon :: ThingOf l TyCon } @@ -35,13 +29,10 @@ data PolysemyStuff (l :: LookupState) = PolysemyStuff -- | All of the things we need to lookup. polysemyStuffLocations :: PolysemyStuff 'Locations polysemyStuffLocations = PolysemyStuff - { findClass = ("Polysemy.Internal.Union", "Find") - , foundTyCon = ("Polysemy.Internal.Union", "Found") - , semTyCon = ("Polysemy.Internal", "Sem") - , ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck") - , indexOfTyCon = ("Polysemy.Internal.Union", "IndexOf") - , promotedSDataCon = ("Polysemy.Internal.Union", "S") - , promotedZDataCon = ("Polysemy.Internal.Union", "Z") + { findClass = ("Polysemy.Internal.Union", "Find") + , semTyCon = ("Polysemy.Internal", "Sem") + , ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck") + , indexOfTyCon = ("Polysemy.Internal.Union", "IndexOf") } @@ -49,14 +40,11 @@ polysemyStuffLocations = PolysemyStuff -- | Lookup all of the 'PolysemyStuff'. polysemyStuff :: TcPluginM (PolysemyStuff 'Things) polysemyStuff = - let PolysemyStuff a b c d e f g = polysemyStuffLocations + let PolysemyStuff a b c d = polysemyStuffLocations in PolysemyStuff <$> doLookup a <*> doLookup b <*> doLookup c <*> doLookup d - <*> doLookup e - <*> (fmap promoteDataCon $ doLookup f) - <*> (fmap promoteDataCon $ doLookup g) ------------------------------------------------------------------------------ @@ -77,26 +65,19 @@ type family ThingOf (l :: LookupState) (a :: Type) :: Type where -- | Things that can be found in a 'TcPluginM' environment. class CanLookup a where lookupStrategy :: Name -> TcPluginM a - mkLookupOcc :: String -> OccName instance CanLookup Class where lookupStrategy = tcLookupClass - mkLookupOcc = mkTcOcc instance CanLookup TyCon where lookupStrategy = tcLookupTyCon - mkLookupOcc = mkTcOcc - -instance CanLookup DataCon where - lookupStrategy = tcLookupDataCon - mkLookupOcc = mkDataOcc ------------------------------------------------------------------------------ -- | Transform a @'ThingOf' 'Locations@ into a @'ThingOf' 'Things@. -doLookup :: forall a. CanLookup a => ThingOf 'Locations a -> TcPluginM (ThingOf 'Things a) +doLookup :: CanLookup a => ThingOf 'Locations a -> TcPluginM (ThingOf 'Things a) doLookup (mdname, name) = do md <- lookupModule (mkModuleName mdname) $ fsLit "polysemy" - nm <- lookupName md $ mkLookupOcc @a name + nm <- lookupName md $ mkTcOcc name lookupStrategy nm diff --git a/polysemy-plugin/src/Polysemy/Plugin/Fundep/Unification.hs b/polysemy-plugin/src/Polysemy/Plugin/Fundep/Unification.hs index 0d50df2..5012ae1 100644 --- a/polysemy-plugin/src/Polysemy/Plugin/Fundep/Unification.hs +++ b/polysemy-plugin/src/Polysemy/Plugin/Fundep/Unification.hs @@ -1,14 +1,8 @@ module Polysemy.Plugin.Fundep.Unification where -import Control.Arrow ((&&&)) import Data.Bool import Data.Function (on) -import Data.Generics -import Data.List -import Data.Ord import qualified Data.Set as S -import DataCon (DataCon) -import Outputable hiding ((<>)) import TcRnTypes import Type @@ -111,37 +105,8 @@ canUnify poly_given_ok wt gt = data Unification = Unification { _unifyLHS :: OrdType , _unifyRHS :: OrdType - , _unifyCt :: Ct } - -instance Eq Unification where - Unification a b _ == Unification a' b' _ = a == a' && b == b' - -instance Ord Unification where - Unification a b _ `compare` Unification a' b' _ = compare a a' <> compare b b' - -instance Outputable Unification where - ppr (Unification (OrdType a) (OrdType b) _) = ppr a <+> text " --> " <+> ppr b - - -getGoodUnifications :: [Unification] -> [Unification] -getGoodUnifications = fmap mostSpecificUnification . groupUnifications - - -groupUnifications :: [Unification] -> [[Unification]] -groupUnifications = fmap (fmap snd) - . groupBy ((==) `on` fst) - . sortBy (comparing fst) - . fmap (_unifyRHS &&& id) - - -specificityMetric :: Type -> Int -specificityMetric = everything (+) $ mkQ 0 $ \case - (dc :: Type) -> 1 - -mostSpecificUnification :: [Unification] -> Unification -mostSpecificUnification - = head . sortBy (comparing $ Down . specificityMetric . getOrdType . _unifyLHS) + deriving (Eq, Ord) ------------------------------------------------------------------------------ @@ -158,3 +123,14 @@ instance Eq OrdType where instance Ord OrdType where compare = nonDetCmpType `on` getOrdType + +------------------------------------------------------------------------------ +-- | Filter out the unifications we've already emitted, and then give back the +-- things we should put into the @S.Set Unification@, and the new constraints +-- we should emit. +unzipNewWanteds + :: S.Set Unification + -> [(Unification, Ct)] + -> ([Unification], [Ct]) +unzipNewWanteds old = unzip . filter (not . flip S.member old . fst) + diff --git a/polysemy-plugin/test/BadSpec.hs b/polysemy-plugin/test/BadSpec.hs index 127a5f6..9336164 100644 --- a/polysemy-plugin/test/BadSpec.hs +++ b/polysemy-plugin/test/BadSpec.hs @@ -1,5 +1,4 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -fdefer-type-errors -fno-warn-deferred-type-errors #-} @@ -15,10 +14,6 @@ data KVStore k v m a where makeSem ''KVStore -runKVStore :: [(k, v)] -> InterpreterFor (KVStore k v) r -runKVStore = interpret $ \case - GetKV _ -> pure Nothing - positivePos :: Member (KVStore k v) r => Sem r (Maybe v) positivePos = do getKV "hello" @@ -35,12 +30,9 @@ spec :: Spec spec = do describe "incorrectly polymorphic constraint" $ do it "should not typecheck in positive position" $ do - shouldNotTypecheck (run . runKVStore [("hello", True)] - $ positivePos @String @Bool @'[KVStore String Bool]) + shouldNotTypecheck positivePos it "should not typecheck in negative position" $ do - shouldNotTypecheck (run . runKVStore [("hello", True)] - $ negativePos @Bool @'[KVStore String Bool]) + shouldNotTypecheck negativePos it "should not typecheck badly polymorphic State" $ do - shouldNotTypecheck (run . runState () - $ badState @() @'[State ()]) + shouldNotTypecheck badState diff --git a/polysemy-plugin/test/HistorySpec.hs b/polysemy-plugin/test/HistorySpec.hs deleted file mode 100644 index f40a01a..0000000 --- a/polysemy-plugin/test/HistorySpec.hs +++ /dev/null @@ -1,84 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeOperators #-} - -{-# OPTIONS_GHC -fplugin=Polysemy.Plugin -fconstraint-solver-iterations=10 #-} - -module HistorySpec where - -import Polysemy -import Polysemy.State -import Test.Hspec - -data History s m a where - Undo :: History s m () - Redo :: History s m () - PutAndForget :: s -> History s m () - -makeSem ''History - - -spec :: Spec -spec = describe "HistorySpec" $ it "should compile" $ do - let z = run . runState (0 :: Int) . runHistory $ do - modify (+ 5) - undo - x <- get - redo - y <- get - undo - put 1 - redo - pure (x, y) - z `shouldBe` (1 :: Int, (0 :: Int, 5 :: Int)) - - -data Zipper a = Zipper [a] a [a] - -focusZ :: Zipper a -> a -focusZ (Zipper _ a _) = a - -modifyZ :: (a -> a) -> Zipper a -> Zipper a -modifyZ f (Zipper past a _) = Zipper (a : past) (f a) [] - -goBack :: Zipper a -> Zipper a -goBack z@(Zipper [] _ _) = z -goBack (Zipper (p : ps) a fs) = Zipper ps p (a : fs) - -goForward :: Zipper a -> Zipper a -goForward z@(Zipper _ _ []) = z -goForward (Zipper ps a (f : fs)) = Zipper (a : ps) f fs - -runHistory - :: forall s r a - . Member (State s) r - => Sem (History s ': r) a - -> Sem r a -runHistory m = do - s <- get - evalState (Zipper [] s []) - . interpret (\case - Undo -> do - s' <- modify goBack >> gets focusZ - put s' - Redo -> do - s' <- modify goForward >> gets focusZ - put s' - PutAndForget s' -> - put s') - . intercept @(State s) (\case - Get -> get - Put s' -> do - modify $ modifyZ $ const s' - put s') - . raiseUnder @(State (Zipper s)) - $ m - diff --git a/polysemy-plugin/test/SpecificitySpec.hs b/polysemy-plugin/test/SpecificitySpec.hs deleted file mode 100644 index f82cdd4..0000000 --- a/polysemy-plugin/test/SpecificitySpec.hs +++ /dev/null @@ -1,31 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeOperators #-} - -{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-} - -module SpecificitySpec where - -import Polysemy -import Polysemy.State -import Polysemy.Internal -import Polysemy.Internal.Union -import Test.Hspec -import Data.Functor.Identity - - -spec :: Spec -spec = describe "HistorySpec" $ it "should compile" $ True `shouldBe` True - -foo :: Members [State s, State (Identity s)] r => Sem r () -foo = do - s <- get - put $ Identity s