From 5f9aabb24d84498899e0b6b53ab4a3dde6fdc521 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 18:52:10 -0800 Subject: [PATCH 1/2] Make sure split respects GADT equalities --- .../src/Ide/Plugin/Tactic/Tactics.hs | 5 ++--- plugins/hls-tactics-plugin/test/GoldenSpec.hs | 4 +++- .../hls-tactics-plugin/test/golden/AutoSplitGADT.hs | 12 ++++++++++++ .../test/golden/AutoSplitGADT.hs.expected | 12 ++++++++++++ 4 files changed, 29 insertions(+), 4 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoSplitGADT.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoSplitGADT.hs.expected diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index b388a4cee9..67a3c9ca0c 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -182,10 +182,9 @@ split :: TacticsM () split = tracing "split(user)" $ do jdg <- goal let g = jGoal jdg - case splitTyConApp_maybe $ unCType g of + case tacticsGetDataCons $ unCType g of Nothing -> throwError $ GoalMismatch "split" g - Just (tc, _) -> do - let dcs = tyConDataCons tc + Just (dcs, _) -> do choice $ fmap splitDataCon dcs diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs index e7a263814f..5ef937edbb 100644 --- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs +++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs @@ -115,10 +115,12 @@ spec = do refineTest "RefineReader.hs" 4 8 refineTest "RefineGADT.hs" 8 8 - + -- test via: + -- stack test hls-tactics-plugin --test-arguments '--match "Golden/golden tests/"' describe "golden tests" $ do let autoTest = mkGoldenTest allFeatures Auto "" + autoTest "AutoSplitGADT.hs" 11 8 goldenTest Intros "" "GoldenIntros.hs" 2 8 autoTest "GoldenEitherAuto.hs" 2 11 autoTest "GoldenJoinCont.hs" 4 12 diff --git a/plugins/hls-tactics-plugin/test/golden/AutoSplitGADT.hs b/plugins/hls-tactics-plugin/test/golden/AutoSplitGADT.hs new file mode 100644 index 0000000000..b15621e091 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/AutoSplitGADT.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE GADTs #-} + +data GADT b a where + GBool :: b -> GADT b Bool + GInt :: GADT b Int + +-- wingman would prefer to use GBool since then it can use its argument. But +-- that won't unify with GADT Int, so it is forced to pick GInt and ignore the +-- argument. +test :: b -> GADT b Int +test = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/AutoSplitGADT.hs.expected b/plugins/hls-tactics-plugin/test/golden/AutoSplitGADT.hs.expected new file mode 100644 index 0000000000..2521b651eb --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/AutoSplitGADT.hs.expected @@ -0,0 +1,12 @@ +{-# LANGUAGE GADTs #-} + +data GADT b a where + GBool :: b -> GADT b Bool + GInt :: GADT b Int + +-- wingman would prefer to use GBool since then it can use its argument. But +-- that won't unify with GADT Int, so it is forced to pick GInt and ignore the +-- argument. +test :: b -> GADT b Int +test _ = GInt + From 37486281191815b4bb00dee12f064578479451ee Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 18:53:58 -0800 Subject: [PATCH 2/2] Unnecessary do --- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 67a3c9ca0c..c0c0a88616 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -184,8 +184,7 @@ split = tracing "split(user)" $ do let g = jGoal jdg case tacticsGetDataCons $ unCType g of Nothing -> throwError $ GoalMismatch "split" g - Just (dcs, _) -> do - choice $ fmap splitDataCon dcs + Just (dcs, _) -> choice $ fmap splitDataCon dcs ------------------------------------------------------------------------------