WIP: GHC-9.0 support for hls-tactics-plugin

.github/workflows/test.yml

@@ -200,7 +200,7 @@ jobs:
         name: Test hls-fourmolu-plugin
         run: cabal test hls-fourmolu-plugin --test-options="-j1 --rerun-update" || cabal test hls-fourmolu-plugin --test-options="-j1 --rerun" || LSP_TEST_LOG_COLOR=0 LSP_TEST_LOG_MESSAGES=true LSP_TEST_LOG_STDERR=true cabal test hls-fourmolu-plugin --test-options="-j1 --rerun"
 
-      - if: ${{ needs.pre_job.outputs.should_skip != 'true' && matrix.test && matrix.ghc != '9.0.1' }}
+      - if: ${{ needs.pre_job.outputs.should_skip != 'true' && matrix.test }}
         name: Test hls-tactics-plugin test suite
         run: cabal test hls-tactics-plugin --test-options="-j1 --rerun-update" || cabal test hls-tactics-plugin --test-options="-j1 --rerun" || LSP_TEST_LOG_COLOR=0 LSP_TEST_LOG_MESSAGES=true LSP_TEST_LOG_STDERR=true cabal test hls-tactics-plugin --test-options="-j1 --rerun"
 

cabal-ghc901.project

@@ -6,7 +6,7 @@ packages:
          ./ghcide
          ./hls-plugin-api
          ./hls-test-utils
-        -- ./plugins/hls-tactics-plugin
+        ./plugins/hls-tactics-plugin
         -- ./plugins/hls-brittany-plugin
         -- ./plugins/hls-stylish-haskell-plugin
         -- ./plugins/hls-fourmolu-plugin
@@ -65,7 +65,7 @@ index-state: 2021-09-16T07:00:23Z
 
 constraints:
     -- These plugins don't work on GHC9 yet
-    haskell-language-server -brittany -class -fourmolu -stylishhaskell -tactic
+    haskell-language-server -brittany -class -fourmolu -stylishhaskell
 
 allow-newer:
     floskell:base,

configuration-ghc-901.nix

@@ -3,7 +3,6 @@
 
 let
   disabledPlugins = [
-    "hls-tactics-plugin"
     "hls-brittany-plugin"
     "hls-stylish-haskell-plugin"
     "hls-fourmolu-plugin"
@@ -54,7 +53,10 @@ let
       dependent-sum-template = hself.callCabal2nix "dependent-sum-template"
         "${dependent-sum-src}/dependent-sum-template" { };
 
-      hlint = hself.hlint_3_3_1;
+      hlint = hself.hlint_3_3_4;
+
+      generic-lens = hself.generic-lens_2_2_0_0;
+      generic-lens-core = hself.generic-lens-core_2_2_0_0;
 
       ghc-lib-parser = hself.ghc-lib-parser_9_0_1_20210324;
 
@@ -85,7 +87,6 @@ let
           "-f-class"
           "-f-fourmolu"
           "-f-stylishhaskell"
-          "-f-tactic"
         ]) { };
 
       # YOLO

ghcide/src/Development/IDE/GHC/Compat/Core.hs

