diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -2,6 +2,11 @@ ## Unreleased +## 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 diff --git a/polysemy-plugin.cabal b/polysemy-plugin.cabal --- a/polysemy-plugin.cabal +++ b/polysemy-plugin.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: polysemy-plugin -version: 0.4.0.0 +version: 0.4.1.0 synopsis: Disambiguate obvious uses of effects. description: Please see the README on GitHub at category: Polysemy @@ -77,6 +77,7 @@ type: exitcode-stdio-1.0 main-is: Main.hs other-modules: + AmbiguousSpec BadSpec DoctestSpec ExampleSpec diff --git a/src/Polysemy/Plugin/Fundep.hs b/src/Polysemy/Plugin/Fundep.hs --- a/src/Polysemy/Plugin/Fundep.hs +++ b/src/Polysemy/Plugin/Fundep.hs @@ -1,6 +1,6 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE CPP #-} ------------------------------------------------------------------------------ -- The MIT License (MIT) @@ -35,31 +35,53 @@ 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 + #if __GLASGOW_HASKELL__ >= 900 +import GHC.Builtin.Types.Prim (alphaTys) +import GHC.Plugins (idType, tyConClass_maybe) 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) 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 -import TcEvidence -import TcPluginM (TcPluginM, tcPluginIO) -import TcRnTypes #if __GLASGOW_HASKELL__ >= 810 import Constraint #endif + +import Class (classTyCon) +import GhcPlugins (idType, tyConClass_maybe) +import Inst (tcGetInstEnvs) +import InstEnv (lookupInstEnv, is_dfun) +import MonadUtils (allM, anyM) +import TcEvidence +import TcPluginM (tcPluginIO) +import TcRnTypes +import TcType (tcSplitPhiTy, tcSplitTyConApp) import TcSMonad hiding (tcLookupClass) import Type +import TysPrim (alphaTys) #endif @@ -75,6 +97,17 @@ ------------------------------------------------------------------------------ +-- | Like 'PredType', but has an 'Ord' instance. +newtype PredType' = PredType' { getPredType :: PredType } + +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 @@ -100,22 +133,63 @@ ------------------------------------------------------------------------------ --- | 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 + CDictCan{cc_class = cls, cc_tyargs = as} <- cts + 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' -> TCvSubst -> PredType -> TcM Bool +checkExtraEvidence givens subst = flip evalStateT givens . getInstance . substTy subst + + +------------------------------------------------------------------------------ -- | Given an effect, compute its effect name. getEffName :: Type -> Type getEffName t = fst $ splitAppTys t @@ -138,6 +212,7 @@ where wanted = fcEffect fc + ------------------------------------------------------------------------------ -- | Generate a wanted unification for the effect described by the -- 'FindConstraint' and the given effect --- if they can be unified in this @@ -148,7 +223,7 @@ -> Type -- ^ The given effect. -> TcPluginM (Maybe (Unification, Ct)) mkWanted fc solve_ctx given = - whenA (not (mustUnify solve_ctx) || canUnifyRecursive solve_ctx wanted given) $ + whenA (not (mustUnify solve_ctx) || isJust (unify solve_ctx wanted given)) $ mkWantedForce fc given where wanted = fcEffect fc @@ -188,7 +263,17 @@ (idx, [_, _, r]) <- splitTyConApp_list expr guard $ idx == locateEffectTyCon stuff guard $ elem @[] (OrdType r) $ coerce bogus - pure (error "bogus proof for stuck type family", ct) + pure (error $ unlines + [ "Bogus proof for stuck type family." + , "" + , "This means there's a type error in your program, but the fact that" + , "you're seeing this message is a bug in `polysemy-plugin`." + , "" + , "Please file a bug at https://github.com/polysemy-research/polysemy" + , "with a minimal reproduction for how you managed to get this error." + ] + , ct + ) ------------------------------------------------------------------------------ @@ -211,6 +296,37 @@ $ 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 -> do + let (con, apps) = tcSplitTyConApp predty + Just cls = tyConClass_maybe con + 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 @@ -223,10 +339,14 @@ solveFundep (ref, stuff) given _ wanted = do 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). @@ -250,3 +370,4 @@ tcPluginIO $ modifyIORef ref $ S.union $ S.fromList unifications pure $ TcPluginOk (solveBogusError stuff wanted) new_wanteds + diff --git a/src/Polysemy/Plugin/Fundep/Unification.hs b/src/Polysemy/Plugin/Fundep/Unification.hs --- a/src/Polysemy/Plugin/Fundep/Unification.hs +++ b/src/Polysemy/Plugin/Fundep/Unification.hs @@ -1,9 +1,10 @@ -{-# 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__ >= 900 import GHC.Tc.Types.Constraint @@ -15,22 +16,24 @@ #if __GLASGOW_HASKELL__ >= 900 import GHC.Core.Type +import GHC.Core.Unify #else import Type +import Unify #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) + deriving (Eq, Ord) ------------------------------------------------------------------------------ @@ -39,79 +42,39 @@ -- 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 (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 TCvSubst +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 _ -> mempty + 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 - ] +tryUnifyUnivarsButNotSkolems :: Set TyVar -> Type -> Type -> Maybe TCvSubst +tryUnifyUnivarsButNotSkolems skolems goal inst = + case tcUnifyTysFG + (bool BindMe Skolem . flip S.member skolems) + [inst] + [goal] of + Unifiable subst -> pure subst + _ -> Nothing ------------------------------------------------------------------------------ diff --git a/test/AmbiguousSpec.hs b/test/AmbiguousSpec.hs new file mode 100644 --- /dev/null +++ b/test/AmbiguousSpec.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +{-# OPTIONS_GHC -fdefer-type-errors #-} +{-# OPTIONS_GHC -fno-warn-deferred-type-errors #-} +{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-} + +module AmbiguousSpec where + +import Control.Monad.IO.Class (liftIO) +import Data.Functor.Identity +import Data.Monoid +import Polysemy +import Polysemy.Embed (runEmbedded) +import Polysemy.State +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 () + +ambiguous1 :: Members '[State (Sum Int), State String] r => Sem r () +ambiguous1 = put mempty + +ambiguous2 :: (Num String, Members '[State Int, State String] r) => Sem r () +ambiguous2 = put 10 + + +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` () + + it "should not typecheck ambiguous1" $ do + shouldNotTypecheck ambiguous1 + + it "should not typecheck ambiguous2" $ do + shouldNotTypecheck ambiguous2 + diff --git a/test/ExampleSpec.hs b/test/ExampleSpec.hs --- a/test/ExampleSpec.hs +++ b/test/ExampleSpec.hs @@ -1,5 +1,4 @@ {-# LANGUAGE TemplateHaskell #-} -{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-} module ExampleSpec where