Properly scope GADT equality evidence in the judgment (#1942)

* Properly scope GADT equality evidence in the judgment

Fixes #1937

* Haddock and a bit of refactoring

* Track coercions in a TCvSubst instead

Author: isovector

plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs

@@ -68,8 +68,6 @@ destructMatches use_field_puns f scrut t jdg = do
             -- #syn_scoped
             method_hy = foldMap evidenceToHypothesis ev
             args = conLikeInstOrigArgTys' con apps
-        modify $ evidenceToSubst ev
-        subst <- gets ts_unifier
         ctx <- ask
 
         let names_in_scope = hyNamesInScope hy
@@ -80,7 +78,7 @@ destructMatches use_field_puns f scrut t jdg = do
         let hy' = patternHypothesis scrut con jdg
                 $ zip names'
                 $ coerce args
-            j = fmap (CType . substTyAddInScope subst . unCType)
+            j = withNewCoercions (evidenceToCoercions ev)
               $ introduce ctx hy'
               $ introduce ctx method_hy
               $ withNewGoal g jdg

plugins/hls-tactics-plugin/src/Wingman/Judgements.hs

@@ -18,6 +18,7 @@ import           OccName
 import           SrcLoc
 import           Type
 import           Wingman.GHC (algebraicTyCon, normalizeType)
+import           Wingman.Judgements.Theta
 import           Wingman.Types
 
 
@@ -69,6 +70,15 @@ withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t = field @"_jGoal" .~ t
 
 
+------------------------------------------------------------------------------
+-- | Add some new type equalities to the local judgement.
+withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement
+withNewCoercions ev j =
+  let subst = allEvidenceToSubst mempty $ coerce ev
+   in fmap (CType . substTyAddInScope subst . unCType) j
+      & field @"j_coercion" %~ unionTCvSubst subst
+
+
 normalizeHypothesis :: Functor f => Context -> f CType -> f CType
 normalizeHypothesis = fmap . coerce . normalizeType
 
@@ -414,6 +424,7 @@ mkFirstJudgement ctx hy top goal =
       , _jWhitelistSplit    = True
       , _jIsTopHole         = top
       , _jGoal              = CType goal
+      , j_coercion          = emptyTCvSubst
       }
 
 

plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs

@@ -5,14 +5,17 @@ module Wingman.Judgements.Theta
   ( Evidence
   , getEvidenceAtHole
   , mkEvidence
+  , evidenceToCoercions
   , evidenceToSubst
   , evidenceToHypothesis
   , evidenceToThetaType
+  , allEvidenceToSubst
   ) where
 
 import           Class (classTyVars)
 import           Control.Applicative (empty)
 import           Control.Lens (preview)
+import           Data.Coerce (coerce)
 import           Data.Maybe (fromMaybe, mapMaybe, maybeToList)
 import           Data.Generics.Sum (_Ctor)
 import           Data.Set (Set)
@@ -109,14 +112,17 @@ allEvidenceToSubst skolems ((a, b) : evs) =
     $ allEvidenceToSubst skolems
     $ fmap (substPair subst) evs
 
+------------------------------------------------------------------------------
+-- | Given some 'Evidence', get a list of which types are now equal.
+evidenceToCoercions :: [Evidence] -> [(CType, CType)]
+evidenceToCoercions = coerce . mapMaybe (preview $ _Ctor @"EqualityOfTypes")
+
 ------------------------------------------------------------------------------
 -- | Update our knowledge of which types are equal.
 evidenceToSubst :: [Evidence] -> TacticState -> TacticState
 evidenceToSubst evs ts =
   updateSubst
-    (allEvidenceToSubst (ts_skolems ts)
-      $ mapMaybe (preview $ _Ctor @"EqualityOfTypes")
-      $ evs)
+    (allEvidenceToSubst (ts_skolems ts) . coerce $ evidenceToCoercions evs)
     ts
 
 

plugins/hls-tactics-plugin/src/Wingman/Machinery.hs

@@ -40,6 +40,17 @@ substCTy :: TCvSubst -> CType -> CType
 substCTy subst = coerce . substTy subst . coerce
 
 
