diff --git a/hie.yaml.cbl b/hie.yaml.cbl index e30fd51d61..46730ab9d9 100644 --- a/hie.yaml.cbl +++ b/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" diff --git a/hie.yaml.stack b/hie.yaml.stack index 18be9ff283..f9400d0914 100644 --- a/hie.yaml.stack +++ b/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" diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 1f1f3ea449..156673f5fe 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/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 diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml index c052b7fa0b..eb00a542bb 100644 --- a/stack-8.10.2.yaml +++ b/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 diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index e770ad8a41..bcef3e3951 100644 --- a/test/functional/Tactic.hs +++ b/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 "" ] diff --git a/test/testdata/tactic/GoldenGADTAuto.hs b/test/testdata/tactic/GoldenGADTAuto.hs new file mode 100644 index 0000000000..1c47dd0e07 --- /dev/null +++ b/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 diff --git a/test/testdata/tactic/GoldenGADTAuto.hs.expected b/test/testdata/tactic/GoldenGADTAuto.hs.expected new file mode 100644 index 0000000000..2159d09f3b --- /dev/null +++ b/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 ()) diff --git a/test/testdata/tactic/GoldenGADTDestruct.hs b/test/testdata/tactic/GoldenGADTDestruct.hs new file mode 100644 index 0000000000..588cf362a2 --- /dev/null +++ b/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 diff --git a/test/testdata/tactic/GoldenGADTDestruct.hs.expected b/test/testdata/tactic/GoldenGADTDestruct.hs.expected new file mode 100644 index 0000000000..2243aafdf6 --- /dev/null +++ b/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) -> _ })