polysemy-plugin 0.4.0.0 → 0.4.1.0

raw patch · 6 files changed

+251/−87 lines, 6 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−0
• polysemy-plugin.cabal +2/−1
• src/Polysemy/Plugin/Fundep.hs +140/−19
• src/Polysemy/Plugin/Fundep/Unification.hs +29/−66
• test/AmbiguousSpec.hs +75/−0
• test/ExampleSpec.hs +0/−1

@@ -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

@@ -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 <https://github.com/polysemy-research/polysemy/tree/master/polysemy-plugin#readme> category:       Polysemy@@ -77,6 +77,7 @@   type: exitcode-stdio-1.0   main-is: Main.hs   other-modules:+      AmbiguousSpec       BadSpec       DoctestSpec       ExampleSpec

@@ -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+

@@ -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   ------------------------------------------------------------------------------

@@ -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+

@@ -1,5 +1,4 @@ {-# LANGUAGE TemplateHaskell #-}-{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}  module ExampleSpec where