+getSubstForJudgement
+    :: MonadState TacticState m
+    => Judgement
+    -> m TCvSubst
+getSubstForJudgement j = do
+  -- NOTE(sandy): It's OK to use mempty here, because coercions _can_ give us
+  -- substitutions for skolems.
+  let coercions = j_coercion j
+  unifier <- gets ts_unifier
+  pure $ unionTCvSubst unifier coercions
+
 ------------------------------------------------------------------------------
 -- | Produce a subgoal that must be solved before we can solve the original
 -- goal.
@@ -48,7 +59,7 @@ newSubgoal
     -> Rule
 newSubgoal j = do
   ctx <- ask
-  unifier <- gets ts_unifier
+  unifier <- getSubstForJudgement j
   subgoal
     $ normalizeJudgement ctx
     $ substJdg unifier

plugins/hls-tactics-plugin/src/Wingman/Tactics.hs

@@ -13,7 +13,7 @@ import           Control.Monad (unless)
 import           Control.Monad.Except (throwError)
 import           Control.Monad.Extra (anyM)
 import           Control.Monad.Reader.Class (MonadReader (ask))
-import           Control.Monad.State.Strict (StateT(..), runStateT, gets)
+import           Control.Monad.State.Strict (StateT(..), runStateT)
 import           Data.Bool (bool)
 import           Data.Foldable
 import           Data.Functor ((<&>))
@@ -72,6 +72,10 @@ 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!
+
+-- TODO(sandy): There's a bug here! This should use the polymorphic defining
+-- types, not the ones available via 'getCurrentDefinitions'. As it is, this
+-- tactic doesn't support polymorphic recursion.
 recursion = requireConcreteHole $ tracing "recursion" $ do
   defs <- getCurrentDefinitions
   attemptOn (const defs) $ \(name, ty) -> markRecursion $ do
@@ -349,7 +353,7 @@ destructAll = do
            $ unHypothesis
            $ jHypothesis jdg
   for_ args $ \arg -> do
-    subst <- gets ts_unifier
+    subst <- getSubstForJudgement =<< goal
     destruct $ fmap (coerce substTy subst) arg
 
 --------------------------------------------------------------------------------

plugins/hls-tactics-plugin/src/Wingman/Types.hs

@@ -297,8 +297,9 @@ data Judgement' a = Judgement
   , _jWhitelistSplit    :: !Bool
   , _jIsTopHole         :: !Bool
   , _jGoal              :: !a
+  , j_coercion          :: TCvSubst
   }
-  deriving stock (Eq, Generic, Functor, Show)
+  deriving stock (Generic, Functor, Show)
 
 type Judgement = Judgement' CType
 
@@ -328,7 +329,6 @@ data TacticError
   | TooPolymorphic
   | NotInScope OccName
   | TacticPanic String
-  deriving stock (Eq)
 
 instance Show TacticError where
     show (UndefinedHypothesis name) =

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

@@ -33,6 +33,6 @@ spec = do
     metaTest 11 11 "MetaUseMethod"
     metaTest  9 38 "MetaCataCollapse"
     metaTest  7 16 "MetaCataCollapseUnary"
-    metaTest 21 32 "MetaCataAST"
+    metaTest 10 32 "MetaCataAST"
     metaTest  6 46 "MetaPointwise"
     metaTest  4 28 "MetaUseSymbol"

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

@@ -7,19 +7,8 @@ data AST a where
     Equal :: AST a -> AST a -> AST Bool
 
 eval :: AST a -> a
--- NOTE(sandy): There is an unrelated bug that is shown off in this test
--- namely, that
---
--- @eval (IntLit n) = _@
---
--- but should be
---
--- @eval (IntLit n) = n@
---
--- https://github.com/haskell/haskell-language-server/issues/1937
-
 eval (BoolLit b) = b
-eval (IntLit n) = _
+eval (IntLit n) = n
 eval (If ast ast' ast_a)
   = let
       ast_c = eval ast

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

@@ -7,16 +7,5 @@ data AST a where
     Equal :: AST a -> AST a -> AST Bool
 
 eval :: AST a -> a
--- NOTE(sandy): There is an unrelated bug that is shown off in this test
--- namely, that
---
--- @eval (IntLit n) = _@
---
--- but should be
---
--- @eval (IntLit n) = n@
---
--- https://github.com/haskell/haskell-language-server/issues/1937
-
 eval = [wingman| intros x, cata x; collapse |]