From 1f533bddf59ce22c97aa5b8af53166f93eecd3b5 Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Sat, 17 Oct 2020 13:53:52 +0900 Subject: [PATCH 1/8] Excludes predicate types at once --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 156673f5fe..e9901dc829 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -54,11 +54,11 @@ destructMatches f f2 t jdg = do -- | 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. +-- we just filter out class dictionaries anc coercions from the result. dataConInstOrigArgTys' :: DataCon -> [Type] -> [Type] dataConInstOrigArgTys' con ty = let tys0 = dataConInstArgTys con ty - in filter (maybe True (not . isClassTyCon) . tyConAppTyCon_maybe) tys0 + in filter (not . isPredTy) tys0 ------------------------------------------------------------------------------ -- | Combinator for performing case splitting, and running sub-rules on the From c706fa59d6fdf90ed5acf8d2e0697a27e28f3846 Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Sat, 17 Oct 2020 13:54:00 +0900 Subject: [PATCH 2/8] Adds a test case from #32 --- test/functional/Tactic.hs | 1 + test/testdata/tactic/GoldenGADTDestructCoercion.hs | 8 ++++++++ .../tactic/GoldenGADTDestructCoercion.hs.expected | 8 ++++++++ 3 files changed, 17 insertions(+) create mode 100644 test/testdata/tactic/GoldenGADTDestructCoercion.hs create mode 100644 test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index bcef3e3951..b53d7d904e 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -94,6 +94,7 @@ tests = testGroup , goldenTest "GoldenNote.hs" 2 8 Auto "" , goldenTest "GoldenPureList.hs" 2 12 Auto "" , goldenTest "GoldenGADTDestruct.hs" 7 17 Destruct "gadt" + , goldenTest "GoldenGADTDestructCoercion.hs" 8 17 Destruct "gadt" , goldenTest "GoldenGADTAuto.hs" 7 13 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) -> _ }) From 25ac4a9245f083f92a584214ee35820b36e3d87d Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Sat, 17 Oct 2020 13:58:18 +0900 Subject: [PATCH 3/8] Fixes typo --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index e9901dc829..5acc641b67 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -54,7 +54,7 @@ destructMatches f f2 t jdg = do -- | 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 class dictionaries anc coercions from the result. +-- we just filter out class dictionaries and coercions from the result. dataConInstOrigArgTys' :: DataCon -> [Type] -> [Type] dataConInstOrigArgTys' con ty = let tys0 = dataConInstArgTys con ty From 229397ec4e98db0c2099497b1c2857979560fd9a Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Sat, 17 Oct 2020 15:44:48 +0900 Subject: [PATCH 4/8] Gives another try for `dataConInstOrigArgTys` --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 5acc641b67..28ed5eaf5a 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -57,7 +57,7 @@ destructMatches f f2 t jdg = do -- we just filter out class dictionaries and coercions from the result. dataConInstOrigArgTys' :: DataCon -> [Type] -> [Type] dataConInstOrigArgTys' con ty = - let tys0 = dataConInstArgTys con ty + let tys0 = dataConInstOrigArgTys con ty in filter (not . isPredTy) tys0 ------------------------------------------------------------------------------ From 4ad648e8bdfaf0ec9ba4dc92bb941dff109300ac Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Mon, 23 Nov 2020 15:15:14 +0900 Subject: [PATCH 5/8] Glue code --- plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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 From 96bd4c9dde269da6856be3171d5b12eb5181bc78 Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Mon, 23 Nov 2020 15:17:23 +0900 Subject: [PATCH 6/8] Proper treatment of existentially quantified type variables in DataCons --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index ffceafdec1..c43b1bb614 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,13 @@ 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 class dictionaries and coercions from the result. +-- but only accepts universally quantified types as the second arguments +-- and automatically introduces existentials. dataConInstOrigArgTys' :: DataCon -> [Type] -> [Type] -dataConInstOrigArgTys' con ty = - let tys0 = dataConInstOrigArgTys con ty - in filter (not . isPredTy) tys0 +dataConInstOrigArgTys' con uniTys = + let exvars = dataConExTys con + in dataConInstOrigArgTys con $ + uniTys ++ map mkTyVarTy exvars ------------------------------------------------------------------------------ -- | Combinator for performing case splitting, and running sub-rules on the From 53712b3762e55e5d5c89a8d2434d61536369c1c5 Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Tue, 24 Nov 2020 00:16:00 +0900 Subject: [PATCH 7/8] Uses `fmap` instead --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index c43b1bb614..43c86fb489 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -127,7 +127,7 @@ dataConInstOrigArgTys' :: DataCon -> [Type] -> [Type] dataConInstOrigArgTys' con uniTys = let exvars = dataConExTys con in dataConInstOrigArgTys con $ - uniTys ++ map mkTyVarTy exvars + uniTys ++ fmap mkTyVarTy exvars ------------------------------------------------------------------------------ -- | Combinator for performing case splitting, and running sub-rules on the From 01110c8eeb22ea567128d0e7ae4921c331894a94 Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Tue, 24 Nov 2020 01:51:34 +0900 Subject: [PATCH 8/8] Adds notes on implementation of `dataConInstOrigArgTys` --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 43c86fb489..2afc9acb10 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -123,11 +123,28 @@ unzipTrace l = -- | Essentially same as 'dataConInstOrigArgTys' in GHC, -- but only accepts universally quantified types as the second arguments -- and automatically introduces existentials. -dataConInstOrigArgTys' :: DataCon -> [Type] -> [Type] +-- +-- 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