From a56067a680166d10dfbf22f2622d9ff09cd851fa Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 17 Jun 2021 14:03:23 -0700 Subject: [PATCH 1/3] Properly scope GADT equality evidence in the judgment Fixes #1937 --- plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs | 4 +--- .../hls-tactics-plugin/src/Wingman/Judgements.hs | 5 +++++ .../src/Wingman/Judgements/Theta.hs | 8 ++++++++ plugins/hls-tactics-plugin/src/Wingman/Machinery.hs | 5 ++++- plugins/hls-tactics-plugin/src/Wingman/Types.hs | 1 + .../test/CodeAction/RunMetaprogramSpec.hs | 2 +- .../test/golden/MetaCataAST.expected.hs | 13 +------------ .../hls-tactics-plugin/test/golden/MetaCataAST.hs | 11 ----------- 8 files changed, 21 insertions(+), 28 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 0944b99ed7..478f5e41c0 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs index ae2c053e9c..7dd27450a5 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs +++ b/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 } diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs index 622eb4584f..a60fc96542 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index ec078a210e..b7ea036404 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index df61ba50d5..f6d7129694 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/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) diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs index 36eb56f00a..e6ec079562 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs +++ b/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" diff --git a/plugins/hls-tactics-plugin/test/golden/MetaCataAST.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaCataAST.expected.hs index 4b41db7867..d0597676d2 100644 --- a/plugins/hls-tactics-plugin/test/golden/MetaCataAST.expected.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/test/golden/MetaCataAST.hs b/plugins/hls-tactics-plugin/test/golden/MetaCataAST.hs index 7eb7f00c8d..26e3a03cec 100644 --- a/plugins/hls-tactics-plugin/test/golden/MetaCataAST.hs +++ b/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 |] From 1e0458a6aa0c20b0d01bef7e30e3ac0b457bb3ce Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 17 Jun 2021 14:08:54 -0700 Subject: [PATCH 2/3] Haddock and a bit of refactoring --- plugins/hls-tactics-plugin/src/Wingman/Judgements.hs | 2 ++ plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs | 6 ++---- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs index 7dd27450a5..bf614104fa 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs @@ -69,6 +69,8 @@ withNewGoal :: a -> Judgement' a -> Judgement' a withNewGoal t = field @"_jGoal" .~ t +------------------------------------------------------------------------------ +-- | Add some new type equalities to the local judgement. withNewCoercions :: [(a, a)] -> Judgement' a -> Judgement' a withNewCoercions ev = field @"j_coercion" <>~ ev diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs index a60fc96542..21b16edbc4 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs @@ -113,7 +113,7 @@ allEvidenceToSubst skolems ((a, b) : evs) = $ fmap (substPair subst) evs ------------------------------------------------------------------------------ --- | Update our knowledge of which types are equal. +-- | Given some 'Evidence', get a list of which types are now equal. evidenceToCoercions :: [Evidence] -> [(CType, CType)] evidenceToCoercions = coerce . mapMaybe (preview $ _Ctor @"EqualityOfTypes") @@ -122,9 +122,7 @@ evidenceToCoercions = coerce . mapMaybe (preview $ _Ctor @"EqualityOfTypes") 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 From 8ed877d849b2d0c53906707ac8d95ee61583f41c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 17 Jun 2021 20:14:20 -0700 Subject: [PATCH 3/3] Track coercions in a TCvSubst instead --- .../src/Wingman/Judgements.hs | 10 +++++++--- .../src/Wingman/Machinery.hs | 18 +++++++++++++----- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 8 ++++++-- .../hls-tactics-plugin/src/Wingman/Types.hs | 5 ++--- 4 files changed, 28 insertions(+), 13 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs index bf614104fa..91ffd3743d 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs +++ b/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 @@ -71,8 +72,11 @@ withNewGoal t = field @"_jGoal" .~ t ------------------------------------------------------------------------------ -- | Add some new type equalities to the local judgement. -withNewCoercions :: [(a, a)] -> Judgement' a -> Judgement' a -withNewCoercions ev = field @"j_coercion" <>~ ev +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 @@ -420,7 +424,7 @@ mkFirstJudgement ctx hy top goal = , _jWhitelistSplit = True , _jIsTopHole = top , _jGoal = CType goal - , j_coercion = mempty + , j_coercion = emptyTCvSubst } diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index b7ea036404..d581c70100 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -32,7 +32,6 @@ 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 @@ -41,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. @@ -49,12 +59,10 @@ newSubgoal -> Rule newSubgoal j = do ctx <- ask - skolems <- gets ts_skolems - let coercions = allEvidenceToSubst skolems $ coerce $ j_coercion j - unifier <- gets ts_unifier + unifier <- getSubstForJudgement j subgoal $ normalizeJudgement ctx - $ substJdg (unionTCvSubst unifier coercions) + $ substJdg unifier $ unsetIsTopHole $ normalizeJudgement ctx j diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 95d79c1913..be831c4287 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/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 -------------------------------------------------------------------------------- diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index f6d7129694..758d3e408c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs @@ -297,9 +297,9 @@ data Judgement' a = Judgement , _jWhitelistSplit :: !Bool , _jIsTopHole :: !Bool , _jGoal :: !a - , j_coercion :: [(a, a)] + , j_coercion :: TCvSubst } - deriving stock (Eq, Generic, Functor, Show) + deriving stock (Generic, Functor, Show) type Judgement = Judgement' CType @@ -329,7 +329,6 @@ data TacticError | TooPolymorphic | NotInScope OccName | TacticPanic String - deriving stock (Eq) instance Show TacticError where show (UndefinedHypothesis name) =