Pull Wingman's method hypotheses directly from in-scope dicts

plugins/hls-tactics-plugin/hls-tactics-plugin.cabal

@@ -34,6 +34,7 @@ library
     Ide.Plugin.Tactic.FeatureSet
     Ide.Plugin.Tactic.GHC
     Ide.Plugin.Tactic.Judgements
+    Ide.Plugin.Tactic.Judgements.Theta
     Ide.Plugin.Tactic.KnownStrategies
     Ide.Plugin.Tactic.KnownStrategies.QuickCheck
     Ide.Plugin.Tactic.LanguageServer

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs

@@ -3,22 +3,14 @@
 
 module Ide.Plugin.Tactic.Context where
 
-import           Bag
-import           Control.Arrow
-import           Control.Monad.Reader
-import           Data.List
-import           Data.Maybe                   (mapMaybe)
-import           Data.Set                     (Set)
-import qualified Data.Set                     as S
-import           Development.IDE.GHC.Compat
-import           Ide.Plugin.Tactic.FeatureSet (FeatureSet)
-import           Ide.Plugin.Tactic.GHC        (tacticsThetaTy)
-import           Ide.Plugin.Tactic.Machinery  (methodHypothesis)
-import           Ide.Plugin.Tactic.Types
-import           OccName
-import           TcRnTypes
-import           TcType                       (substTy, tcSplitSigmaTy)
-import           Unify                        (tcUnifyTy)
+import Bag
+import Control.Arrow
+import Control.Monad.Reader
+import Development.IDE.GHC.Compat
+import Ide.Plugin.Tactic.FeatureSet (FeatureSet)
+import Ide.Plugin.Tactic.Types
+import OccName
+import TcRnTypes
 
 
 mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context
@@ -33,49 +25,6 @@ mkContext features locals tcg = Context
   }
 
 
-------------------------------------------------------------------------------
--- | Find all of the class methods that exist from the givens in the context.
-contextMethodHypothesis :: Context -> Hypothesis CType
-contextMethodHypothesis ctx
-  = Hypothesis
-  . excludeForbiddenMethods
-  . join
-  . concatMap
-      ( mapMaybe methodHypothesis
-      . tacticsThetaTy
-      . unCType
-      )
-  . mapMaybe (definedThetaType ctx)
-  . fmap fst
-  $ ctxDefiningFuncs ctx
-
-
-------------------------------------------------------------------------------
--- | Many operations are defined in typeclasses for performance reasons, rather
--- than being a true part of the class. This function filters out those, in
--- order to keep our hypothesis space small.
-excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
-excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)
-  where
-    forbiddenMethods :: Set OccName
-    forbiddenMethods = S.map mkVarOcc $ S.fromList
-      [ -- monadfail
-        "fail"
-      ]
-
-
-------------------------------------------------------------------------------
--- | Given the name of a function that exists in 'ctxDefiningFuncs', get its
--- theta type.
-definedThetaType :: Context -> OccName -> Maybe CType
-definedThetaType ctx name = do
-  (_, CType mono) <- find ((== name) . fst) $ ctxDefiningFuncs ctx
-  (_, CType poly) <- find ((== name) . fst) $ ctxModuleFuncs ctx
-  let (_, _, poly') = tcSplitSigmaTy poly
-  subst <- tcUnifyTy poly' mono
-  pure $ CType $ substTy subst $ snd $ splitForAllTys poly
-
-
 splitId :: Id -> (OccName, CType)
 splitId = occName &&& CType . idType
 
@@ -91,5 +40,3 @@ getFunBindId _ = []
 getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
 getCurrentDefinitions = asks ctxDefiningFuncs
 
-getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)]
-getModuleHypothesis = asks ctxModuleFuncs

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs

@@ -0,0 +1,50 @@
+{-# LANGUAGE ViewPatterns #-}
+
+module Ide.Plugin.Tactic.Judgements.Theta
+  ( getMethodHypothesisAtHole
+  ) where
+
+import           Data.Maybe (fromMaybe)
+import           Data.Set (Set)
+import qualified Data.Set as S
+import           Development.IDE.GHC.Compat
+import           Generics.SYB
+import           GhcPlugins (EvVar, mkVarOcc)
+import           Ide.Plugin.Tactic.Machinery
+import           Ide.Plugin.Tactic.Types
+
+
+------------------------------------------------------------------------------
+-- | Create a 'Hypothesis' containing 'ClassMethodPrv' provenance. For every
+-- dictionary that is in scope at the given 'SrcSpan', find every method and
+-- superclass method available.
+getMethodHypothesisAtHole :: SrcSpan -> LHsBinds GhcTc -> Hypothesis CType
+getMethodHypothesisAtHole dst
+  = Hypothesis
+  . excludeForbiddenMethods
+  . fromMaybe []
+  . foldMap methodHypothesis
+  . (everything (<>) $ mkQ mempty $ evbinds dst)
+
+
+------------------------------------------------------------------------------
+-- | Many operations are defined in typeclasses for performance reasons, rather
+-- than being a true part of the class. This function filters out those, in
+-- order to keep our hypothesis space small.
+excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
+excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)
+  where
+    forbiddenMethods :: Set OccName
+    forbiddenMethods = S.map mkVarOcc $ S.fromList
+      [ -- monadfail
+        "fail"
+      ]
+
+
+------------------------------------------------------------------------------
+-- | Extract the types of the evidence bindings in scope.
+evbinds ::  SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
+evbinds dst (L src (AbsBinds _ _ h _ _ _ _))
+  | dst `isSubspanOf` src = fmap idType h
+evbinds _ _ = []
+

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs

@@ -44,6 +44,7 @@ import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.FeatureSet
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.Judgements.Theta (getMethodHypothesisAtHole)
 import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.Types
 import           Language.LSP.Server (MonadLsp, sendNotification)
@@ -139,7 +140,7 @@ mkJudgementAndContext
     -> TcModuleResult
     -> (Judgement, Context)
 mkJudgementAndContext features g binds rss tcmod = do
-      let tcg  = tmrTypechecked tcmod
+      let tcg = tmrTypechecked tcmod
           tcs = tcg_binds tcg
           ctx = mkContext features
                   (mapMaybe (sequenceA . (occName *** coerce))
@@ -148,7 +149,7 @@ mkJudgementAndContext features g binds rss tcmod = do
           top_provs = getRhsPosVals rss tcs
           local_hy = spliceProvenance top_provs
                    $ hypothesisFromBindings rss binds
-          cls_hy = contextMethodHypothesis ctx
+          cls_hy = getMethodHypothesisAtHole (RealSrcSpan rss) tcs
        in ( mkFirstJudgement
               (local_hy <> cls_hy)
               (isRhsHole rss tcs)

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs

@@ -68,6 +68,8 @@ assume name = rule $ \jdg -> do
 
 
 recursion :: TacticsM ()
+-- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test,
+-- presumably due to running afoul of 'requireConcreteHole'. Look into this!
 recursion = requireConcreteHole $ tracing "recursion" $ do
   defs <- getCurrentDefinitions
   attemptOn (const defs) $ \(name, ty) -> markRecursion $ do

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs

@@ -124,6 +124,12 @@ instance Show CType where
 instance Show OccName where
   show  = unsafeRender
 
+instance Show Name where
+  show  = unsafeRender
+
+instance Show Type where
+  show  = unsafeRender
+
 instance Show Var where
   show  = unsafeRender
 
@@ -142,6 +148,9 @@ instance Show (HsExpr GhcPs) where
 instance Show (Pat GhcPs) where
   show  = unsafeRender
 
+instance Show (LHsSigType GhcPs) where
+  show  = unsafeRender
+
 
 ------------------------------------------------------------------------------
 -- | The state that should be shared between subgoals. Extracts move towards

plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs

@@ -47,6 +47,7 @@ spec = do
     autoTest  2  9 "Fgmap.hs"
     autoTest  4 19 "FmapJoinInLet.hs"
     autoTest  9 12 "AutoEndo.hs"
+    autoTest 12 10 "AutoThetaFix.hs"
 
     failing "flaky in CI" $
       autoTest 2 11 "GoldenApplicativeThen.hs"

plugins/hls-tactics-plugin/test/UnificationSpec.hs

@@ -4,25 +4,20 @@
 module UnificationSpec where
 
 import           Control.Arrow
-import           Data.Bool                   (bool)
-import           Data.Functor                ((<&>))
-import           Data.Maybe                  (mapMaybe)
-import qualified Data.Set                    as S
+import           Data.Bool (bool)
+import           Data.Functor ((<&>))
+import           Data.Maybe (mapMaybe)
+import qualified Data.Set as S
 import           Data.Traversable
-import           Data.Tuple                  (swap)
-import           Ide.Plugin.Tactic.Debug
+import           Data.Tuple (swap)
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Types
-import           TcType                      (substTy, tcGetTyVar_maybe)
+import           TcType (substTy, tcGetTyVar_maybe)
 import           Test.Hspec
 import           Test.QuickCheck
-import           Type                        (mkTyVarTy)
-import           TysPrim                     (alphaTyVars)
-import           TysWiredIn                  (mkBoxedTupleTy)
-
-
-instance Show Type where
-  show = unsafeRender
+import           Type (mkTyVarTy)
+import           TysPrim (alphaTyVars)
+import           TysWiredIn (mkBoxedTupleTy)
 
 
 spec :: Spec

plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs

@@ -0,0 +1,13 @@
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+data Fix f a = Fix (f (Fix f a))
+
+instance ( Functor f
+           -- FIXME(sandy): Unfortunately, the recursion tactic fails to fire
+           -- on this case. By explicitly adding the @Functor (Fix f)@
+           -- dictionary, we can get Wingman to generate the right definition.
+         , Functor (Fix f)
+         ) => Functor (Fix f) where
+  fmap = _
+

plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs.expected

@@ -0,0 +1,7 @@
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+data Fix f a = Fix (f (Fix f a))
+instance (Functor f, Functor (Fix f)) => Functor (Fix f) where
+  fmap fab (Fix fffa) = Fix (fmap (fmap fab) fffa)
+