[WIP] Allow applicative idioms when solving tactics

plugins/tactics/src/Ide/Plugin/Tactic.hs

@@ -31,6 +31,7 @@ import           Data.Monoid
 import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
+import           Development.IDE (HscEnvEq(hscEnv))
 import           Development.IDE.Core.PositionMapping
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Service (runAction)
@@ -258,11 +259,13 @@ judgementForHole state nfp range = do
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
+  (hsc, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
       tcs = tm_typechecked_source $ tmrModule tcmod
       ctx = mkContext
               (mapMaybe (sequenceA . (occName *** coerce))
                 $ getDefiningBindings binds rss)
+              (hscEnv hsc)
               tcg
       hyps = hypothesisFromBindings rss binds
       ambient = M.fromList $ contextMethodHypothesis ctx
@@ -289,11 +292,12 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        x <- lift $ timeout 2e8 $
-          case runTactic ctx jdg
-                $ tac
-                $ mkVarOcc
-                $ T.unpack var_name of
+        x <- lift $ timeout 2e8 $ do
+          res <- runTactic ctx jdg
+               $ tac
+               $ mkVarOcc
+               $ T.unpack var_name
+          case res of
             Left err ->
               pure $ (, Nothing)
                 $ Left

plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs

@@ -1,8 +1,9 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TupleSections    #-}
-{-# LANGUAGE ViewPatterns     #-}
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections     #-}
+{-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE ViewPatterns      #-}
 
 module Ide.Plugin.Tactic.CodeGen where
 
@@ -211,6 +212,16 @@ coerceName :: HasOccName a => a -> RdrNameStr
 coerceName = fromString . occNameString . occName
 
 
+------------------------------------------------------------------------------
+-- | Converts a function application into applicative form
+idiomize :: LHsExpr GhcPs -> LHsExpr GhcPs
+idiomize x = noLoc $ case unLoc x of
+   HsApp _ (L _ (HsVar _ (L _ x))) gshgp3 ->
+     op (bvar' $ occName x) "<$>" (unLoc gshgp3)
+   HsApp _ gsigp gshgp3 ->
+     op (unLoc $ idiomize gsigp) "<*>" (unLoc gshgp3)
+   y -> y
+
 
 ------------------------------------------------------------------------------
 -- | Like 'var', but works over standard GHC 'OccName's.

plugins/tactics/src/Ide/Plugin/Tactic/Context.hs

@@ -11,26 +11,33 @@ import           Data.Maybe (mapMaybe)
 import           Data.Set (Set)
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
+import           FastString (fsLit)
 import           Ide.Plugin.Tactic.GHC (tacticsThetaTy)
 import           Ide.Plugin.Tactic.Machinery (methodHypothesis)
 import           Ide.Plugin.Tactic.Types
 import           OccName
+import           SrcLoc
+import           TcRnMonad (initTcWithGbl)
 import           TcRnTypes
 import           TcType (substTy, tcSplitSigmaTy)
 import           Unify (tcUnifyTy)
 
 
-mkContext :: [(OccName, CType)] -> TcGblEnv -> Context
-mkContext locals tcg = Context
+mkContext :: [(OccName, CType)] -> HscEnv -> TcGblEnv -> Context
+mkContext locals env tcg = Context
   { ctxDefiningFuncs = locals
   , ctxModuleFuncs = fmap splitId
                    . (getFunBindId =<<)
                    . fmap unLoc
                    . bagToList
                    $ tcg_binds tcg
+  , ctxRunTcM = \tcr -> do
+      let loc = mkRealSrcLoc (fsLit "generated") 0 0
+      fmap snd $ initTcWithGbl env tcg (mkRealSrcSpan loc loc) tcr
   }
 
 
+
 ------------------------------------------------------------------------------
 -- | Find all of the class methods that exist from the givens in the context.
 contextMethodHypothesis :: Context -> [(OccName, CType)]
@@ -56,8 +63,34 @@ excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods  . fst)
   where
     forbiddenMethods :: Set OccName
     forbiddenMethods = S.map mkVarOcc $ S.fromList
-      [ -- monadfail
-        "fail"
+      [ -- applicative methods
+        "<*"
+      , "<$"
+        -- monad methods
+      , ">>"
+      , "return"
+        -- foldable methods
+      , "foldMap'"
+      , "foldr"
+      , "foldl"
+      , "foldr'"
+      , "foldl'"
+      , "foldr1"
+      , "foldl1"
+      , "maximum"
+      , "minimum"
+      , "sum"
+      , "product"
+      , "elem"
+      , "null"
+      , "mapM"
+        -- traversable methods
+      , "sequence"
+      , "pass"
+      , "censor"
+      , "state"
+        -- monadfail methods
+      , "fail"
       ]
 
 

plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs

@@ -5,21 +5,32 @@
 
 module Ide.Plugin.Tactic.GHC where
 
+import           Control.Arrow
 import           Control.Monad.State
 import qualified Data.Map as M
 import           Data.Maybe (isJust)
 import           Data.Traversable
 import           Development.IDE.GHC.Compat
 import           Generics.SYB (mkT, everywhere)
+import           Id (mkVanillaGlobal)
 import           Ide.Plugin.Tactic.Types
 import           OccName
+import           TcEnv (tcLookupTyCon)
+import           TcEvidence (TcEvBinds (..), evBindMapBinds)
+import           TcRnMonad
+import           TcSMonad (runTcS)
+import           TcSimplify (solveWanteds)
 import           TcType
 import           TyCoRep
 import           Type
 import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import           Unique
 import           Var
 
+#if __GLASGOW_HASKELL__ >= 810
+import Constraint
+#endif
+
 
 tcTyVar_maybe :: Type -> Maybe Var
 tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty'
@@ -148,3 +159,31 @@ getPatName (fromPatCompat -> p0) =
 #endif
     _             -> Nothing
 
+
+-- Generates the evidence for `Show ()`.
+generateDictionary :: Name -> [Type] -> TcM (Var, TcEvBinds)
+generateDictionary cls tys = do
+  showTyCon <- tcLookupTyCon cls
+  dictName <- newName $ mkDictOcc $ mkVarOcc "magic"
+  let dict_ty  = mkTyConApp showTyCon tys
+      dict_var = mkVanillaGlobal dictName dict_ty
+  ev <- getDictionaryBindings dict_var
+  return (dict_var, ev)
+
+
+-- Pass in a variable `x` which has type `Show ()` (for example) to generate
+-- evidence for `Show ()` which will be bound to `x`.
+getDictionaryBindings :: Var -> TcM TcEvBinds
+getDictionaryBindings dict_var = do
+    loc <- getCtLocM (GivenOrigin UnkSkol) Nothing
+    let nonC = mkNonCanonical CtWanted
+            { ctev_pred = varType dict_var
+            , ctev_nosh = WDeriv
+            , ctev_dest = EvVarDest dict_var
+            , ctev_loc = loc
+            }
+        wCs = mkSimpleWC [cc_ev nonC]
+    traceMX "looking for a wanted: " $ unsafeRender wCs
+    (_, evBinds) <- second evBindMapBinds <$> runTcS (solveWanteds wCs)
+    return (EvBinds evBinds)
+

plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs

@@ -70,6 +70,13 @@ withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t = field @"_jGoal" .~ t
 
 
+------------------------------------------------------------------------------
+-- | Like 'withNewGoal' but allows you to modify the goal rather than replacing
+-- it.
+withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a
+withModifiedGoal f = field @"_jGoal" %~ f
+
+
 introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
 introducing ns =
   field @"_jHypothesis" <>~ M.fromList ns

plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs

@@ -32,17 +32,25 @@ import           Data.Functor ((<&>))
 import           Data.Generics (mkQ, everything, gcount)
 import           Data.List (nub, sortBy)
 import           Data.Ord (comparing, Down(..))
+import           Data.Set (Set)
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
+import           HscTypes (lookupTypeEnv)
 import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Types
-import           OccName (HasOccName(occName))
+import           InstEnv (emptyInstEnv, lookupInstEnv, InstEnvs(InstEnvs))
+import           Module (emptyModuleSet)
+import           OccName (mkVarOcc, HasOccName(occName))
 import           Refinery.ProofState
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
+import TcEnv (tcLookupGlobal)
+import Ide.Plugin.Tactic.GHC (generateDictionary)
+import TcEvidence (TcEvBinds(EvBinds))
+import Bag (isEmptyBag)
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -69,8 +77,8 @@ runTactic
     :: Context
     -> Judgement
     -> TacticsM ()       -- ^ Tactic to use
-    -> Either [TacticError] RunTacticResults
-runTactic ctx jdg t =
+    -> IO (Either [TacticError] RunTacticResults)
+runTactic ctx jdg t = do
     let skolems = nub
                 $ foldMap (tyCoVarsOfTypeWellScoped . unCType)
                 $ jGoal jdg
@@ -81,10 +89,10 @@ runTactic ctx jdg t =
             { ts_skolems = skolems
             , ts_unused_top_vals = S.fromList unused_topvals
             }
-    in case partitionEithers
-          . flip runReader ctx
+    res <- flip runReaderT ctx
           . unExtractM
-          $ runTacticT t jdg tacticState of
+          $ runTacticT t jdg tacticState
+    pure $ case partitionEithers res of
       (errs, []) -> Left $ take 50 $ errs
       (_, fmap assoc23 -> solns) -> do
         let sorted =
@@ -229,6 +237,20 @@ methodHypothesis ty = do
 
 
 ------------------------------------------------------------------------------
+-- | Check if the types have a MPTC instance for the given clas name.;
+hasInstance :: MonadTc m => Name -> [Type] -> m Bool
+hasInstance nm tys = do
+  liftTc (generateDictionary nm tys) >>= \case
+    Just (_, ev) -> do
+      case ev of
+        EvBinds bag -> do
+          pure $ not $ isEmptyBag bag
+        _ -> pure False
+    Nothing -> do
+      pure False
+
+
+--------------------------------------------------------------------------------
 -- | Run the given tactic iff the current hole contains no univars. Skolems and
 -- already decided univars are OK though.
 requireConcreteHole :: TacticsM a -> TacticsM a
@@ -240,3 +262,16 @@ requireConcreteHole m = do
     0 -> m
     _ -> throwError TooPolymorphic
 
+
+------------------------------------------------------------------------------
+-- | Prevent the tactic from running when deriving a function with a name in
+-- the given set. Useful for preventing bottoms.
+disallowWhenDeriving
+    :: Set String
+    -> TacticsM a
+    -> TacticsM a
+disallowWhenDeriving what m = do
+  defs <- asks $ S.fromList . fmap fst . ctxDefiningFuncs
+  case S.null $ S.intersection defs $ S.map mkVarOcc what of
+    True  -> m
+    False -> throwError NoProgress