@@ -66,7 +66,10 @@ module Development.IDE.GHC.Compat.Core (
     -- slightly unsafe
     setUnsafeGlobalDynFlags,
     -- * Linear Haskell
+#if !MIN_VERSION_ghc(9,0,0)
     Scaled,
+    unrestricted,
+#endif
     scaledThing,
     -- * Interface Files
     IfaceExport,
@@ -121,9 +124,12 @@ module Development.IDE.GHC.Compat.Core (
       TyCoRep.CoercionTy
       ),
     pattern FunTy,
+    pattern ConPatIn,
     Development.IDE.GHC.Compat.Core.splitForAllTyCoVars,
+#if !MIN_VERSION_ghc(9,0,0)
     Development.IDE.GHC.Compat.Core.mkVisFunTys,
     Development.IDE.GHC.Compat.Core.mkInfForAllTys,
+#endif
     -- * Specs
     ImpDeclSpec(..),
     ImportSpec(..),
@@ -336,6 +342,7 @@ module Development.IDE.GHC.Compat.Core (
     module GHC.Types.Var,
     module GHC.Unit.Module,
     module GHC.Utils.Error,
+    module TcType,
 #else
     module BasicTypes,
     module Class,
@@ -769,7 +776,9 @@ dataConExTyCoVars = DataCon.dataConExTyVars
 type Scaled a = a
 scaledThing :: Scaled a -> a
 scaledThing = id
-#endif
+
+unrestricted :: a -> Scaled a
+unrestricted = id
 
 mkVisFunTys :: [Scaled Type] -> Type -> Type
 mkVisFunTys =
@@ -781,10 +790,7 @@ mkVisFunTys =
 
 mkInfForAllTys :: [TyVar] -> Type -> Type
 mkInfForAllTys =
-#if MIN_VERSION_ghc(9,0,0)
-  TcType.mkInfForAllTys
-#else
-  mkInvForAllTys
+  mkInfForAllTys
 #endif
 
 splitForAllTyCoVars :: Type -> ([TyCoVar], Type)
@@ -846,3 +852,10 @@ type PlainGhcException = Plain.PlainGhcException
 #else
 type PlainGhcException = Plain.GhcException
 #endif
+
+#if MIN_VERSION_ghc(9,0,0)
+-- This is from the old api, but it still simplifies
+pattern ConPatIn :: SrcLoc.Located (ConLikeP GhcPs) -> HsConPatDetails GhcPs -> Pat GhcPs
+pattern ConPatIn con args = ConPat NoExtField con args
+#endif
+

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

@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP               #-}
 {-# LANGUAGE FlexibleContexts  #-}
 {-# LANGUAGE OverloadedLabels  #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -57,7 +58,7 @@ destructMatches use_field_puns f scrut t jdg = do
     Just (dcs, apps) ->
       fmap unzipTrace $ for dcs $ \dc -> do
         let con = RealDataCon dc
-            ev = concatMap mkEvidence $ dataConInstArgTys dc apps
+            ev = concatMap (mkEvidence . scaledThing) $ dataConInstArgTys dc apps
             -- We explicitly do not need to add the method hypothesis to
             -- #syn_scoped
             method_hy = foldMap evidenceToHypothesis ev
@@ -140,6 +141,7 @@ mkDestructPat already_in_scope con names
 
         in (names', )
          $ ConPatIn (noLoc $ Unqual $ occName $ conLikeName con)
+        --  $ ConPat NoExtField (noLoc $ Unqual $ occName $ conLikeName con)
          $ RecCon
          $ HsRecFields rec_fields
          $ Nothing
@@ -186,7 +188,7 @@ conLikeInstOrigArgTys'
       -- ^ 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 $
+   in map scaledThing $ 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.
@@ -230,7 +232,11 @@ destructLambdaCase' use_field_puns f jdg = do
   when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic
   let g  = jGoal jdg
   case splitFunTy_maybe (unCType g) of
+#if __GLASGOW_HASKELL__ >= 900
+    Just (_multiplicity, arg, _) | isAlgType arg ->
+#else
     Just (arg, _) | isAlgType arg ->
+#endif
       fmap (fmap noLoc lambdaCase) <$>
         destructMatches use_field_puns f Nothing (CType arg) jdg
     _ -> cut -- throwError $ GoalMismatch "destructLambdaCase'" g

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

@@ -11,6 +11,7 @@ import           Development.IDE.GHC.Compat.Util
 import           Wingman.GHC (normalizeType)
 import           Wingman.Judgements.Theta
 import           Wingman.Types
+-- import GHC.Tc.Utils.TcType (tcSplitPhiTy, tcSplitTyConApp)
 
 
 mkContext

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

@@ -88,7 +88,7 @@ scrutinzedType :: EmptyCaseSort Type -> Maybe Type
 scrutinzedType (EmptyCase ty) = pure  ty
 scrutinzedType (EmptyLamCase ty) =
   case tacticsSplitFunTy ty of
-    (_, _, tys, _) -> listToMaybe  tys
+    (_, _, tys, _) -> listToMaybe $ map scaledThing tys
 
 
 ------------------------------------------------------------------------------

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

@@ -17,6 +17,7 @@ import           Data.Traversable
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Compat.Util
 import           GHC.SourceGen (lambda)
+-- import           GHC.Tc.Utils.TcType (tcSplitSigmaTy, tcSplitNestedSigmaTys, tcSplitFunTys, tyCoVarsOfTypeList)
 import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
 import           Wingman.StaticPlugin (pattern MetaprogramSyntax)
 import           Wingman.Types
@@ -57,7 +58,7 @@ isFunction _                                    = True
 ------------------------------------------------------------------------------
 -- | Split a function, also splitting out its quantified variables and theta
 -- context.
-tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)
+tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Scaled Type], Type)
 tacticsSplitFunTy t
   = let (vars, theta, t') = tcSplitNestedSigmaTys t
         (args, res) = tcSplitFunTys t'
@@ -182,7 +183,11 @@ allOccNames = everything (<>) $ mkQ mempty $ \case
 
 ------------------------------------------------------------------------------
 -- | Unpack the relevant parts of a 'Match'
+#if __GLASGOW_HASKELL__ >= 900
+pattern AMatch :: HsMatchContext (NoGhcTc GhcPs) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
+#else
 pattern AMatch :: HsMatchContext (NameOrRdrName (IdP GhcPs)) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
+#endif
 pattern AMatch ctx pats body <-
   Match { m_ctxt = ctx
         , m_pats = fmap fromPatCompat -> pats
@@ -195,7 +200,7 @@ pattern SingleLet bind pats val expr <-
   HsLet _
     (L _ (HsValBinds _
       (ValBinds _ (bagToList ->
-        [(L _ (FunBind _ (L _ bind) (MG _ (L _ [L _ (AMatch _ pats val)]) _) _ _))]) _)))
+        [L _ (FunBind {fun_id = (L _ bind), fun_matches = (MG _ (L _ [L _ (AMatch _ pats val)]) _)})]) _)))
     (L _ expr)
 
 
