From 3bb84540d6b91d0d46db5176627020d16226ffb2 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 3 Jun 2021 18:09:17 -0700 Subject: [PATCH 1/6] Fix unification pertaining to evidence --- .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 3 +-- .../src/Wingman/Judgements/Theta.hs | 23 +++++++++++++++---- .../src/Wingman/LanguageServer.hs | 4 ++-- .../test/CodeAction/AutoSpec.hs | 1 + .../AutoThetaMultipleUnification.expected.hs | 21 +++++++++++++++++ .../golden/AutoThetaMultipleUnification.hs | 21 +++++++++++++++++ 6 files changed, 65 insertions(+), 8 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 8795f14944..cdd7ab4242 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -18,7 +18,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 @@ -67,7 +66,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 let names_in_scope = hyNamesInScope hy diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs index de2ef33911..809b4f4223 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs @@ -18,7 +18,7 @@ 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 GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst, unionTCvSubst, emptyTCvSubst, TCvSubst) #if __GLASGOW_HASKELL__ > 806 import GhcPlugins (eqTyCon) #else @@ -77,8 +77,8 @@ getEvidenceAtHole (unTrack -> dst) ------------------------------------------------------------------------------ -- | Update our knowledge of which types are equal. -evidenceToSubst :: Evidence -> TacticState -> TacticState -evidenceToSubst (EqualityOfTypes a b) ts = +hi :: Evidence -> TacticState -> TacticState +hi (EqualityOfTypes a b) ts = 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 @@ -89,7 +89,22 @@ evidenceToSubst (EqualityOfTypes a b) ts = case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of Just subst -> updateSubst subst ts Nothing -> ts -evidenceToSubst HasInstance{} ts = ts +hi HasInstance{} ts = ts + +substEvidence :: TCvSubst -> Evidence -> Evidence +substEvidence subst (EqualityOfTypes ty ty') = + EqualityOfTypes (substTy subst ty) (substTy subst ty') +substEvidence _ x = x + +allEvidenceToSubst :: [Evidence] -> TCvSubst +allEvidenceToSubst [] = emptyTCvSubst +allEvidenceToSubst (HasInstance{} : evs) = allEvidenceToSubst evs +allEvidenceToSubst (eq@EqualityOfTypes{} : evs) = + let subst = ts_unifier $ hi eq defaultTacticState + in unionTCvSubst subst $ allEvidenceToSubst $ fmap (substEvidence subst) evs + +evidenceToSubst :: [Evidence] -> TacticState -> TacticState +evidenceToSubst = updateSubst . allEvidenceToSubst ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs index c7052a7070..0bc3d9b84e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs @@ -270,9 +270,9 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs local_hy = spliceProvenance top_provs $ hypothesisFromBindings binds_rss binds - evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs + evidence = traceIdX "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) $ mkFirstJudgement 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/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') = _ + From 494b66a2c787bde0ea5f0b484c4c9a0a952b2633 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 3 Jun 2021 21:30:40 -0700 Subject: [PATCH 2/6] Cleanup interface; better names --- .../src/Wingman/Judgements/Theta.hs | 61 +++++++++++-------- .../src/Wingman/LanguageServer.hs | 2 +- 2 files changed, 38 insertions(+), 25 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs index 809b4f4223..d60526ee5b 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs @@ -12,12 +12,15 @@ 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 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) @@ -40,7 +43,7 @@ data Evidence = EqualityOfTypes Type Type -- | We have an instance in scope | HasInstance PredType - deriving (Show) + deriving (Show, Generic) ------------------------------------------------------------------------------ @@ -75,36 +78,46 @@ getEvidenceAtHole (unTrack -> dst) . unTrack ------------------------------------------------------------------------------- --- | Update our knowledge of which types are equal. -hi :: Evidence -> TacticState -> TacticState -hi (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 -hi HasInstance{} ts = ts - -substEvidence :: TCvSubst -> Evidence -> Evidence -substEvidence subst (EqualityOfTypes ty ty') = - EqualityOfTypes (substTy subst ty) (substTy subst ty') -substEvidence _ x = x - -allEvidenceToSubst :: [Evidence] -> TCvSubst -allEvidenceToSubst [] = emptyTCvSubst -allEvidenceToSubst (HasInstance{} : evs) = allEvidenceToSubst evs -allEvidenceToSubst (eq@EqualityOfTypes{} : evs) = - let subst = ts_unifier $ hi eq defaultTacticState - in unionTCvSubst subst $ allEvidenceToSubst $ fmap (substEvidence subst) evs + 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 = updateSubst . allEvidenceToSubst +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 0bc3d9b84e..71400a8527 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs @@ -270,7 +270,7 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs local_hy = spliceProvenance top_provs $ hypothesisFromBindings binds_rss binds - evidence = traceIdX "evidence" $ getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs + evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs cls_hy = foldMap evidenceToHypothesis evidence subst = ts_unifier $ evidenceToSubst evidence defaultTacticState pure $ From a2218df880f9cbd05122d8459f401cb32f5d704f Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 3 Jun 2021 21:58:13 -0700 Subject: [PATCH 3/6] Need to reapply the substituion after each arg --- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index ed0f825b4f..ec7b7fd884 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 ((<&>)) @@ -160,7 +160,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 @@ -170,14 +170,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 ------------------------------------------------------------------------------ @@ -191,7 +191,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) ------------------------------------------------------------------------------ @@ -335,7 +335,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) @@ -345,7 +345,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 " From 0345066ec43961d825a9ca032e81f67c19d32fdc Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 3 Jun 2021 21:58:27 -0700 Subject: [PATCH 4/6] Reenable error debugging --- plugins/hls-tactics-plugin/src/Wingman/Plugin.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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) -> From 14e747a61a84a1df24290bd93ed109ad626b6cbd Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 3 Jun 2021 22:01:00 -0700 Subject: [PATCH 5/6] Add destruct_all evidence test --- .../test/CodeAction/DestructAllSpec.hs | 1 + .../DestructAllGADTEvidence.expected.hs | 21 +++++++++++++++++++ .../test/golden/DestructAllGADTEvidence.hs | 20 ++++++++++++++++++ 3 files changed, 42 insertions(+) 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/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/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 = _ + From 2dd4f5d833b04ac906e2d817c09323d49b0b9b4b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 4 Jun 2021 07:06:24 -0700 Subject: [PATCH 6/6] Fix tests that were accidentally sorted incorrectly --- .../test/golden/DestructAllMany.expected.hs | 30 +++++++++---------- .../test/golden/MetaMaybeAp.expected.hs | 2 +- 2 files changed, 16 insertions(+), 16 deletions(-) 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)