Make sure split respects GADT equalities (#1466)

* Make sure split respects GADT equalities

* Unnecessary do

Co-authored-by: Junyoung/Clare Jang <jjc9310@gmail.com>

Author: isovector

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs

@@ -191,11 +191,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
-      choice $ fmap splitDataCon dcs
+    Just (dcs, _) -> choice $ fmap splitDataCon dcs
 
 
 ------------------------------------------------------------------------------

plugins/hls-tactics-plugin/test/GoldenSpec.hs

@@ -143,9 +143,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

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 = _
+

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
+