diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index ec8caf8a9b..2afc9acb10 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -23,6 +23,7 @@ import GHC.SourceGen.Binds import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat +import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Naming @@ -120,13 +121,30 @@ unzipTrace l = -- | 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 +-- but only accepts universally quantified types as the second arguments +-- and automatically introduces existentials. +-- +-- NOTE: The behaviour depends on GHC's 'dataConInstOrigArgTys'. +-- We need some tweaks if the compiler changes the implementation. +dataConInstOrigArgTys' + :: DataCon + -- ^ 'DataCon'structor + -> [Type] + -- ^ /Universally/ quantified type arguments to a result type. + -- It /MUST NOT/ contain any dictionaries, coercion and existentials. + -- + -- For example, for @MkMyGADT :: b -> MyGADT a c@, we + -- must pass @[a, c]@ as this argument but not @b@, as @b@ is an existential. + -> [Type] + -- ^ Types of arguments to the DataCon with returned type is instantiated with the second argument. +dataConInstOrigArgTys' con uniTys = + let exvars = dataConExTys con + in dataConInstOrigArgTys con $ + uniTys ++ fmap mkTyVarTy exvars + -- Rationale: At least in GHC <= 8.10, 'dataConInstOrigArgTys' + -- unifies the second argument with DataCon's universals followed by existentials. + -- If the definition of 'dataConInstOrigArgTys' changes, + -- this place must be changed accordingly. ------------------------------------------------------------------------------ -- | Combinator for performing case splitting, and running sub-rules on the diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs index 3b66956257..3285479a49 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs @@ -9,6 +9,7 @@ import Control.Monad.State import qualified Data.Map as M import Data.Maybe (isJust) import Data.Traversable +import qualified DataCon as DataCon import Development.IDE.GHC.Compat import Generics.SYB (mkT, everywhere) import Ide.Plugin.Tactic.Types @@ -20,7 +21,6 @@ import TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon) import Unique import Var - tcTyVar_maybe :: Type -> Maybe Var tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty' tcTyVar_maybe (CastTy ty _) = tcTyVar_maybe ty -- look through casts, as @@ -148,3 +148,9 @@ getPatName (fromPatCompat -> p0) = #endif _ -> Nothing +dataConExTys :: DataCon -> [TyCoVar] +#if __GLASGOW_HASKELL__ >= 808 +dataConExTys = DataCon.dataConExTyCoVars +#else +dataConExTys = DataCon.dataConExTyVars +#endif \ No newline at end of file diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index a37474771b..7eeac215d8 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -104,6 +104,7 @@ tests = testGroup , goldenTest "GoldenSwap.hs" 2 8 Auto "" , goldenTest "GoldenFmapTree.hs" 4 11 Auto "" , goldenTest "GoldenGADTDestruct.hs" 7 17 Destruct "gadt" + , goldenTest "GoldenGADTDestructCoercion.hs" 8 17 Destruct "gadt" , goldenTest "GoldenGADTAuto.hs" 7 13 Auto "" , goldenTest "GoldenSwapMany.hs" 2 12 Auto "" , goldenTest "GoldenBigTuple.hs" 4 12 Auto "" diff --git a/test/testdata/tactic/GoldenGADTDestructCoercion.hs b/test/testdata/tactic/GoldenGADTDestructCoercion.hs new file mode 100644 index 0000000000..9eca759e85 --- /dev/null +++ b/test/testdata/tactic/GoldenGADTDestructCoercion.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE GADTs #-} +module GoldenGADTDestruct where +data E a b where + E :: forall a b. (b ~ a, Ord a) => b -> E a [a] + +ctxGADT :: E a b -> String +ctxGADT gadt = _decons diff --git a/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected b/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected new file mode 100644 index 0000000000..dca8ee9260 --- /dev/null +++ b/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected @@ -0,0 +1,8 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE GADTs #-} +module GoldenGADTDestruct where +data E a b where + E :: forall a b. (b ~ a, Ord a) => b -> E a [a] + +ctxGADT :: E a b -> String +ctxGADT gadt = (case gadt of { (E b) -> _ })