Use ConLikes instead of DataCons

plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs

@@ -9,6 +9,7 @@ module Wingman.CodeGen
   ) where
 
 
+import           ConLike
 import           Control.Lens ((%~), (<>~), (&))
 import           Control.Monad.Except
 import           Control.Monad.State
@@ -25,6 +26,7 @@ import           GHC.SourceGen.Binds
 import           GHC.SourceGen.Expr
 import           GHC.SourceGen.Overloaded
 import           GHC.SourceGen.Pat
+import           PatSyn
 import           Type hiding (Var)
 import           Wingman.CodeGen.Utils
 import           Wingman.GHC
@@ -36,7 +38,7 @@ import           Wingman.Types
 
 
 destructMatches
-    :: (DataCon -> Judgement -> Rule)
+    :: (ConLike -> Judgement -> Rule)
        -- ^ How to construct each match
     -> Maybe OccName
        -- ^ Scrutinee
@@ -54,47 +56,49 @@ destructMatches f scrut t jdg = do
       case dcs of
         [] -> throwError $ GoalMismatch "destruct" g
         _ -> fmap unzipTrace $ for dcs $ \dc -> do
-          let ev = mapMaybe mkEvidence $ dataConInstArgTys dc apps
+          let con = RealDataCon dc
+              ev = mapMaybe mkEvidence $ dataConInstArgTys dc apps
               -- We explicitly do not need to add the method hypothesis to
               -- #syn_scoped
               method_hy = foldMap evidenceToHypothesis ev
-              args = dataConInstOrigArgTys' dc apps
+              args = conLikeInstOrigArgTys' con apps
           modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev
           subst <- gets ts_unifier
           names <- mkManyGoodNames (hyNamesInScope hy) args
-          let hy' = patternHypothesis scrut dc jdg
+          let hy' = patternHypothesis scrut con jdg
                   $ zip names
                   $ coerce args
               j = fmap (CType . substTyAddInScope subst . unCType)
                 $ introduce hy'
                 $ introduce method_hy
                 $ withNewGoal g jdg
-          ext <- f dc j
+          ext <- f con j
           pure $ ext
             & #syn_trace %~ rose ("match " <> show dc <> " {" <> intercalate ", " (fmap show names) <> "}")
                           . pure
             & #syn_scoped <>~ hy'
-            & #syn_val     %~ match [mkDestructPat dc names] . unLoc
+            & #syn_val     %~ match [mkDestructPat con names] . unLoc
 
 
 ------------------------------------------------------------------------------
 -- | Produces a pattern for a data con and the names of its fields.
-mkDestructPat :: DataCon -> [OccName] -> Pat GhcPs
-mkDestructPat dcon names
-  | isTupleDataCon dcon =
+mkDestructPat :: ConLike -> [OccName] -> Pat GhcPs
+mkDestructPat con names
+  | RealDataCon dcon <- con
+  , isTupleDataCon dcon =
       tuple pat_args
   | otherwise =
-      infixifyPatIfNecessary dcon $
+      infixifyPatIfNecessary con $
         conP
-          (coerceName $ dataConName dcon)
+          (coerceName $ conLikeName con)
           pat_args
   where
     pat_args = fmap bvar' names
 
 
-infixifyPatIfNecessary :: DataCon -> Pat GhcPs -> Pat GhcPs
+infixifyPatIfNecessary :: ConLike -> Pat GhcPs -> Pat GhcPs
 infixifyPatIfNecessary dcon x
-  | dataConIsInfix dcon =
+  | conLikeIsInfix dcon =
       case x of
         ConPatIn op (PrefixCon [lhs, rhs]) ->
           ConPatIn op $ InfixCon lhs rhs
@@ -113,8 +117,8 @@ unzipTrace = sequenceA
 --
 -- NOTE: The behaviour depends on GHC's 'dataConInstOrigArgTys'.
 --       We need some tweaks if the compiler changes the implementation.
-dataConInstOrigArgTys'
-  :: DataCon
+conLikeInstOrigArgTys'
+  :: ConLike
       -- ^ 'DataCon'structor
   -> [Type]
       -- ^ /Universally/ quantified type arguments to a result type.
@@ -123,21 +127,30 @@ dataConInstOrigArgTys'
       --   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 $
