Merge pull request #508 from konn/tactic-exclude-coercions

Makes dictionary argument exclusion logic in Tactic plugin more robust

Author: jneira

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

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

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 ""

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

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) -> _ })