From 04446746623312b92abdf2e81bc745cf4cce7988 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 19 Jan 2022 16:13:58 -0800 Subject: [PATCH 1/3] Fix fundeps --- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 11 ++++++++++ .../src/Wingman/Machinery.hs | 21 ++++++++++++++++++- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 3 ++- .../test/CodeAction/RunMetaprogramSpec.hs | 2 ++ .../test/golden/MetaFundeps.expected.hs | 16 ++++++++++++++ .../test/golden/MetaFundeps.hs | 16 ++++++++++++++ 6 files changed, 67 insertions(+), 2 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaFundeps.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaFundeps.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index 8a2da92770..04f4964d86 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -366,6 +366,17 @@ tryUnifyUnivarsButNotSkolems skolems goal inst = Unifiable subst -> pure subst _ -> Nothing +------------------------------------------------------------------------------ +-- | Like 'tryUnifyUnivarsButNotSkolems', but takes a list +-- of pairs of types to unify. +-- TODO(sandy): can the other one be implemented in terms of this? +tryUnifyUnivarsButNotSkolemsMany :: Set TyVar -> [(Type, Type)] -> Maybe TCvSubst +tryUnifyUnivarsButNotSkolemsMany skolems (unzip -> (goal, inst)) = + tcUnifyTys + (bool BindMe Skolem . flip S.member skolems) + inst + goal + updateSubst :: TCvSubst -> TacticState -> TacticState updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) } diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 44baec5a4b..8571ef1747 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -30,10 +30,12 @@ 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, tryUnifyUnivarsButNotSkolemsMany) import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types +import FunDeps (fd_eqs, improveFromInstEnv) +import Pair substCTy :: TCvSubst -> CType -> CType @@ -245,6 +247,23 @@ unify goal inst = do modify $ updateSubst subst Nothing -> cut +------------------------------------------------------------------------------ +-- | Get a substition out of a theta's fundeps +learnFromFundeps + :: ThetaType + -> RuleM () +learnFromFundeps theta = do + inst_envs <- asks ctxInstEnvs + skolems <- gets ts_skolems + subst <- gets ts_unifier + let theta' = substTheta subst theta + fundeps = foldMap (foldMap fd_eqs . improveFromInstEnv inst_envs (\_ _ -> ())) theta' + case tryUnifyUnivarsButNotSkolemsMany skolems $ fmap unPair fundeps of + Just subst -> + modify $ updateSubst subst + Nothing -> cut + + cut :: RuleT jdg ext err s m a cut = RuleT Empty diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 6e27b05cd4..d2d1e7121c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -279,11 +279,12 @@ apply (Unsaturated n) hi = tracing ("apply' " <> show (hi_name hi)) $ do ty = unCType $ hi_type hi func = hi_name hi ty' <- freshTyvars ty - let (_, _, all_args, ret) = tacticsSplitFunTy ty' + let (_, theta, all_args, ret) = tacticsSplitFunTy ty' saturated_args = dropEnd n all_args unsaturated_args = takeEnd n all_args rule $ \jdg -> do unify g (CType $ mkVisFunTys unsaturated_args ret) + learnFromFundeps theta ext <- fmap unzipTrace $ traverse ( newSubgoal diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs index 2fdf6a8936..453ee8edf6 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs @@ -41,5 +41,7 @@ spec = do metaTest 2 34 "MetaWithArg" metaTest 2 18 "MetaLetSimple" + metaTest 14 10 "MetaFundeps" + metaTest 2 12 "IntrosTooMany" diff --git a/plugins/hls-tactics-plugin/test/golden/MetaFundeps.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaFundeps.expected.hs new file mode 100644 index 0000000000..f589d989f7 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaFundeps.expected.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +class Blah a b | a -> b, b -> a +instance Blah Int Bool + +foo :: Int +foo = 10 + +bar :: Blah a b => a -> b +bar = undefined + +qux :: Bool +qux = bar foo + + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaFundeps.hs b/plugins/hls-tactics-plugin/test/golden/MetaFundeps.hs new file mode 100644 index 0000000000..36d0d4bf73 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaFundeps.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +class Blah a b | a -> b, b -> a +instance Blah Int Bool + +foo :: Int +foo = 10 + +bar :: Blah a b => a -> b +bar = undefined + +qux :: Bool +qux = [wingman| use bar, use foo |] + + From f4c93c387460aa107a590b5e2597f0c326f8b8b2 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 19 Jan 2022 16:19:27 -0800 Subject: [PATCH 2/3] One unifier to rule them all --- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index 04f4964d86..e90fce6de8 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -6,6 +6,7 @@ module Wingman.GHC where import Control.Monad.State import Control.Monad.Trans.Maybe (MaybeT(..)) import Data.Bool (bool) +import Data.Coerce (coerce) import Data.Function (on) import Data.Functor ((<&>)) import Data.List (isPrefixOf) @@ -359,17 +360,11 @@ expandTyFam ctx = snd . normaliseType (ctxFamInstEnvs ctx) Nominal -- | 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) - [unCType inst] - [unCType goal] of - Unifiable subst -> pure subst - _ -> Nothing + tryUnifyUnivarsButNotSkolemsMany skolems $ coerce [(goal, inst)] ------------------------------------------------------------------------------ -- | Like 'tryUnifyUnivarsButNotSkolems', but takes a list -- of pairs of types to unify. --- TODO(sandy): can the other one be implemented in terms of this? tryUnifyUnivarsButNotSkolemsMany :: Set TyVar -> [(Type, Type)] -> Maybe TCvSubst tryUnifyUnivarsButNotSkolemsMany skolems (unzip -> (goal, inst)) = tcUnifyTys From 3c49390e06670b90a7961ea999dad9b8b61348da Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 19 Jan 2022 16:26:48 -0800 Subject: [PATCH 3/3] Fix imports --- plugins/hls-tactics-plugin/src/Wingman/Machinery.hs | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 8571ef1747..5da56959a7 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -1,5 +1,6 @@ -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TupleSections #-} module Wingman.Machinery where @@ -34,8 +35,14 @@ import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tactics import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types + +#if __GLASGOW_HASKELL__ < 900 import FunDeps (fd_eqs, improveFromInstEnv) -import Pair +import Pair (unPair) +#else +import GHC.Tc.Instance.FunDeps (fd_eqs, improveFromInstEnv) +import GHC.Data.Pair (unPair) +#endif substCTy :: TCvSubst -> CType -> CType