+      -- ^ Types of arguments to the ConLike with returned type is instantiated with the second argument.
+conLikeInstOrigArgTys' con uniTys =
+  let exvars = conLikeExTys con
+   in conLikeInstOrigArgTys 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.
 
+
+conLikeExTys :: ConLike -> [TyCoVar]
+conLikeExTys (RealDataCon d) = dataConExTys d
+conLikeExTys (PatSynCon p) = patSynExTys p
+
+patSynExTys :: PatSyn -> [TyCoVar]
+patSynExTys ps = patSynExTyVars ps
+
+
 ------------------------------------------------------------------------------
 -- | Combinator for performing case splitting, and running sub-rules on the
 -- resulting matches.
 
-destruct' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
+destruct' :: (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
 destruct' f hi jdg = do
   when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
   let term = hi_name hi
@@ -156,7 +169,7 @@ destruct' f hi jdg = do
 ------------------------------------------------------------------------------
 -- | Combinator for performign case splitting, and running sub-rules on the
 -- resulting matches.
-destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
+destructLambdaCase' :: (ConLike -> Judgement -> Rule) -> Judgement -> Rule
 destructLambdaCase' f jdg = do
   when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
   let g  = jGoal jdg
@@ -171,11 +184,11 @@ destructLambdaCase' f jdg = do
 -- | Construct a data con with subgoals for each field.
 buildDataCon
     :: Judgement
-    -> DataCon            -- ^ The data con to build
+    -> ConLike            -- ^ The data con to build
     -> [Type]             -- ^ Type arguments for the data con
     -> RuleM (Synthesized (LHsExpr GhcPs))
 buildDataCon jdg dc tyapps = do
-  let args = dataConInstOrigArgTys' dc tyapps
+  let args = conLikeInstOrigArgTys' dc tyapps
   ext
       <- fmap unzipTrace
        $ traverse ( \(arg, n) ->

plugins/hls-tactics-plugin/src/Wingman/CodeGen/Utils.hs

@@ -1,5 +1,6 @@
 module Wingman.CodeGen.Utils where
 
+import ConLike (ConLike(RealDataCon), conLikeName)
 import Data.List
 import DataCon
 import Development.IDE.GHC.Compat
@@ -13,25 +14,32 @@ import Wingman.GHC (getRecordFields)
 
 ------------------------------------------------------------------------------
 -- | Make a data constructor with the given arguments.
-mkCon :: DataCon -> [Type] -> [LHsExpr GhcPs] -> LHsExpr GhcPs
-mkCon dcon apps (fmap unLoc -> args)
-  | dcon == nilDataCon
+mkCon :: ConLike -> [Type] -> [LHsExpr GhcPs] -> LHsExpr GhcPs
+mkCon con apps (fmap unLoc -> args)
+  | RealDataCon dcon <- con
+  , dcon == nilDataCon
   , [ty] <- apps
   , ty `eqType` charTy = noLoc $ string ""
-  | isTupleDataCon dcon =
+
+  | RealDataCon dcon <- con
+  , isTupleDataCon dcon =
       noLoc $ tuple args
-  | dataConIsInfix dcon
+
+  | RealDataCon dcon <- con
+  , dataConIsInfix dcon
   , (lhs : rhs : args') <- args =
-      noLoc $ foldl' (@@) (op lhs (coerceName dcon_name) rhs) args'
-  | Just fields <- getRecordFields dcon
+      noLoc $ foldl' (@@) (op lhs (coerceName con_name) rhs) args'
+
+  | Just fields <- getRecordFields con
   , length fields >= 2 =  --  record notation is unnatural on single field ctors
-      noLoc $ recordConE (coerceName dcon_name) $ do
+      noLoc $ recordConE (coerceName con_name) $ do
         (arg, (field, _)) <- zip args fields
         pure (coerceName field, arg)
+
   | otherwise =
-      noLoc $ foldl' (@@) (bvar' $ occName dcon_name) args
+      noLoc $ foldl' (@@) (bvar' $ occName con_name) args
   where
-    dcon_name = dataConName dcon
+    con_name = conLikeName con
 
 
 coerceName :: HasOccName a => a -> RdrNameStr

plugins/hls-tactics-plugin/src/Wingman/GHC.hs

@@ -3,6 +3,7 @@
 
 module Wingman.GHC where
 
+import           ConLike
 import           Control.Monad.State
 import           Data.Function (on)
 import           Data.Functor ((<&>))
