From 48100aced7ecca30987dbfd189b6b810820fc5d1 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 8 Sep 2021 11:53:07 -0500 Subject: [PATCH 1/9] Correctly track skolems when reasoning about GADT constructors --- .../src/Wingman/AbstractLSP/TacticActions.hs | 1 - .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 9 ++-- .../src/Wingman/EmptyCase.hs | 8 ++- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 51 ++++++++++++++++--- .../src/Wingman/Judgements.hs | 15 ++++++ .../Wingman/LanguageServer/TacticProviders.hs | 27 +++++++--- .../src/Wingman/Machinery.hs | 19 +++---- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 14 +++-- 8 files changed, 105 insertions(+), 39 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs index 89769ae8aa..239128db6e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs @@ -17,7 +17,6 @@ import Development.IDE.GHC.Compat import Development.IDE.GHC.ExactPrint import Generics.SYB.GHC (mkBindListT, everywhereM') import GhcPlugins (occName) -import System.Timeout (timeout) import Wingman.AbstractLSP.Types import Wingman.CaseSplit import Wingman.GHC (liftMaybe, isHole, pattern AMatch, unXPat) diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 07b112e01a..a7929a6157 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -59,7 +59,8 @@ destructMatches destructMatches use_field_puns f scrut t jdg = do let hy = jEntireHypothesis jdg g = jGoal jdg - case tacticsGetDataCons $ unCType t of + skolems <- gets ts_skolems + case tacticsGetDataCons skolems $ unCType t of Nothing -> cut -- throwError $ GoalMismatch "destruct" g Just (dcs, apps) -> fmap unzipTrace $ for dcs $ \dc -> do @@ -93,11 +94,11 @@ destructMatches use_field_puns f scrut t jdg = do ------------------------------------------------------------------------------ -- | Generate just the 'Match'es for a case split on a specific type. -destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)] +destructionFor :: S.Set TyVar -> Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)] -- TODO(sandy): In an ideal world, this would be the same codepath as -- 'destructMatches'. Make sure to change that if you ever change this. -destructionFor hy t = do - case tacticsGetDataCons t of +destructionFor skolems hy t = do + case tacticsGetDataCons skolems t of Nothing -> Nothing Just ([], _) -> Nothing Just (dcs, apps) -> do diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs index 93deee4e3a..323eb1600a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs @@ -68,7 +68,9 @@ emptyCaseInteraction = Interaction $ range = realSrcSpanToRange $ unTrack ss matches <- liftMaybe $ - destructionFor + -- TODO(sandy): This needs a judgment in order to correctly compute + -- the skolems! But we don't have a judgement yet :( + destructionFor mempty (foldMap (hySingleton . occName . fst) bindings) ty edits <- liftMaybe $ hush $ @@ -149,7 +151,9 @@ emptyCaseScrutinees state nfp = do . fmap (scrutinzedType <=< sequence) . traverse (typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg') $ scrutinee - case null $ tacticsGetDataCons ty of + -- TODO(sandy): This needs a judgment in order to correctly compute the + -- skolems! But we don't have a judgement yet :( + case null $ tacticsGetDataCons mempty ty of True -> pure empty False -> case ss of diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index f3b82f9835..45cd61d6f2 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -28,6 +28,7 @@ import GHC.SourceGen (lambda) import Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT) import GhcPlugins (Role (Nominal)) import OccName +import PrelNames (eqTyConKey, heqTyConKey) import TcRnMonad import TcType import TyCoRep @@ -90,17 +91,50 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta, _)) = theta ------------------------------------------------------------------------------ -- | Get the data cons of a type, if it has any. -tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type]) -tacticsGetDataCons ty +tacticsGetDataCons :: Set TyVar -> Type -> Maybe ([DataCon], [Type]) +tacticsGetDataCons skolems ty | Just (_, ty') <- tcSplitForAllTy_maybe ty - = tacticsGetDataCons ty' -tacticsGetDataCons ty + = tacticsGetDataCons skolems ty' +tacticsGetDataCons skolems ty | Just _ <- algebraicTyCon ty = splitTyConApp_maybe ty <&> \(tc, apps) -> - ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc + ( filter (not . tacticsDataConCantMatch skolems apps) $ tyConDataCons tc , apps ) -tacticsGetDataCons _ = Nothing +tacticsGetDataCons _ _ = Nothing + + +------------------------------------------------------------------------------ +-- | Directly ripped from GHC; minor changes to allow for skolems. +tacticsDataConCantMatch :: Set TyVar -> [Type] -> DataCon -> Bool +-- Returns True iff the data con *definitely cannot* match a +-- scrutinee of type (T tys) +-- where T is the dcRepTyCon for the data con +tacticsDataConCantMatch skolems tys con + | null inst_theta = False -- Common + | all isTyVarTy tys = False -- Also common + | otherwise = typesCantMatch (concatMap predEqs inst_theta) + where + (_, inst_theta, _) = dataConInstSig con tys + + -- TODO: could gather equalities from superclasses too + predEqs pred = case classifyPredType pred of + EqPred NomEq ty1 ty2 -> [(ty1, ty2)] + ClassPred eq args + | eq `hasKey` eqTyConKey + , [_, ty1, ty2] <- args -> [(ty1, ty2)] + | eq `hasKey` heqTyConKey + , [_, _, ty1, ty2] <- args -> [(ty1, ty2)] + _ -> [] + + typesCantMatch :: [(Type,Type)] -> Bool + -- See Note [Pruning dead case alternatives] + typesCantMatch prs = any (uncurry cant_match) prs + where + cant_match :: Type -> Type -> Bool + cant_match t1 t2 = case tcUnifyTysFG (isSkolem skolems) [t1] [t2] of + SurelyApart -> True + _ -> False ------------------------------------------------------------------------------ -- | Instantiate all of the quantified type variables in a type with fresh @@ -378,12 +412,15 @@ expandTyFam :: Context -> Type -> Type expandTyFam ctx = snd . normaliseType (ctxFamInstEnvs ctx) Nominal +isSkolem :: Set TyVar -> TyVar -> BindFlag +isSkolem skolems = bool BindMe Skolem . flip S.member skolems + ------------------------------------------------------------------------------ -- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of. tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst tryUnifyUnivarsButNotSkolems skolems goal inst = case tcUnifyTysFG - (bool BindMe Skolem . flip S.member skolems) + (isSkolem skolems) [unCType inst] [unCType goal] of Unifiable subst -> pure subst diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs index 21c1e609a8..569b11be38 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs @@ -6,6 +6,7 @@ import Control.Lens hiding (Context) import Data.Bool import Data.Char import Data.Coerce +import Data.Foldable (toList) import Data.Generics.Product (field) import Data.Map (Map) import qualified Data.Map as M @@ -473,3 +474,17 @@ isAlreadyDestructed _ = False expandDisallowed :: Provenance -> Provenance expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv expandDisallowed prv = prv + + +------------------------------------------------------------------------------ +-- | Compute the skolems in scope for a given judgement. +skolemsForJudgment :: Judgement -> Set TyVar +skolemsForJudgment jdg + = S.fromList + $ foldMap (tyCoVarsOfTypeWellScoped . unCType) + $ (:) (jGoal jdg) + $ fmap hi_type + $ toList + $ hyByName + $ jHypothesis jdg + diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index 5a0844b73c..de10a74518 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -118,7 +118,8 @@ commandProvider DestructPun = provide DestructPun $ T.pack $ occNameString occ commandProvider Homomorphism = requireHoleSort (== Hole) $ - filterBindingType homoFilter $ \occ _ -> + withSkolems $ \skolems -> + filterBindingType (homoFilter skolems) $ \occ _ -> provide Homomorphism $ T.pack $ occNameString occ commandProvider DestructLambdaCase = requireHoleSort (== Hole) $ @@ -128,7 +129,8 @@ commandProvider DestructLambdaCase = commandProvider HomomorphismLambdaCase = requireHoleSort (== Hole) $ requireExtension LambdaCase $ - filterGoalType (liftLambdaCase False homoFilter) $ + withSkolems $ \skolems -> + filterGoalType (liftLambdaCase False $ homoFilter skolems) $ provide HomomorphismLambdaCase "" commandProvider DestructAll = requireHoleSort (== Hole) $ @@ -138,12 +140,13 @@ commandProvider DestructAll = False -> mempty commandProvider UseDataCon = requireHoleSort (== Hole) $ + withSkolems $ \skolems -> withConfig $ \cfg -> filterTypeProjection ( guardLength (<= cfg_max_use_ctor_actions cfg) . fromMaybe [] . fmap fst - . tacticsGetDataCons + . tacticsGetDataCons skolems ) $ \dcon -> provide UseDataCon . T.pack @@ -266,7 +269,17 @@ filterTypeProjection p tp tpd = ------------------------------------------------------------------------------ -- | Get access to the 'Config' when building a 'TacticProvider'. withConfig :: (Config -> TacticProvider) -> TacticProvider -withConfig tp tpd = tp (le_config $ tpd_lspEnv tpd) tpd +withConfig = withs $ le_config . tpd_lspEnv + + +withSkolems :: (S.Set TyVar -> TacticProvider) -> TacticProvider +withSkolems = withs $ skolemsForJudgment . tpd_jdg + + +------------------------------------------------------------------------------ +-- | Use something from the TPD to construct a 'TacticProvider'. +withs :: (TacticProviderData -> a) -> (a -> TacticProvider) -> TacticProvider +withs f tp tpd = tp (f tpd) tpd ------------------------------------------------------------------------------ @@ -286,9 +299,9 @@ tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" ------------------------------------------------------------------------------ -- | We should show homos only when the goal type is the same as the binding -- type, and that both are usual algebraic types. -homoFilter :: Type -> Type -> Bool -homoFilter codomain domain = - case uncoveredDataCons domain codomain of +homoFilter :: S.Set TyVar -> Type -> Type -> Bool +homoFilter skolems codomain domain = + case uncoveredDataCons skolems domain codomain of Just s -> S.null s _ -> False diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 0cebec94b7..bf0641d9fe 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -93,16 +93,9 @@ runTactic -> TacticsM () -- ^ Tactic to use -> IO (Either [TacticError] RunTacticResults) runTactic duration ctx jdg t = do - let skolems = S.fromList - $ foldMap (tyCoVarsOfTypeWellScoped . unCType) - $ (:) (jGoal jdg) - $ fmap hi_type - $ toList - $ hyByName - $ jHypothesis jdg - tacticState = + let tacticState = defaultTacticState - { ts_skolems = skolems + { ts_skolems = skolemsForJudgment jdg } let stream = hoistListT (flip runReaderT ctx . unExtractM) @@ -414,9 +407,9 @@ getCurrentDefinitions = do -- data constructor in the domain to the same in the codomain. This function -- returns 'Just' when all the lookups succeeded, and a non-empty value if the -- homomorphism *is not* possible. -uncoveredDataCons :: Type -> Type -> Maybe (S.Set (Uniquely DataCon)) -uncoveredDataCons domain codomain = do - (g_dcs, _) <- tacticsGetDataCons codomain - (hi_dcs, _) <- tacticsGetDataCons domain +uncoveredDataCons :: S.Set TyVar -> Type -> Type -> Maybe (S.Set (Uniquely DataCon)) +uncoveredDataCons skolems domain codomain = do + (g_dcs, _) <- tacticsGetDataCons skolems codomain + (hi_dcs, _) <- tacticsGetDataCons skolems domain pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 9075acb3b0..d865672ab2 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 (filterM) import Control.Monad (unless) import Control.Monad.Extra (anyM) 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 ((<&>)) @@ -236,10 +236,11 @@ homo :: HyInfo CType -> TacticsM () homo hi = requireConcreteHole . tracing "homo" $ do jdg <- goal let g = jGoal jdg + skolems <- gets ts_skolems -- Ensure that every data constructor in the domain type is covered in the -- codomain; otherwise 'homo' will produce an ill-typed program. - case (uncoveredDataCons (coerce $ hi_type hi) (coerce g)) of + case (uncoveredDataCons skolems (coerce $ hi_type hi) (coerce g)) of Just uncovered_dcs -> unless (S.null uncovered_dcs) $ failure $ TacticPanic "Can't cover every datacon in domain" @@ -313,7 +314,8 @@ split :: TacticsM () split = tracing "split(user)" $ do jdg <- goal let g = jGoal jdg - case tacticsGetDataCons $ unCType g of + skolems <- gets ts_skolems + case tacticsGetDataCons skolems $ unCType g of Nothing -> failure $ GoalMismatch "split" g Just (dcs, _) -> choice $ fmap splitDataCon dcs @@ -326,7 +328,8 @@ splitAuto :: TacticsM () splitAuto = requireConcreteHole $ tracing "split(auto)" $ do jdg <- goal let g = jGoal jdg - case tacticsGetDataCons $ unCType g of + skolems <- gets ts_skolems + case tacticsGetDataCons skolems $ unCType g of Nothing -> failure $ GoalMismatch "split" g Just (dcs, _) -> do case isSplitWhitelisted jdg of @@ -343,7 +346,8 @@ splitSingle :: TacticsM () splitSingle = tracing "splitSingle" $ do jdg <- goal let g = jGoal jdg - case tacticsGetDataCons $ unCType g of + skolems <- gets ts_skolems + case tacticsGetDataCons skolems $ unCType g of Just ([dc], _) -> do splitDataCon dc _ -> failure $ GoalMismatch "splitSingle" g From 1f227d055d8af96313b408972a22b86db87280d3 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 8 Sep 2021 12:17:12 -0500 Subject: [PATCH 2/9] If it's maybe apart, it's definitely apart --- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index 45cd61d6f2..3813c5a40e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -112,7 +112,6 @@ tacticsDataConCantMatch :: Set TyVar -> [Type] -> DataCon -> Bool -- where T is the dcRepTyCon for the data con tacticsDataConCantMatch skolems tys con | null inst_theta = False -- Common - | all isTyVarTy tys = False -- Also common | otherwise = typesCantMatch (concatMap predEqs inst_theta) where (_, inst_theta, _) = dataConInstSig con tys @@ -134,7 +133,9 @@ tacticsDataConCantMatch skolems tys con cant_match :: Type -> Type -> Bool cant_match t1 t2 = case tcUnifyTysFG (isSkolem skolems) [t1] [t2] of SurelyApart -> True - _ -> False + -- Still contains skolems, so it's actually surely apart. + MaybeApart _ -> True + Unifiable _ -> False ------------------------------------------------------------------------------ -- | Instantiate all of the quantified type variables in a type with fresh From 6f9942eb855f62a338240ecaa20ce30ecef08928 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 8 Sep 2021 12:17:39 -0500 Subject: [PATCH 3/9] Add a test --- plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs | 1 + .../test/golden/MessageRespectGADTSkolem.hs | 8 ++++++++ 2 files changed, 9 insertions(+) create mode 100644 plugins/hls-tactics-plugin/test/golden/MessageRespectGADTSkolem.hs diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs index cc97666a2a..fcef99ec26 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs @@ -88,4 +88,5 @@ spec = do mkShowMessageTest Auto "" 2 8 "MessageForallA" TacticErrors mkShowMessageTest Auto "" 7 8 "MessageCantUnify" TacticErrors mkShowMessageTest Auto "" 12 8 "MessageNotEnoughGas" NotEnoughGas + mkShowMessageTest Auto "" 7 8 "MessageRespectGADTSkolem" TacticErrors diff --git a/plugins/hls-tactics-plugin/test/golden/MessageRespectGADTSkolem.hs b/plugins/hls-tactics-plugin/test/golden/MessageRespectGADTSkolem.hs new file mode 100644 index 0000000000..1096bb1a6f --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MessageRespectGADTSkolem.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE GADTs #-} + +data Foo a where + Foo :: Foo Int + +test :: Foo as +test = _ + From ce7bda41c2c4225913fac9a30bf3c62a66cc938c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 9 Sep 2021 11:54:41 -0500 Subject: [PATCH 4/9] EqPred has moved on us! --- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index 3813c5a40e..1b698d85c3 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -40,6 +40,10 @@ import Var import Wingman.StaticPlugin (pattern MetaprogramSyntax) import Wingman.Types +#if __GLASGOW_HASKELL__ >= 810 +import GHC.Core.Predicate +#endif + tcTyVar_maybe :: Type -> Maybe Var tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty' @@ -126,6 +130,7 @@ tacticsDataConCantMatch skolems tys con , [_, _, ty1, ty2] <- args -> [(ty1, ty2)] _ -> [] + typesCantMatch :: [(Type,Type)] -> Bool -- See Note [Pruning dead case alternatives] typesCantMatch prs = any (uncurry cant_match) prs From 550001ea7a826d352846223ec934f3df0fb77083 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 9 Sep 2021 13:15:30 -0500 Subject: [PATCH 5/9] Predicate is slippery --- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index 1b698d85c3..fdaf1251cb 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -40,9 +40,11 @@ import Var import Wingman.StaticPlugin (pattern MetaprogramSyntax) import Wingman.Types -#if __GLASGOW_HASKELL__ >= 810 +#if __GLASGOW_HASKELL__ == 810 +import Predicate +#elif __GLASGOW_HASKELL__ >= 900 import GHC.Core.Predicate -#endif +#end tcTyVar_maybe :: Type -> Maybe Var From 43a7b14145326a885fd57a92e97a548218cdfa7a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 9 Sep 2021 17:19:24 -0500 Subject: [PATCH 6/9] I'm bad at CPP --- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index fdaf1251cb..e1c2db4ca0 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -44,7 +44,7 @@ import Wingman.Types import Predicate #elif __GLASGOW_HASKELL__ >= 900 import GHC.Core.Predicate -#end +#endif tcTyVar_maybe :: Type -> Maybe Var From 7a32a9c40df49cabc516177e4a1030fff0752b73 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sat, 11 Sep 2021 10:33:54 -0500 Subject: [PATCH 7/9] We need to track if we're de/constructing a term --- .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 4 +-- .../src/Wingman/EmptyCase.hs | 2 +- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 28 ++++++++++++------- .../Wingman/LanguageServer/TacticProviders.hs | 2 +- .../src/Wingman/Machinery.hs | 6 ++-- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 6 ++-- 6 files changed, 28 insertions(+), 20 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index a7929a6157..b95299d7ee 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -60,7 +60,7 @@ destructMatches use_field_puns f scrut t jdg = do let hy = jEntireHypothesis jdg g = jGoal jdg skolems <- gets ts_skolems - case tacticsGetDataCons skolems $ unCType t of + case tacticsGetDataCons Destruction skolems $ unCType t of Nothing -> cut -- throwError $ GoalMismatch "destruct" g Just (dcs, apps) -> fmap unzipTrace $ for dcs $ \dc -> do @@ -98,7 +98,7 @@ destructionFor :: S.Set TyVar -> Hypothesis a -> Type -> Maybe [LMatch GhcPs (LH -- TODO(sandy): In an ideal world, this would be the same codepath as -- 'destructMatches'. Make sure to change that if you ever change this. destructionFor skolems hy t = do - case tacticsGetDataCons skolems t of + case tacticsGetDataCons Destruction skolems t of Nothing -> Nothing Just ([], _) -> Nothing Just (dcs, apps) -> do diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs index 323eb1600a..9cef94b6a5 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs @@ -153,7 +153,7 @@ emptyCaseScrutinees state nfp = do $ scrutinee -- TODO(sandy): This needs a judgment in order to correctly compute the -- skolems! But we don't have a judgement yet :( - case null $ tacticsGetDataCons mempty ty of + case null $ tacticsGetDataCons Destruction mempty ty of True -> pure empty False -> case ss of diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index e1c2db4ca0..028fa9a86d 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -97,26 +97,29 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta, _)) = theta ------------------------------------------------------------------------------ -- | Get the data cons of a type, if it has any. -tacticsGetDataCons :: Set TyVar -> Type -> Maybe ([DataCon], [Type]) -tacticsGetDataCons skolems ty +tacticsGetDataCons :: DataConMatchMode -> Set TyVar -> Type -> Maybe ([DataCon], [Type]) +tacticsGetDataCons mm skolems ty | Just (_, ty') <- tcSplitForAllTy_maybe ty - = tacticsGetDataCons skolems ty' -tacticsGetDataCons skolems ty + = tacticsGetDataCons mm skolems ty' +tacticsGetDataCons mm skolems ty | Just _ <- algebraicTyCon ty = splitTyConApp_maybe ty <&> \(tc, apps) -> - ( filter (not . tacticsDataConCantMatch skolems apps) $ tyConDataCons tc + ( filter (not . tacticsDataConCantMatch mm skolems apps) $ tyConDataCons tc , apps ) -tacticsGetDataCons _ _ = Nothing +tacticsGetDataCons _ _ _ = Nothing +data DataConMatchMode = Construction | Destruction + deriving (Eq, Ord, Show, Enum, Bounded) + ------------------------------------------------------------------------------ -- | Directly ripped from GHC; minor changes to allow for skolems. -tacticsDataConCantMatch :: Set TyVar -> [Type] -> DataCon -> Bool +tacticsDataConCantMatch :: DataConMatchMode -> Set TyVar -> [Type] -> DataCon -> Bool -- Returns True iff the data con *definitely cannot* match a -- scrutinee of type (T tys) -- where T is the dcRepTyCon for the data con -tacticsDataConCantMatch skolems tys con +tacticsDataConCantMatch mm skolems tys con | null inst_theta = False -- Common | otherwise = typesCantMatch (concatMap predEqs inst_theta) where @@ -140,8 +143,13 @@ tacticsDataConCantMatch skolems tys con cant_match :: Type -> Type -> Bool cant_match t1 t2 = case tcUnifyTysFG (isSkolem skolems) [t1] [t2] of SurelyApart -> True - -- Still contains skolems, so it's actually surely apart. - MaybeApart _ -> True + MaybeApart _ -> + -- TODO(sandy): I don't know if ths logic is reasonable. + -- I experimented until the tests went green, but I have to admit + -- it's hella suspicious. + case mm of + Construction -> True + Destruction -> False Unifiable _ -> False ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index de10a74518..6c2fbb4b22 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -146,7 +146,7 @@ commandProvider UseDataCon = ( guardLength (<= cfg_max_use_ctor_actions cfg) . fromMaybe [] . fmap fst - . tacticsGetDataCons skolems + . tacticsGetDataCons Construction skolems ) $ \dcon -> provide UseDataCon . T.pack diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index bf0641d9fe..f3b021ef8b 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -34,7 +34,7 @@ import System.Timeout (timeout) import TcType import Type (tyCoVarsOfTypeWellScoped) import Wingman.Context (getInstance) -import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons) +import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, DataConMatchMode(..)) import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types @@ -409,7 +409,7 @@ getCurrentDefinitions = do -- homomorphism *is not* possible. uncoveredDataCons :: S.Set TyVar -> Type -> Type -> Maybe (S.Set (Uniquely DataCon)) uncoveredDataCons skolems domain codomain = do - (g_dcs, _) <- tacticsGetDataCons skolems codomain - (hi_dcs, _) <- tacticsGetDataCons skolems domain + (g_dcs, _) <- tacticsGetDataCons Destruction skolems codomain + (hi_dcs, _) <- tacticsGetDataCons Destruction skolems domain pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index d865672ab2..0300bf75fd 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -315,7 +315,7 @@ split = tracing "split(user)" $ do jdg <- goal let g = jGoal jdg skolems <- gets ts_skolems - case tacticsGetDataCons skolems $ unCType g of + case tacticsGetDataCons Construction skolems $ unCType g of Nothing -> failure $ GoalMismatch "split" g Just (dcs, _) -> choice $ fmap splitDataCon dcs @@ -329,7 +329,7 @@ splitAuto = requireConcreteHole $ tracing "split(auto)" $ do jdg <- goal let g = jGoal jdg skolems <- gets ts_skolems - case tacticsGetDataCons skolems $ unCType g of + case tacticsGetDataCons Construction skolems $ unCType g of Nothing -> failure $ GoalMismatch "split" g Just (dcs, _) -> do case isSplitWhitelisted jdg of @@ -347,7 +347,7 @@ splitSingle = tracing "splitSingle" $ do jdg <- goal let g = jGoal jdg skolems <- gets ts_skolems - case tacticsGetDataCons skolems $ unCType g of + case tacticsGetDataCons Construction skolems $ unCType g of Just ([dc], _) -> do splitDataCon dc _ -> failure $ GoalMismatch "splitSingle" g From 49ffcf363c4cb7ba378bb905e3fc2ecd209f8619 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sat, 11 Sep 2021 12:05:36 -0500 Subject: [PATCH 8/9] Fix a bug in homomorphic coverage; make sure to use it in destructAutoOrHomo --- plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs | 1 + .../src/Wingman/LanguageServer/TacticProviders.hs | 6 ++---- plugins/hls-tactics-plugin/src/Wingman/Machinery.hs | 10 ++++++---- plugins/hls-tactics-plugin/src/Wingman/Tactics.hs | 8 +++++--- 4 files changed, 14 insertions(+), 11 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index b95299d7ee..44cfb6f6c7 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -218,6 +218,7 @@ destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement destruct' use_field_puns f hi jdg = do when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic let term = hi_name hi + -- TODO(sandy): THIS NEEDS TO INTRODUCE SKOLEMS TOO ext <- destructMatches use_field_puns diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index 6c2fbb4b22..c62361d4e5 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -27,7 +27,7 @@ import Wingman.AbstractLSP.Types import Wingman.Auto import Wingman.GHC import Wingman.Judgements -import Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons) +import Wingman.Machinery (useNameFromHypothesis, allDataConsAreCovered) import Wingman.Metaprogramming.Parser (parseMetaprogram) import Wingman.Tactics import Wingman.Types @@ -301,9 +301,7 @@ tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" -- type, and that both are usual algebraic types. homoFilter :: S.Set TyVar -> Type -> Type -> Bool homoFilter skolems codomain domain = - case uncoveredDataCons skolems domain codomain of - Just s -> S.null s - _ -> False + maybe False id $ allDataConsAreCovered skolems domain codomain ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index f3b021ef8b..9c1b7e2cef 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -407,9 +407,11 @@ getCurrentDefinitions = do -- data constructor in the domain to the same in the codomain. This function -- returns 'Just' when all the lookups succeeded, and a non-empty value if the -- homomorphism *is not* possible. -uncoveredDataCons :: S.Set TyVar -> Type -> Type -> Maybe (S.Set (Uniquely DataCon)) -uncoveredDataCons skolems domain codomain = do +allDataConsAreCovered :: S.Set TyVar -> Type -> Type -> Maybe Bool +allDataConsAreCovered skolems domain codomain = do (g_dcs, _) <- tacticsGetDataCons Destruction skolems codomain - (hi_dcs, _) <- tacticsGetDataCons Destruction skolems domain - pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs) + (hi_dcs, _) <- tacticsGetDataCons Construction skolems domain + let constructable = S.fromList (coerce hi_dcs) + destructable = S.fromList (coerce g_dcs) + pure $ S.isSubsetOf @(Uniquely DataCon) destructable constructable diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 0300bf75fd..003ecd0f99 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -204,6 +204,7 @@ destructAuto hi = requireConcreteHole $ tracing "destruct(auto)" $ do destructOrHomoAuto :: HyInfo CType -> TacticsM () destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do jdg <- goal + skolems <- gets ts_skolems let g = unCType $ jGoal jdg ty = unCType $ hi_type hi @@ -213,6 +214,7 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do (rule $ destruct' False (const newSubgoal) hi) $ case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of (Just (gtc, _), Just (tytc, _)) -> gtc == tytc + && (maybe False id $ allDataConsAreCovered skolems ty g) _ -> False @@ -240,9 +242,9 @@ homo hi = requireConcreteHole . tracing "homo" $ do -- Ensure that every data constructor in the domain type is covered in the -- codomain; otherwise 'homo' will produce an ill-typed program. - case (uncoveredDataCons skolems (coerce $ hi_type hi) (coerce g)) of - Just uncovered_dcs -> - unless (S.null uncovered_dcs) $ + case (allDataConsAreCovered skolems (coerce $ hi_type hi) (coerce g)) of + Just covered -> + unless covered $ failure $ TacticPanic "Can't cover every datacon in domain" _ -> failure $ TacticPanic "Unable to fetch datacons" From 9ddf0f633e6f215b6d38fae9e190ac6d3d394eb7 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sat, 11 Sep 2021 12:24:13 -0500 Subject: [PATCH 9/9] Introduce skolems when destructing types --- plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 44cfb6f6c7..9d15ef0b04 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -64,12 +64,16 @@ destructMatches use_field_puns f scrut t jdg = do Nothing -> cut -- throwError $ GoalMismatch "destruct" g Just (dcs, apps) -> fmap unzipTrace $ for dcs $ \dc -> do + let (skolems', theta, args) = dataConInstSig dc apps + modify $ \ts -> + evidenceToSubst (foldMap mkEvidence theta) ts + & #ts_skolems <>~ S.fromList skolems' + let con = RealDataCon dc - ev = concatMap mkEvidence $ dataConInstArgTys dc apps + ev = concatMap mkEvidence $ dataConInstArgTys dc args -- We explicitly do not need to add the method hypothesis to -- #syn_scoped method_hy = foldMap evidenceToHypothesis ev - args = conLikeInstOrigArgTys' con apps ctx <- ask let names_in_scope = hyNamesInScope hy