Tactic plugin: Excludes Dictionary arguments in GADTs in Destruct Tactic

hie.yaml.cbl

@@ -25,6 +25,9 @@ cradle:
             - path: "./plugins/default/src"
               component: "haskell-language-server:exe:haskell-language-server"
 
+            - path: "./plugins/tactics/src"
+              component: "haskell-language-server:exe:haskell-language-server"
+
             - path: "./exe/Wrapper.hs"
               component: "haskell-language-server:exe:haskell-language-server-wrapper"
 

hie.yaml.stack

@@ -21,6 +21,8 @@ cradle:
 
             - path: "./plugins/default/src"
               component: "haskell-language-server:exe:haskell-language-server"
+            - path: "./plugins/tactics/src"
+              component: "haskell-language-server:exe:haskell-language-server"
 
             - path: "./exe/Arguments.hs"
               component: "haskell-language-server:exe:haskell-language-server"

plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs

@@ -38,7 +38,7 @@ destructMatches f f2 t jdg = do
       case dcs of
         [] -> throwError $ GoalMismatch "destruct" g
         _ -> for dcs $ \dc -> do
-          let args = dataConInstArgTys dc apps
+          let args = dataConInstOrigArgTys' dc apps
           names <- mkManyGoodNames hy args
 
           let pat :: Pat GhcPs
@@ -51,9 +51,19 @@ destructMatches f f2 t jdg = do
           pure $ match [pat] $ unLoc sg
 
 
+-- | Essentially same as 'dataConInstOrigArgTys' in GHC,
+--   but we need some tweaks in GHC >= 8.8.
+--   Since old 'dataConInstArgTys' seems working with >= 8.8,
+--   we just filter out non-class types in the result.
+dataConInstOrigArgTys' :: DataCon -> [Type] -> [Type]
+dataConInstOrigArgTys' con ty =
+    let tys0 = dataConInstArgTys con ty
+    in filter (maybe True (not . isClassTyCon) . tyConAppTyCon_maybe) tys0
+
 ------------------------------------------------------------------------------
 -- | Combinator for performing case splitting, and running sub-rules on the
 -- resulting matches.
+
 destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
 destruct' f term jdg = do
   let hy = jHypothesis jdg
@@ -85,7 +95,7 @@ buildDataCon
     -> [Type]             -- ^ Type arguments for the data con
     -> RuleM (LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
-  let args = dataConInstArgTys dc apps
+  let args = dataConInstOrigArgTys' dc apps
   sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
   pure
     . noLoc

stack-8.10.2.yaml

@@ -14,6 +14,7 @@ extra-deps:
   commit: c59655f10d5ad295c2481537fc8abf0a297d9d1c
 - Cabal-3.0.2.0
 - clock-0.7.2
+- data-tree-print-0.1.0.2
 - floskell-0.10.4
 - fourmolu-0.2.0.0
 - monad-dijkstra-0.1.1.2

test/functional/Tactic.hs

@@ -93,6 +93,8 @@ tests = testGroup
   , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto ""
   , goldenTest "GoldenNote.hs"              2 8  Auto ""
   , goldenTest "GoldenPureList.hs"          2 12 Auto ""
+  , goldenTest "GoldenGADTDestruct.hs"      7 17 Destruct "gadt"
+  , goldenTest "GoldenGADTAuto.hs"          7 13 Auto ""
   ]
 
 

test/testdata/tactic/GoldenGADTAuto.hs

@@ -0,0 +1,7 @@
+{-# LANGUAGE GADTs #-}
+module GoldenGADTAuto where
+data CtxGADT a where
+  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT a
+
+ctxGADT :: CtxGADT ()
+ctxGADT = _auto

test/testdata/tactic/GoldenGADTAuto.hs.expected

@@ -0,0 +1,7 @@
+{-# LANGUAGE GADTs #-}
+module GoldenGADTAuto where
+data CtxGADT a where
+  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT a
+
+ctxGADT :: CtxGADT ()
+ctxGADT = (MkCtxGADT ())

test/testdata/tactic/GoldenGADTDestruct.hs

@@ -0,0 +1,7 @@
+{-# LANGUAGE GADTs #-}
+module GoldenGADTDestruct where
+data CtxGADT where
+  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT
+
+ctxGADT :: CtxGADT -> String
+ctxGADT gadt = _decons

test/testdata/tactic/GoldenGADTDestruct.hs.expected

@@ -0,0 +1,7 @@
+{-# LANGUAGE GADTs #-}
+module GoldenGADTDestruct where
+data CtxGADT where
+  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT
+
+ctxGADT :: CtxGADT -> String
+ctxGADT gadt = (case gadt of { (MkCtxGADT a) -> _ })