Properly scope GADT equality evidence in the judgment

Fixes haskell#1937

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

@@ -69,6 +69,10 @@ withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t = field @"_jGoal" .~ t
 
 
+withNewCoercions :: [(a, a)] -> Judgement' a -> Judgement' a
+withNewCoercions ev = field @"j_coercion" <>~ ev
+
+
 normalizeHypothesis :: Functor f => Context -> f CType -> f CType
 normalizeHypothesis = fmap . coerce . normalizeType
 
@@ -414,6 +418,7 @@ mkFirstJudgement ctx hy top goal =
       , _jWhitelistSplit    = True
       , _jIsTopHole         = top
       , _jGoal              = CType goal
+      , j_coercion          = mempty
       }
 
 

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,6 +112,11 @@ allEvidenceToSubst skolems ((a, b) : evs) =
     $ allEvidenceToSubst skolems
     $ fmap (substPair subst) evs
 
+------------------------------------------------------------------------------
+-- | Update our knowledge of which types are equal.
+evidenceToCoercions :: [Evidence] -> [(CType, CType)]
+evidenceToCoercions = coerce . mapMaybe (preview $ _Ctor @"EqualityOfTypes")
+
 ------------------------------------------------------------------------------
 -- | Update our knowledge of which types are equal.
 evidenceToSubst :: [Evidence] -> TacticState -> TacticState

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

@@ -32,6 +32,7 @@ import           Type (tyCoVarsOfTypeWellScoped)
 import           Wingman.Context (getInstance)
 import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst)
 import           Wingman.Judgements
+import           Wingman.Judgements.Theta (allEvidenceToSubst)
 import           Wingman.Simplify (simplify)
 import           Wingman.Types
 
@@ -48,10 +49,12 @@ newSubgoal
     -> Rule
 newSubgoal j = do
   ctx <- ask
+  skolems <- gets ts_skolems
+  let coercions = allEvidenceToSubst skolems $ coerce $ j_coercion j
   unifier <- gets ts_unifier
   subgoal
     $ normalizeJudgement ctx
-    $ substJdg unifier
+    $ substJdg (unionTCvSubst unifier coercions)
     $ unsetIsTopHole
     $ normalizeJudgement ctx j
 

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

@@ -297,6 +297,7 @@ data Judgement' a = Judgement
   , _jWhitelistSplit    :: !Bool
   , _jIsTopHole         :: !Bool
   , _jGoal              :: !a
+  , j_coercion          :: [(a, a)]
   }
   deriving stock (Eq, Generic, Functor, Show)
 

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