Fix a wingman bug caused by mismanaged stale data (#1657)

* Start tracking provenance of stale data It's amazing how wrong this code used to be * Add some machinery for automagically updating the age * Add an applicative instance * Tracked ages makes everything much easier to reason about * Formatting * Haddock and small changes * Update haddock on IdeAction * Update to lsp-1.2 (#1631) * Update to lsp-1.2 * fix stack * fix splice plugin tests * fix tactic plugin tests * fix some tests * fix some tests * fix outline tests * hlint * fix func-test * Avoid reordering plugins (#1629) * Avoid reordering plugins Order of execution matters for notification plugins, so lets avoid unnecessary reorderings * remove duplicate plugins * fix tests * Civilized indexing progress reporting (#1633) * Civilized indexing progress reporting * optProgressStyle * Consistency: Indexing references ==> Indexing * Fix progress tests * Do not override custom user commands (#1650) Co-authored-by: Potato Hatsue <1793913507@qq.com> * Shut the Shake session on exit, instead of restarting it (#1655) Restarting the session will result in progress reporting and other messages being sent to the client, which might have already closed the stream Co-authored-by: Potato Hatsue <1793913507@qq.com> * Fix importing type operators (#1644) * Fix importing type operators * Update test * Add expected failure tests * log exceptions before killing the server (#1651) * log hiedb exceptions before killing the server * This is not the hiedb thread - fix message * Fix handler - either an error or success * additional .gitignore entries (#1659) * Fix ignore paths (#1656) * Skip individual steps * Skip individual steps * And needs pre_job * Add bounds for Diff (#1665) * Replace Barrier with MVar in lsp main (#1668) * Port UseStale to ghcide * Use the new ghcide UseStale machinery * Fix hlint complaints Co-authored-by: wz1000 <zubin.duggal@gmail.com> Co-authored-by: Pepe Iborra <pepeiborra@gmail.com> Co-authored-by: Potato Hatsue <1793913507@qq.com> Co-authored-by: Javier Neira <atreyu.bbb@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
haskell · Apr 6, 2021 · c6421fd · c6421fd
1 parent 334f185
commit c6421fd
Show file tree

Hide file tree

Showing 11 changed files with 305 additions and 97 deletions.
diff --git a/ghcide/ghcide.cabal b/ghcide/ghcide.cabal
@@ -114,6 +114,8 @@ library
  BangPatterns
  DeriveFunctor
  DeriveGeneric
+ DeriveFoldable
+ DeriveTraversable
  FlexibleContexts
  GeneralizedNewtypeDeriving
  LambdaCase
@@ -149,6 +151,7 @@ library
  Development.IDE.Core.Service
  Development.IDE.Core.Shake
  Development.IDE.Core.Tracing
+ Development.IDE.Core.UseStale
  Development.IDE.GHC.Compat
  Development.IDE.Core.Compile
  Development.IDE.GHC.Error

diff --git a/ghcide/src/Development/IDE/Core/PositionMapping.hs b/ghcide/src/Development/IDE/Core/PositionMapping.hs
@@ -11,6 +11,7 @@ module Development.IDE.Core.PositionMapping
  , PositionDelta(..)
  , addDelta
  , idDelta
+ , composeDelta
  , mkDelta
  , toCurrentRange
  , fromCurrentRange

diff --git a/ghcide/src/Development/IDE/Core/Shake.hs b/ghcide/src/Development/IDE/Core/Shake.hs
@@ -838,12 +838,14 @@ usesWithStale_ key files = do
  Nothing -> liftIO $ throwIO $ BadDependency (show key)
  Just v -> return v
 
-newtype IdeAction a = IdeAction { runIdeActionT :: (ReaderT ShakeExtras IO) a }
- deriving newtype (MonadReader ShakeExtras, MonadIO, Functor, Applicative, Monad)
-
 -- | IdeActions are used when we want to return a result immediately, even if it
 -- is stale Useful for UI actions like hover, completion where we don't want to
 -- block.
+--
+-- Run via 'runIdeAction'.
+newtype IdeAction a = IdeAction { runIdeActionT :: (ReaderT ShakeExtras IO) a }
+ deriving newtype (MonadReader ShakeExtras, MonadIO, Functor, Applicative, Monad)
+
 runIdeAction :: String -> ShakeExtras -> IdeAction a -> IO a
 runIdeAction _herald s i = runReaderT (runIdeActionT i) s
 

diff --git a/ghcide/src/Development/IDE/Core/UseStale.hs b/ghcide/src/Development/IDE/Core/UseStale.hs
@@ -0,0 +1,153 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Development.IDE.Core.UseStale
+ ( Age(..)
+ , Tracked
+ , unTrack
+ , PositionMap
+ , TrackedStale (..)
+ , unsafeMkStale
+ , unsafeMkCurrent
+ , unsafeCopyAge
+ , MapAge (..)
+ , dualPositionMap
+ , useWithStale
+ , useWithStale_
+ ) where
+
+import Control.Arrow
+import Control.Category (Category)
+import qualified Control.Category as C
+import Control.DeepSeq (NFData)
+import Data.Aeson
+import Data.Coerce (coerce)
+import Data.Functor ((<&>))
+import Data.Functor.Identity (Identity(Identity))
+import Data.Kind (Type)
+import Data.String (fromString)
+import Development.IDE (NormalizedFilePath, IdeRule, Action, Range, rangeToRealSrcSpan, realSrcSpanToRange)
+import qualified Development.IDE.Core.PositionMapping as P
+import qualified Development.IDE.Core.Shake as IDE
+import qualified FastString as FS
+import SrcLoc
+
+
+------------------------------------------------------------------------------
+-- | A data kind for 'Tracked'.
+data Age = Current | Stale Type
+
+
+------------------------------------------------------------------------------
+-- | Some value, tagged with its age. All 'Current' ages are considered to be
+-- the same thing, but 'Stale' values are protected by an untouchable variable
+-- to ensure they can't be unified.
+newtype Tracked (age :: Age) a = UnsafeTracked
+ { unTrack :: a
+ }
+ deriving stock (Functor, Foldable, Traversable)
+ deriving newtype (Eq, Ord, Show, Read, ToJSON, FromJSON, NFData)
+ deriving (Applicative, Monad) via Identity
+
+
+------------------------------------------------------------------------------
+-- | Like 'P.PositionMapping', but with annotated ages for how 'Tracked' values
+-- change. Use the 'Category' instance to compose 'PositionMapping's in order
+-- to transform between values of different stale ages.
+newtype PositionMap (from :: Age) (to :: Age) = PositionMap
+ { getPositionMapping :: P.PositionMapping
+ }
+
+instance Category PositionMap where
+ id = coerce P.zeroMapping
+ (.) = coerce P.composeDelta
+
+
+------------------------------------------------------------------------------
+-- | Get a 'PositionMap' that runs in the opposite direction.
+dualPositionMap :: PositionMap from to -> PositionMap to from
+dualPositionMap (PositionMap (P.PositionMapping (P.PositionDelta from to))) =
+ PositionMap $ P.PositionMapping $ P.PositionDelta to from
+
+
+------------------------------------------------------------------------------
+-- | A pair containing a @'Tracked' 'Stale'@ value, as well as
+-- a 'PositionMapping' that will fast-forward values to the current age.
+data TrackedStale a where
+ TrackedStale
+ :: Tracked (Stale s) a
+ -> PositionMap (Stale s) Current
+ -> TrackedStale a
+
+instance Functor TrackedStale where
+ fmap f (TrackedStale t pm) = TrackedStale (fmap f t) pm
+
+
+------------------------------------------------------------------------------
+-- | A class for which 'Tracked' values can be run across a 'PositionMapping'
+-- to change their ages.
+class MapAge a where
+ {-# MINIMAL mapAgeFrom | mapAgeTo #-}
+ mapAgeFrom :: PositionMap from to -> Tracked to a -> Maybe (Tracked from a)
+ mapAgeFrom = mapAgeTo . dualPositionMap
+
+ mapAgeTo :: PositionMap from to -> Tracked from a -> Maybe (Tracked to a)
+ mapAgeTo = mapAgeFrom . dualPositionMap
+
+
+instance MapAge Range where
+ mapAgeFrom = coerce P.fromCurrentRange
+ mapAgeTo = coerce P.toCurrentRange
+
+
+instance MapAge RealSrcSpan where
+ mapAgeFrom =
+ invMapAge (\fs -> rangeToRealSrcSpan (fromString $ FS.unpackFS fs))
+ (srcSpanFile &&& realSrcSpanToRange)
+ . mapAgeFrom
+
+
+------------------------------------------------------------------------------
+-- | Helper function for deriving 'MapAge' for values in terms of other
+-- instances.
+invMapAge
+ :: (c -> a -> b)
+ -> (b -> (c, a))
+ -> (Tracked from a -> Maybe (Tracked to a))
+ -> Tracked from b
+ -> Maybe (Tracked to b)
+invMapAge to from f t =
+ let (c, t') = unTrack $ fmap from t
+ in fmap (fmap $ to c) $ f $ UnsafeTracked t'
+
+
+unsafeMkCurrent :: age -> Tracked 'Current age
+unsafeMkCurrent = coerce
+
+
+unsafeMkStale :: age -> Tracked (Stale s) age
+unsafeMkStale = coerce
+
+
+unsafeCopyAge :: Tracked age a -> b -> Tracked age b
+unsafeCopyAge _ = coerce
+
+
+-- | Request a Rule result, it not available return the last computed result, if any, which may be stale
+useWithStale :: IdeRule k v
+ => k -> NormalizedFilePath -> Action (Maybe (TrackedStale v))
+useWithStale key file = do
+ x <- IDE.useWithStale key file
+ pure $ x <&> \(v, pm) ->
+ TrackedStale (coerce v) (coerce pm)
+
+-- | Request a Rule result, it not available return the last computed result which may be stale.
+-- Errors out if none available.
+useWithStale_ :: IdeRule k v
+ => k -> NormalizedFilePath -> Action (TrackedStale v)
+useWithStale_ key file = do
+ (v, pm) <- IDE.useWithStale_ key file
+ pure $ TrackedStale (coerce v) (coerce pm)
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
@@ -12,6 +12,7 @@ import qualified Data.Map as M
 import Data.Maybe
 import Data.Set (Set)
 import qualified Data.Set as S
+import Development.IDE.Core.UseStale (Tracked, unTrack)
 import Development.IDE.Spans.LocalBindings
 import OccName
 import SrcLoc
@@ -22,8 +23,8 @@ import Wingman.Types
 
 ------------------------------------------------------------------------------
 -- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.
-hypothesisFromBindings :: RealSrcSpan -> Bindings -> Hypothesis CType
-hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span
+hypothesisFromBindings :: Tracked age RealSrcSpan -> Tracked age Bindings -> Hypothesis CType
+hypothesisFromBindings (unTrack -> span) (unTrack -> bs) = buildHypothesis $ getLocalScope bs span
 
 
 ------------------------------------------------------------------------------

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
@@ -12,6 +12,7 @@ module Wingman.Judgements.Theta
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Set (Set)
 import qualified Data.Set as S
+import Development.IDE.Core.UseStale
 import Development.IDE.GHC.Compat
 import Generics.SYB hiding (tyConName)
 import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe)
@@ -50,11 +51,12 @@ mkEvidence _ = Nothing
 
 ------------------------------------------------------------------------------
 -- | Compute all the 'Evidence' implicitly bound at the given 'SrcSpan'.
-getEvidenceAtHole :: SrcSpan -> LHsBinds GhcTc -> [Evidence]
-getEvidenceAtHole dst
+getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
+getEvidenceAtHole (unTrack -> dst)
  = mapMaybe mkEvidence
  . (everything (<>) $
  mkQ mempty (absBinds dst) `extQ` wrapperBinds dst `extQ` matchBinds dst)
+ . unTrack
 
 
 ------------------------------------------------------------------------------