@@ -106,12 +107,12 @@ freshTyvars t = do
 ------------------------------------------------------------------------------
 -- | Given a datacon, extract its record fields' names and types. Returns
 -- nothing if the datacon is not a record.
-getRecordFields :: DataCon -> Maybe [(OccName, CType)]
+getRecordFields :: ConLike -> Maybe [(OccName, CType)]
 getRecordFields dc =
-  case dataConFieldLabels dc of
+  case conLikeFieldLabels dc of
     [] -> Nothing
     lbls -> for lbls $ \lbl -> do
-      (_, ty) <- dataConFieldType_maybe dc $ flLabel lbl
+      let ty = conLikeFieldType dc $ flLabel lbl
       pure (mkVarOccFS $ flLabel lbl, CType ty)
 
 

plugins/hls-tactics-plugin/src/Wingman/Judgements.hs

@@ -1,17 +1,17 @@
 module Wingman.Judgements where
 
+import           ConLike (ConLike)
 import           Control.Arrow
-import           Control.Lens                        hiding (Context)
+import           Control.Lens hiding (Context)
 import           Data.Bool
 import           Data.Char
 import           Data.Coerce
-import           Data.Generics.Product               (field)
-import           Data.Map                            (Map)
-import qualified Data.Map                            as M
+import           Data.Generics.Product (field)
+import           Data.Map (Map)
+import qualified Data.Map as M
 import           Data.Maybe
-import           Data.Set                            (Set)
-import qualified Data.Set                            as S
-import           DataCon                             (DataCon)
+import           Data.Set (Set)
+import qualified Data.Set as S
 import           Development.IDE.Spans.LocalBindings
 import           OccName
 import           SrcLoc
@@ -163,7 +163,7 @@ findPositionVal jdg defn pos = listToMaybe $ do
 ------------------------------------------------------------------------------
 -- | Helper function for determining the ancestry list for
 -- 'filterSameTypeFromOtherPositions'.
-findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName]
+findDconPositionVals :: Judgement' a -> ConLike -> Int -> [OccName]
 findDconPositionVals jdg dcon pos = do
   (name, hi) <- M.toList $ hyByName $ jHypothesis jdg
   case hi_provenance hi of
@@ -178,7 +178,7 @@ findDconPositionVals jdg dcon pos = do
 -- given position for the datacon. Used to ensure recursive functions like
 -- 'fmap' preserve the relative ordering of their arguments by eliminating any
 -- other term which might match.
-filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement
+filterSameTypeFromOtherPositions :: ConLike -> Int -> Judgement -> Judgement
 filterSameTypeFromOtherPositions dcon pos jdg =
   let hy = hyByName
          . jHypothesis
@@ -230,7 +230,7 @@ extremelyStupid__definingFunction =
 
 patternHypothesis
     :: Maybe OccName
-    -> DataCon
+    -> ConLike
     -> Judgement' a
     -> [(OccName, a)]
     -> Hypothesis a
@@ -369,13 +369,6 @@ isTopLevel TopLevelArgPrv{} = True
 isTopLevel _                = False
 
 
-------------------------------------------------------------------------------
--- | Was this term defined by the user?
-isUserProv :: Provenance -> Bool
-isUserProv UserPrv{} = True
-isUserProv _         = False
-
-
 ------------------------------------------------------------------------------
 -- | Is this a local function argument, pattern match or user val?
 isLocalHypothesis :: Provenance -> Bool

plugins/hls-tactics-plugin/src/Wingman/KnownStrategies/QuickCheck.hs

@@ -1,5 +1,6 @@
 module Wingman.KnownStrategies.QuickCheck where
 
+import ConLike (ConLike(RealDataCon))
 import Control.Monad.Except (MonadError (throwError))
 import Data.Bool (bool)
 import Data.Generics (everything, mkQ)
@@ -76,7 +77,7 @@ data Generator = Generator
 mkGenerator :: TyCon -> [Type] -> DataCon -> Generator
 mkGenerator tc apps dc = do
   let dc_expr   = var' $ occName $ dataConName dc
-      args = dataConInstOrigArgTys' dc apps
+      args = conLikeInstOrigArgTys' (RealDataCon dc) apps
       num_recursive_calls = sum $ fmap (bool 0 1 . doesTypeContain tc) args
       mkArbitrary = mkArbitraryCall tc num_recursive_calls
   Generator num_recursive_calls $ case args of

plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs

@@ -31,7 +31,7 @@ import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi
 import           Development.Shake (Action, RuleResult)
 import           Development.Shake.Classes (Typeable, Binary, Hashable, NFData)
 import qualified FastString
-import           GhcPlugins (mkAppTys, tupleDataCon, consDataCon, substTyAddInScope)
+import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope)
 import           Ide.Plugin.Config (PluginConfig (plcConfig))
 import qualified Ide.Plugin.Config as Plugin
 import           Language.LSP.Server (MonadLsp, sendNotification)
@@ -236,25 +236,25 @@ buildPatHy prov (fromPatCompatTc -> p0) =
     -- Desugar lists into cons
     ListPat _ [] -> pure mempty
     ListPat x@(ListPatTc ty _) (p : ps) ->
-      mkDerivedConHypothesis prov consDataCon [ty]
+      mkDerivedConHypothesis prov (RealDataCon consDataCon) [ty]
         [ (0, p)
         , (1, toPatCompatTc $ ListPat x ps)
         ]
     -- Desugar tuples into an explicit constructor
     TuplePat tys pats boxity ->
       mkDerivedConHypothesis
         prov
-        (tupleDataCon boxity $ length pats)
+        (RealDataCon $ tupleDataCon boxity $ length pats)
         tys
           $ zip [0.. ] pats
-    ConPatOut (L _ (RealDataCon dc)) args _ _ _ f _ ->
+    ConPatOut (L _ con) args _ _ _ f _ ->
       case f of
         PrefixCon l_pgt ->
-          mkDerivedConHypothesis prov dc args $ zip [0..] l_pgt
+          mkDerivedConHypothesis prov con args $ zip [0..] l_pgt
         InfixCon pgt pgt5 ->
-          mkDerivedConHypothesis prov dc args $ zip [0..] [pgt, pgt5]
+          mkDerivedConHypothesis prov con args $ zip [0..] [pgt, pgt5]
         RecCon r ->
-          mkDerivedRecordHypothesis prov dc args r
+          mkDerivedRecordHypothesis prov con args r
 #if __GLASGOW_HASKELL__ >= 808
     SigPat  _ p _ -> buildPatHy prov p
 #endif
@@ -268,7 +268,7 @@ buildPatHy prov (fromPatCompatTc -> p0) =
 -- | Like 'mkDerivedConHypothesis', but for record patterns.
 mkDerivedRecordHypothesis
     :: Provenance
-    -> DataCon  -- ^ Destructing constructor
+    -> ConLike  -- ^ Destructing constructor
     -> [Type]   -- ^ Applied type variables
     -> HsRecFields GhcTc (PatCompat GhcTc)
     -> State Int (Hypothesis CType)
@@ -300,7 +300,7 @@ mkFakeVar = do
 -- build a sub-hypothesis for the pattern match.
 mkDerivedConHypothesis
     :: Provenance
-    -> DataCon                   -- ^ Destructing constructor
+    -> ConLike                   -- ^ Destructing constructor
     -> [Type]                    -- ^ Applied type variables
     -> [(Int, PatCompat GhcTc)]  -- ^ Patterns, and their order in the data con
     -> State Int (Hypothesis CType)
@@ -324,7 +324,7 @@ mkDerivedConHypothesis prov dc args ps = do
     -- way to get the real one. It's probably OK though, since we're generating
     -- this term with a disallowed provenance, and it doesn't actually exist
     -- anyway.
-    $ mkAppTys (dataConUserType dc) args
+    $ conLikeResTy dc args
 
 
 ------------------------------------------------------------------------------

plugins/hls-tactics-plugin/src/Wingman/Machinery.hs

@@ -166,7 +166,7 @@ scoreSolution ext goal holes
     initial_scope = hyByName $ jEntireHypothesis goal
     intro_vals = M.keysSet $ hyByName $ syn_scoped ext
     used_vals = S.intersection intro_vals $ syn_used_vals ext
-    used_user_vals = filter (isUserProv . hi_provenance)
+    used_user_vals = filter (isLocalHypothesis . hi_provenance)
                    $ mapMaybe (flip M.lookup initial_scope)
                    $ S.toList
                    $ syn_used_vals ext