diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 5f2f86605c..3d31d5b268 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -52,16 +52,21 @@ 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 Destruction skolems $ unCType t of 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 @@ -86,11 +91,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 Destruction skolems t of Nothing -> Nothing Just ([], _) -> Nothing Just (dcs, apps) -> do @@ -210,6 +215,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/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs index 42c62cfc19..2f64f2d2e7 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs @@ -65,7 +65,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 $ @@ -146,7 +148,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 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 647d6cd60b..3393d39876 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -18,9 +18,26 @@ import Development.IDE.GHC.Compat import Development.IDE.GHC.Compat.Util 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 +import Type +import TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon) +import Unify +import Unique +import Var import Wingman.StaticPlugin (pattern MetaprogramSyntax) import Wingman.Types +#if __GLASGOW_HASKELL__ == 810 +import Predicate +#elif __GLASGOW_HASKELL__ >= 900 +import GHC.Core.Predicate +#endif + tcTyVar_maybe :: Type -> Maybe Var tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty' @@ -72,17 +89,60 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta, _)) = theta ------------------------------------------------------------------------------ -- | Get the data cons of a type, if it has any. -tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type]) -tacticsGetDataCons ty +tacticsGetDataCons :: DataConMatchMode -> Set TyVar -> Type -> Maybe ([DataCon], [Type]) +tacticsGetDataCons mm skolems ty | Just (_, ty') <- tcSplitForAllTyVarBinder_maybe ty - = tacticsGetDataCons ty' -tacticsGetDataCons ty + = tacticsGetDataCons mm skolems ty' +tacticsGetDataCons mm skolems ty | Just _ <- algebraicTyCon ty = splitTyConApp_maybe ty <&> \(tc, apps) -> - ( filter (not . dataConCannotMatch 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 :: 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 mm skolems tys con + | null inst_theta = False -- 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 + 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 ------------------------------------------------------------------------------ -- | Instantiate all of the quantified type variables in a type with fresh @@ -346,12 +406,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 1b5a88999b..ef97b9ae1e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs @@ -5,6 +5,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 @@ -470,3 +471,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 631baf58b7..2b9a59316d 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -25,7 +25,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 @@ -116,7 +116,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) $ @@ -126,7 +127,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) $ @@ -136,12 +138,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 Construction skolems ) $ \dcon -> provide UseDataCon . T.pack @@ -264,7 +267,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 ------------------------------------------------------------------------------ @@ -284,11 +297,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 - Just s -> S.null s - _ -> False +homoFilter :: S.Set TyVar -> Type -> Type -> Bool +homoFilter skolems codomain domain = + 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 56fd9f7b2e..823b16a89f 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -31,7 +31,7 @@ import Refinery.Tactic import Refinery.Tactic.Internal import System.Timeout (timeout) import Wingman.Context (getInstance) -import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars) +import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars, DataConMatchMode(..)) import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types @@ -90,16 +90,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) @@ -417,9 +410,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 :: Type -> Type -> Maybe (S.Set (Uniquely DataCon)) -uncoveredDataCons domain codomain = do - (g_dcs, _) <- tacticsGetDataCons codomain - (hi_dcs, _) <- tacticsGetDataCons domain - pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs) +allDataConsAreCovered :: S.Set TyVar -> Type -> Type -> Maybe Bool +allDataConsAreCovered skolems domain codomain = do + (g_dcs, _) <- tacticsGetDataCons Destruction skolems codomain + (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 d6909a11ca..474b81eda9 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -12,7 +12,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 ((<&>)) @@ -198,6 +198,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 @@ -207,6 +208,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 @@ -230,12 +232,13 @@ 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 - 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" @@ -307,7 +310,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 Construction skolems $ unCType g of Nothing -> failure $ GoalMismatch "split" g Just (dcs, _) -> choice $ fmap splitDataCon dcs @@ -320,7 +324,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 Construction skolems $ unCType g of Nothing -> failure $ GoalMismatch "split" g Just (dcs, _) -> do case isSplitWhitelisted jdg of @@ -337,7 +342,8 @@ splitSingle :: TacticsM () splitSingle = tracing "splitSingle" $ do jdg <- goal let g = jGoal jdg - case tacticsGetDataCons $ unCType g of + skolems <- gets ts_skolems + case tacticsGetDataCons Construction skolems $ unCType g of Just ([dc], _) -> do splitDataCon dc _ -> failure $ GoalMismatch "splitSingle" g 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 = _ +