Fix a wingman bug caused by mismanaged stale data

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

ghcide/src/Development/IDE/Core/PositionMapping.hs

@@ -11,6 +11,7 @@ module Development.IDE.Core.PositionMapping
   , PositionDelta(..)
   , addDelta
   , idDelta
+  , composeDelta
   , mkDelta
   , toCurrentRange
   , fromCurrentRange

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
 

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

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

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