From 1163ae7e00bbdf04891dd5d13e65c967c89a7d47 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 4 Jun 2021 16:50:36 -0700 Subject: [PATCH] Fix unification pertaining to evidence (#1885) * Fix unification pertaining to evidence * Cleanup interface; better names * Need to reapply the substituion after each arg * Reenable error debugging * Add destruct_all evidence test * Fix tests that were accidentally sorted incorrectly Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com> --- .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 3 +- .../src/Wingman/Judgements/Theta.hs | 52 ++++++++++++++----- .../src/Wingman/LanguageServer.hs | 2 +- .../hls-tactics-plugin/src/Wingman/Plugin.hs | 4 +- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 16 +++--- .../test/CodeAction/AutoSpec.hs | 1 + .../test/CodeAction/DestructAllSpec.hs | 1 + .../AutoThetaMultipleUnification.expected.hs | 21 ++++++++ .../golden/AutoThetaMultipleUnification.hs | 21 ++++++++ .../DestructAllGADTEvidence.expected.hs | 21 ++++++++ .../test/golden/DestructAllGADTEvidence.hs | 20 +++++++ .../test/golden/DestructAllMany.expected.hs | 30 +++++------ .../test/golden/MetaMaybeAp.expected.hs | 2 +- 13 files changed, 155 insertions(+), 39 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 11094d08fb..0ed87e3068 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -19,7 +19,6 @@ import Data.Bool (bool) import Data.Functor ((<&>)) import Data.Generics.Labels () import Data.List -import Data.Monoid (Endo(..)) import qualified Data.Set as S import Data.Traversable import DataCon @@ -68,7 +67,7 @@ destructMatches use_field_puns f scrut t jdg = do -- #syn_scoped method_hy = foldMap evidenceToHypothesis ev args = conLikeInstOrigArgTys' con apps - modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev + modify $ evidenceToSubst ev subst <- gets ts_unifier ctx <- ask diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs index de2ef33911..d60526ee5b 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs @@ -12,13 +12,16 @@ module Wingman.Judgements.Theta import Class (classTyVars) import Control.Applicative (empty) +import Control.Lens (preview) import Data.Maybe (fromMaybe, mapMaybe, maybeToList) +import Data.Generics.Sum (_Ctor) 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, empty) -import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst) +import Generics.SYB hiding (tyConName, empty, Generic) +import GHC.Generics +import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst, unionTCvSubst, emptyTCvSubst, TCvSubst) #if __GLASGOW_HASKELL__ > 806 import GhcPlugins (eqTyCon) #else @@ -40,7 +43,7 @@ data Evidence = EqualityOfTypes Type Type -- | We have an instance in scope | HasInstance PredType - deriving (Show) + deriving (Show, Generic) ------------------------------------------------------------------------------ @@ -75,21 +78,46 @@ getEvidenceAtHole (unTrack -> dst) . unTrack ------------------------------------------------------------------------------- --- | Update our knowledge of which types are equal. -evidenceToSubst :: Evidence -> TacticState -> TacticState -evidenceToSubst (EqualityOfTypes a b) ts = +mkSubst :: Set TyVar -> Type -> Type -> TCvSubst +mkSubst skolems a b = let tyvars = S.fromList $ mapMaybe getTyVar_maybe [a, b] -- If we can unify our skolems, at least one is no longer a skolem. -- Removing them from this set ensures we can get a subtitution between -- the two. But it's okay to leave them in 'ts_skolems' in general, since -- they won't exist after running this substitution. - skolems = ts_skolems ts S.\\ tyvars + skolems' = skolems S.\\ tyvars in - case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of - Just subst -> updateSubst subst ts - Nothing -> ts -evidenceToSubst HasInstance{} ts = ts + case tryUnifyUnivarsButNotSkolems skolems' (CType a) (CType b) of + Just subst -> subst + Nothing -> emptyTCvSubst + + +substPair :: TCvSubst -> (Type, Type) -> (Type, Type) +substPair subst (ty, ty') = (substTy subst ty, substTy subst ty') + + +------------------------------------------------------------------------------ +-- | Construct a substitution given a list of types that are equal to one +-- another. This is more subtle than it seems, since there might be several +-- equalities for the same type. We must be careful to push the accumulating +-- substitution through each pair of types before adding their equalities. +allEvidenceToSubst :: Set TyVar -> [(Type, Type)] -> TCvSubst +allEvidenceToSubst _ [] = emptyTCvSubst +allEvidenceToSubst skolems ((a, b) : evs) = + let subst = mkSubst skolems a b + in unionTCvSubst subst + $ allEvidenceToSubst skolems + $ fmap (substPair subst) evs + +------------------------------------------------------------------------------ +-- | 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) + ts ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs index 57888e96dc..3a39beecaf 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs @@ -272,7 +272,7 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm $ hypothesisFromBindings binds_rss binds evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs cls_hy = foldMap evidenceToHypothesis evidence - subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState + subst = ts_unifier $ evidenceToSubst evidence defaultTacticState pure $ ( disallowing AlreadyDestructed already_destructed $ fmap (CType . substTyAddInScope subst . unCType) $ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index 95cb965f7f..6967f5ac5a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -121,7 +121,9 @@ tacticCmd tac pId state (TacticParams uri range var_name) timingOut (cfg_timeout_seconds cfg * seconds) $ join $ case runTactic hj_ctx hj_jdg t of - Left _ -> Left TacticErrors + Left errs -> do + traceMX "errs" errs + Left TacticErrors Right rtr -> case rtr_extract rtr of L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index a076138823..b2d6aafa20 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -11,7 +11,7 @@ import Control.Lens ((&), (%~), (<>~)) import Control.Monad (unless) import Control.Monad.Except (throwError) import Control.Monad.Reader.Class (MonadReader (ask)) -import Control.Monad.State.Strict (StateT(..), runStateT) +import Control.Monad.State.Strict (StateT(..), runStateT, gets) import Data.Bool (bool) import Data.Foldable import Data.Functor ((<&>)) @@ -161,7 +161,7 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do attemptWhen (rule $ destruct' False (\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys g) hi) - (rule $ destruct' False (const subgoal) hi) + (rule $ destruct' False (const newSubgoal) hi) $ case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of (Just (gtc, _), Just (tytc, _)) -> gtc == tytc _ -> False @@ -171,14 +171,14 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do -- | Case split, and leave holes in the matches. destruct :: HyInfo CType -> TacticsM () destruct hi = requireConcreteHole $ tracing "destruct(user)" $ - rule $ destruct' False (const subgoal) hi + rule $ destruct' False (const newSubgoal) hi ------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches. Performs record punning. destructPun :: HyInfo CType -> TacticsM () destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $ - rule $ destruct' True (const subgoal) hi + rule $ destruct' True (const newSubgoal) hi ------------------------------------------------------------------------------ @@ -192,7 +192,7 @@ homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg -> -- | LambdaCase split, and leave holes in the matches. destructLambdaCase :: TacticsM () destructLambdaCase = - tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const subgoal) + tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const newSubgoal) ------------------------------------------------------------------------------ @@ -336,7 +336,7 @@ destructAll :: TacticsM () destructAll = do jdg <- goal let args = fmap fst - $ sort + $ sortOn snd $ mapMaybe (\(hi, prov) -> case prov of TopLevelArgPrv _ idx _ -> pure (hi, idx) @@ -346,7 +346,9 @@ destructAll = do $ filter (isAlgType . unCType . hi_type) $ unHypothesis $ jHypothesis jdg - for_ args destruct + for_ args $ \arg -> do + subst <- gets ts_unifier + destruct $ fmap (coerce substTy subst) arg -------------------------------------------------------------------------------- -- | User-facing tactic to implement "Use constructor " diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs index 5c6b6efff5..bc1b7ef946 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs @@ -65,6 +65,7 @@ spec = do autoTest 6 8 "AutoThetaEqGADTDestruct" autoTest 6 10 "AutoThetaRefl" autoTest 6 8 "AutoThetaReflDestruct" + autoTest 19 30 "AutoThetaMultipleUnification" describe "known" $ do autoTest 25 13 "GoldenArbitrary" diff --git a/plugins/hls-tactics-plugin/test/CodeAction/DestructAllSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/DestructAllSpec.hs index 89579f7ba9..488fb3ebad 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/DestructAllSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/DestructAllSpec.hs @@ -34,4 +34,5 @@ spec = do destructAllTest 4 23 "DestructAllMany" destructAllTest 2 18 "DestructAllNonVarTopMatch" destructAllTest 2 18 "DestructAllFunc" + destructAllTest 19 18 "DestructAllGADTEvidence" diff --git a/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.expected.hs b/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.expected.hs new file mode 100644 index 0000000000..446a4d73b3 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.expected.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +import Data.Kind + +data Nat = Z | S Nat + +data HList (ls :: [Type]) where + HNil :: HList '[] + HCons :: t -> HList ts -> HList (t ': ts) + +data ElemAt (n :: Nat) t (ts :: [Type]) where + AtZ :: ElemAt 'Z t (t ': ts) + AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts) + +lookMeUp :: ElemAt i ty tys -> HList tys -> ty +lookMeUp AtZ (HCons t _) = t +lookMeUp (AtS ea') (HCons t hl') = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.hs b/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.hs new file mode 100644 index 0000000000..b0b520347d --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +import Data.Kind + +data Nat = Z | S Nat + +data HList (ls :: [Type]) where + HNil :: HList '[] + HCons :: t -> HList ts -> HList (t ': ts) + +data ElemAt (n :: Nat) t (ts :: [Type]) where + AtZ :: ElemAt 'Z t (t ': ts) + AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts) + +lookMeUp :: ElemAt i ty tys -> HList tys -> ty +lookMeUp AtZ (HCons t hl') = _ +lookMeUp (AtS ea') (HCons t hl') = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs new file mode 100644 index 0000000000..b0b520347d --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +import Data.Kind + +data Nat = Z | S Nat + +data HList (ls :: [Type]) where + HNil :: HList '[] + HCons :: t -> HList ts -> HList (t ': ts) + +data ElemAt (n :: Nat) t (ts :: [Type]) where + AtZ :: ElemAt 'Z t (t ': ts) + AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts) + +lookMeUp :: ElemAt i ty tys -> HList tys -> ty +lookMeUp AtZ (HCons t hl') = _ +lookMeUp (AtS ea') (HCons t hl') = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.hs new file mode 100644 index 0000000000..3ac66d5444 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +import Data.Kind + +data Nat = Z | S Nat + +data HList (ls :: [Type]) where + HNil :: HList '[] + HCons :: t -> HList ts -> HList (t ': ts) + +data ElemAt (n :: Nat) t (ts :: [Type]) where + AtZ :: ElemAt 'Z t (t ': ts) + AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts) + +lookMeUp :: ElemAt i ty tys -> HList tys -> ty +lookMeUp ea hl = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs index 27e3c93ae0..c443ed795e 100644 --- a/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs @@ -2,26 +2,26 @@ data ABC = A | B | C many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> () many () (Left a) False Nothing A = _ -many () (Left a) False (Just abc') A = _ -many () (Right b') False Nothing A = _ -many () (Right b') False (Just abc') A = _ -many () (Left a) True Nothing A = _ -many () (Left a) True (Just abc') A = _ -many () (Right b') True Nothing A = _ -many () (Right b') True (Just abc') A = _ many () (Left a) False Nothing B = _ +many () (Left a) False Nothing C = _ +many () (Left a) False (Just abc') A = _ many () (Left a) False (Just abc') B = _ -many () (Right b') False Nothing B = _ -many () (Right b') False (Just abc') B = _ +many () (Left a) False (Just abc') C = _ +many () (Left a) True Nothing A = _ many () (Left a) True Nothing B = _ +many () (Left a) True Nothing C = _ +many () (Left a) True (Just abc') A = _ many () (Left a) True (Just abc') B = _ -many () (Right b') True Nothing B = _ -many () (Right b') True (Just abc') B = _ -many () (Left a) False Nothing C = _ -many () (Left a) False (Just abc') C = _ +many () (Left a) True (Just abc') C = _ +many () (Right b') False Nothing A = _ +many () (Right b') False Nothing B = _ many () (Right b') False Nothing C = _ +many () (Right b') False (Just abc') A = _ +many () (Right b') False (Just abc') B = _ many () (Right b') False (Just abc') C = _ -many () (Left a) True Nothing C = _ -many () (Left a) True (Just abc') C = _ +many () (Right b') True Nothing A = _ +many () (Right b') True Nothing B = _ many () (Right b') True Nothing C = _ +many () (Right b') True (Just abc') A = _ +many () (Right b') True (Just abc') B = _ many () (Right b') True (Just abc') C = _ diff --git a/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.expected.hs index 8e40c9fa3f..e0b60b74fa 100644 --- a/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.expected.hs +++ b/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.expected.hs @@ -1,5 +1,5 @@ maybeAp :: Maybe (a -> b) -> Maybe a -> Maybe b maybeAp Nothing Nothing = Nothing -maybeAp (Just _) Nothing = Nothing maybeAp Nothing (Just _) = Nothing +maybeAp (Just _) Nothing = Nothing maybeAp (Just fab) (Just a) = Just (fab a)