@@ -258,7 +263,11 @@ pattern LamCase matches <-
 --         @Just False@ if it can't be homomorphic
 --         @Just True@ if it can
 lambdaCaseable :: Type -> Maybe Bool
+#if __GLASGOW_HASKELL__ >= 900
+lambdaCaseable (splitFunTy_maybe -> Just (_multiplicity, arg, res))
+#else
 lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
+#endif
   | isJust (algebraicTyCon arg)
   = Just $ isJust $ algebraicTyCon res
 lambdaCaseable _ = Nothing

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

@@ -180,7 +180,11 @@ absBinds _ _ = []
 ------------------------------------------------------------------------------
 -- | Extract evidence from 'HsWrapper's in scope
 wrapperBinds ::  SrcSpan -> LHsExpr GhcTc -> [PredType]
+#if __GLASGOW_HASKELL__ >= 900
+wrapperBinds dst (L src (XExpr (WrapExpr (HsWrap h _))))
+#else
 wrapperBinds dst (L src (HsWrap _ h _))
+#endif
   | dst `isSubspanOf` src = wrapper h
 wrapperBinds _ _ = []
 
@@ -196,7 +200,11 @@ matchBinds _ _ = []
 ------------------------------------------------------------------------------
 -- | Extract evidence from a 'ConPatOut'.
 patBinds ::  Pat GhcTc -> [PredType]
+#if __GLASGOW_HASKELL__ >= 900
+patBinds (ConPat{ pat_con_ext = ConPatTc { cpt_dicts = dicts }})
+#else
 patBinds (ConPatOut { pat_dicts = dicts })
+#endif
   = fmap idType dicts
 patBinds _ = []
 

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

@@ -292,8 +292,8 @@ getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
 
 getSpanAndTypeAtHole
     :: Tracked age Range
-    -> Tracked age (HieASTs b)
-    -> Maybe (Tracked age RealSrcSpan, b)
+    -> Tracked age (HieASTs Type)
+    -> Maybe (Tracked age RealSrcSpan, Type)
 getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do
   join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->
     case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range) ast of
@@ -386,7 +386,11 @@ buildPatHy prov (fromPatCompat -> p0) =
         (RealDataCon $ tupleDataCon boxity $ length pats)
         tys
           $ zip [0.. ] pats
-    ConPatOut (L _ con) args _ _ _ f _ ->
+#if __GLASGOW_HASKELL__ >= 900
+    ConPat {pat_con = (L _ con), pat_con_ext = ConPatTc {cpt_arg_tys = args}, pat_args = f} ->
+#else
+    ConPatOut {pat_con = (L _ con), pat_arg_tys = args, pat_args = f} ->
+#endif
       case f of
         PrefixCon l_pgt ->
           mkDerivedConHypothesis prov con args $ zip [0..] l_pgt
@@ -540,7 +544,11 @@ wingmanRules plId = do
                       L span (HsVar _ (L _ name))
                         | isHole (occName name) ->
                             maybeToList $ srcSpanToRange span
+#if __GLASGOW_HASKELL__ >= 900
+                      L span (HsUnboundVar _ occ)
+#else
                       L span (HsUnboundVar _ (TrueExprHole occ))
+#endif
                         | isHole occ ->
                             maybeToList $ srcSpanToRange span
 #if __GLASGOW_HASKELL__ <= 808

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

@@ -296,7 +296,7 @@ homoFilter codomain domain =
 liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r
 liftLambdaCase nil f t =
   case tacticsSplitFunTy t of
-    (_, _, arg : _, res) -> f res arg
+    (_, _, arg : _, res) -> f res $ scaledThing arg
     _ -> nil
 
 

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

@@ -17,6 +17,7 @@ import           Data.Traversable
 import           Development.IDE.GHC.Compat.Core hiding (IsFunction)
 import           Text.Hyphenation (hyphenate, english_US)
 import           Wingman.GHC (tcTyVar_maybe)
+-- import GHC.Tc.Utils.TcType (tcSplitFunTys, isBoolTy, isIntegerTy, isIntTy, isFloatingTy, isStringTy, tcSplitAppTys)
 
 
 ------------------------------------------------------------------------------
@@ -38,11 +39,11 @@ data Purpose
 
 pattern IsPredicate :: Type
 pattern IsPredicate <-
-  (tcSplitFunTys -> ([isFunTy -> False], isBoolTy -> True))
+  (tcSplitFunTys -> ([isFunTy . scaledThing -> False], isBoolTy -> True))
 
 pattern IsFunction :: [Type] -> Type -> Type
 pattern IsFunction args res <-
-  (tcSplitFunTys -> (args@(_:_), res))
+  (first (map scaledThing) . tcSplitFunTys -> (args@(_:_), res))
 
 pattern IsString :: Type
 pattern IsString <-