Merge branch 'master' into build-windows-ghcup

Author: jneira

.github/workflows/nix.yml

@@ -44,7 +44,7 @@ jobs:
     - if: ${{ needs.pre_job.outputs.should_skip_develop != 'true' }}
       uses: cachix/install-nix-action@v13
       with:
-        install_url: https://nixos-nix-install-tests.cachix.org/serve/lb41az54kzk6j12p81br4bczary7m145/install
+        install_url: https://nixos-nix-install-tests.cachix.org/serve/i6laym9jw3wg9mw6ncyrk6gjx4l34vvx/install
         install_options: '--tarball-url-prefix https://nixos-nix-install-tests.cachix.org/serve'
         extra_nix_config: |
           experimental-features = nix-command flakes
@@ -81,7 +81,7 @@ jobs:
         submodules: true
     - uses: cachix/install-nix-action@v13
       with:
-        install_url: https://nixos-nix-install-tests.cachix.org/serve/lb41az54kzk6j12p81br4bczary7m145/install
+        install_url: https://nixos-nix-install-tests.cachix.org/serve/i6laym9jw3wg9mw6ncyrk6gjx4l34vvx/install
         install_options: '--tarball-url-prefix https://nixos-nix-install-tests.cachix.org/serve'
         extra_nix_config: |
           experimental-features = nix-command flakes

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

@@ -150,16 +150,19 @@ emptyCaseScrutinees state nfp = do
     hscenv <- stale GhcSessionDeps
 
     let scrutinees = traverse (emptyCaseQ . tcg_binds) tcg
-    for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do
+    fmap catMaybes $ for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do
       ty <- MaybeT
           . fmap (scrutinzedType <=< sequence)
           . traverse (typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg')
           $ scrutinee
-      case ss of
-        RealSrcSpan r   -> do
-          rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
-          pure (rss', ty)
-        UnhelpfulSpan _ -> empty
+      case null $ tacticsGetDataCons ty of
+        True -> pure empty
+        False ->
+          case ss of
+            RealSrcSpan r   -> do
+              rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
+              pure $ Just (rss', ty)
+            UnhelpfulSpan _ -> empty
 
 data EmptyCaseSort a
   = EmptyCase a

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

@@ -22,7 +22,7 @@ import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
-import           GhcPlugins (containsSpan, realSrcLocSpan)
+import           GhcPlugins (containsSpan, realSrcLocSpan, realSrcSpanStart)
 import           Ide.Types
 import           Language.LSP.Types
 import           Prelude hiding (span)
@@ -50,8 +50,9 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr
           case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of
             Just (trss, program) -> do
               let tr_range = fmap realSrcSpanToRange trss
+                  rsl = realSrcSpanStart $ unTrack trss
               HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
-              z <- liftIO $ attempt_it ctx jdg $ T.unpack program
+              z <- liftIO $ attempt_it rsl ctx jdg $ T.unpack program
               pure $ Hover
                 { _contents = HoverContents
                             $ MarkupContent MkMarkdown

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

@@ -17,6 +17,7 @@ import           Data.Bool (bool)
 import           Data.Coerce
 import           Data.Maybe
 import           Data.Monoid
+import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
 import           DataCon (dataConName)
@@ -32,7 +33,7 @@ import           Prelude hiding (span)
 import           Wingman.Auto
 import           Wingman.GHC
 import           Wingman.Judgements
-import           Wingman.Machinery (useNameFromHypothesis)
+import           Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons)
 import           Wingman.Metaprogramming.Parser (parseMetaprogram)
 import           Wingman.Tactics
 import           Wingman.Types
@@ -126,7 +127,7 @@ commandProvider DestructLambdaCase =
 commandProvider HomomorphismLambdaCase =
   requireHoleSort (== Hole) $
   requireExtension LambdaCase $
-    filterGoalType ((== Just True) . lambdaCaseable) $
+    filterGoalType (liftLambdaCase False homoFilter) $
       provide HomomorphismLambdaCase ""
 commandProvider DestructAll =
   requireHoleSort (== Hole) $
@@ -313,8 +314,20 @@ tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
 -- | We should show homos only when the goal type is the same as the binding
 -- type, and that both are usual algebraic types.
 homoFilter :: Type -> Type -> Bool
-homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2
-homoFilter _ _                                                     = False
+homoFilter codomain domain =
+  case uncoveredDataCons domain codomain of
+    Just s -> S.null s
+    _ -> False
+
+
+------------------------------------------------------------------------------
+-- | Lift a function of (codomain, domain) over a lambda case.
+liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r
+liftLambdaCase nil f t =
+  case tacticsSplitFunTy t of
+    (_, _, arg : _, res) -> f res arg
+    _ -> nil
+
 
 
 ------------------------------------------------------------------------------

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

@@ -32,7 +32,7 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type (tyCoVarsOfTypeWellScoped)
 import           Wingman.Context (getInstance)
-import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst)
+import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons)
 import           Wingman.Judgements
 import           Wingman.Simplify (simplify)
 import           Wingman.Types
@@ -412,3 +412,15 @@ getCurrentDefinitions = do
   for ctx_funcs $ \res@(occ, _) ->
     pure . maybe res (occ,) =<< lookupNameInContext occ
 
+
+------------------------------------------------------------------------------
+-- | Given two types, see if we can construct a homomorphism by mapping every
+-- data constructor in the domain to the same in the codomain. This function
+-- returns 'Just' when all the lookups succeeded, and a non-empty value if the
+-- homomorphism *is not* possible.
+uncoveredDataCons :: Type -> Type -> Maybe (S.Set (Uniquely DataCon))
+uncoveredDataCons domain codomain = do
+  (g_dcs, _) <- tacticsGetDataCons codomain
+  (hi_dcs, _) <- tacticsGetDataCons domain
+  pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs)
+

plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs

@@ -21,6 +21,8 @@ import           Wingman.Metaprogramming.Parser.Documentation
 import           Wingman.Metaprogramming.ProofState (proofState, layout)
 import           Wingman.Tactics
 import           Wingman.Types
+import Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)
+import FastString (unpackFS)
 
 
 nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
@@ -421,17 +423,30 @@ wrapError :: String -> String
 wrapError err = "```\n" <> err <> "\n```\n"
 
 
+fixErrorOffset :: RealSrcLoc -> P.ParseErrorBundle a b -> P.ParseErrorBundle a b
+fixErrorOffset rsl (P.ParseErrorBundle ne (P.PosState a n (P.SourcePos _ line col) pos s))
+  = P.ParseErrorBundle ne
+  $ P.PosState a n
+      (P.SourcePos
+        (unpackFS $ srcLocFile rsl)
+        ((<>) line $ P.mkPos $ srcLocLine rsl - 1)
+        ((<>) col  $ P.mkPos $ srcLocCol  rsl - 1 + length @[] "[wingman|")
+      )
+      pos
+      s
+
 ------------------------------------------------------------------------------
 -- | Attempt to run a metaprogram tactic, returning the proof state, or the
 -- errors.
 attempt_it
-    :: Context
+    :: RealSrcLoc
+    -> Context
     -> Judgement
     -> String
     -> IO (Either String String)
-attempt_it ctx jdg program =
+attempt_it rsl ctx jdg program =
   case P.runParser tacticProgram "<splice>" (T.pack program) of
-    Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty peb
+    Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb
     Right tt -> do
       res <- runTactic
             ctx

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

@@ -127,21 +127,23 @@ intros' names = rule $ \jdg -> do
   let g  = jGoal jdg
   case tacticsSplitFunTy $ unCType g of
     (_, _, [], _) -> throwError $ GoalMismatch "intros" g
-    (_, _, as, b) -> do
+    (_, _, args, res) -> do
       ctx <- ask
-      let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names
-          num_args = length vs
+      let occs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args) names
+          num_occs = length occs
           top_hole = isTopHole ctx jdg
-          hy' = lambdaHypothesis top_hole $ zip vs $ coerce as
+          bindings = zip occs $ coerce args
+          bound_occs = fmap fst bindings
+          hy' = lambdaHypothesis top_hole bindings
           jdg' = introduce ctx hy'
-               $ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg
+               $ withNewGoal (CType $ mkFunTys' (drop num_occs args) res) jdg
       ext <- newSubgoal jdg'
       pure $
         ext
-          & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show vs) <> "}")
+          & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show bound_occs) <> "}")
                         . pure
           & #syn_scoped <>~ hy'
-          & #syn_val   %~ noLoc . lambda (fmap bvar' vs) . unLoc
+          & #syn_val   %~ noLoc . lambda (fmap bvar' bound_occs) . unLoc
 
 
 ------------------------------------------------------------------------------
@@ -198,8 +200,23 @@ destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $
 ------------------------------------------------------------------------------
 -- | Case split, using the same data constructor in the matches.
 homo :: HyInfo CType -> TacticsM ()
-homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg ->
-  buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
+homo hi = requireConcreteHole . tracing "homo" $ do
+  jdg <- goal
+  let g = jGoal jdg
+
+  -- Ensure that every data constructor in the domain type is covered in the
+  -- codomain; otherwise 'homo' will produce an ill-typed program.
+  case (uncoveredDataCons (coerce $ hi_type hi) (coerce g)) of
+    Just uncovered_dcs ->
+      unless (S.null uncovered_dcs) $
+        throwError  $ TacticPanic "Can't cover every datacon in domain"
+    _ -> throwError $ TacticPanic "Unable to fetch datacons"
+
+  rule
+    $ destruct'
+        False
+        (\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
+    $ hi
 
 
 ------------------------------------------------------------------------------

plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs

@@ -35,3 +35,81 @@ spec = do
     destructTest "a"  7 17 "LayoutSplitPattern"
     destructTest "a"  8 26 "LayoutSplitPatSyn"
 
+  describe "providers" $ do
+    mkTest
+      "Produces destruct and homomorphism code actions"
+      "T2" 2 21
+      [ (id, Destruct, "eab")
+      , (id, Homomorphism, "eab")
+      , (not, DestructPun, "eab")
+      ]
+
+    mkTest
+      "Won't suggest homomorphism on the wrong type"
+      "T2" 8 8
+      [ (not, Homomorphism, "global")
+      ]
+
+    mkTest
+      "Produces (homomorphic) lambdacase code actions"
+      "T3" 4 24
+      [ (id, HomomorphismLambdaCase, "")
+      , (id, DestructLambdaCase, "")
+      ]
+
+    mkTest
+      "Produces lambdacase code actions"
+      "T3" 7 13
+      [ (id, DestructLambdaCase, "")
+      ]
+
+    mkTest
+      "Doesn't suggest lambdacase without -XLambdaCase"
+      "T2" 11 25
+      [ (not, DestructLambdaCase, "")
+      ]
+
+    mkTest
+      "Doesn't suggest destruct if already destructed"
+      "ProvideAlreadyDestructed" 6 18
+      [ (not, Destruct, "x")
+      ]
+
+    mkTest
+      "...but does suggest destruct if destructed in a different branch"
+      "ProvideAlreadyDestructed" 9 7
+      [ (id, Destruct, "x")
+      ]
+
+    mkTest
+      "Doesn't suggest destruct on class methods"
+      "ProvideLocalHyOnly" 2 12
+      [ (not, Destruct, "mempty")
+      ]
+
+    mkTest
+      "Suggests homomorphism if the domain is bigger than the codomain"
+      "ProviderHomomorphism" 12 13
+      [ (id, Homomorphism, "g")
+      ]
+
+    mkTest
+      "Doesn't suggest homomorphism if the domain is smaller than the codomain"
+      "ProviderHomomorphism" 15 14
+      [ (not, Homomorphism, "g")
+      , (id, Destruct, "g")
+      ]
+
+    mkTest
+      "Suggests lambda homomorphism if the domain is bigger than the codomain"
+      "ProviderHomomorphism" 18 14
+      [ (id, HomomorphismLambdaCase, "")
+      ]
+
+    mkTest
+      "Doesn't suggest lambda homomorphism if the domain is smaller than the codomain"
+      "ProviderHomomorphism" 21 15
+      [ (not, HomomorphismLambdaCase, "")
+      , (id, DestructLambdaCase, "")
+      ]
+

plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs

@@ -38,4 +38,5 @@ spec = do
     metaTest  4 28 "MetaUseSymbol"
     metaTest  7 53 "MetaDeepOf"
     metaTest  2 34 "MetaWithArg"
+    metaTest  2 12 "IntrosTooMany"
 

plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs

@@ -9,6 +9,7 @@ import Utils
 spec :: Spec
 spec = do
   let test = mkCodeLensTest
+      noTest = mkNoCodeLensTest
 
   describe "golden" $ do
     test "EmptyCaseADT"
@@ -19,3 +20,6 @@ spec = do
     test "EmptyCaseGADT"
     test "EmptyCaseLamCase"
 
+  describe "no code lenses" $ do
+    noTest "EmptyCaseSpuriousGADT"
+

plugins/hls-tactics-plugin/test/ProviderSpec.hs

@@ -14,55 +14,9 @@ spec = do
     "T1" 2 14
     [ (id, Intros, "")
     ]
-  mkTest
-    "Produces destruct and homomorphism code actions"
-    "T2" 2 21
-    [ (id, Destruct, "eab")
-    , (id, Homomorphism, "eab")
-    , (not, DestructPun, "eab")
-    ]
-  mkTest
-    "Won't suggest homomorphism on the wrong type"
-    "T2" 8 8
-    [ (not, Homomorphism, "global")
-    ]
+
   mkTest
     "Won't suggest intros on the wrong type"
     "T2" 8 8
     [ (not, Intros, "")
     ]
-  mkTest
-    "Produces (homomorphic) lambdacase code actions"
-    "T3" 4 24
-    [ (id, HomomorphismLambdaCase, "")
-    , (id, DestructLambdaCase, "")
-    ]
-  mkTest
-    "Produces lambdacase code actions"
-    "T3" 7 13
-    [ (id, DestructLambdaCase, "")
-    ]
-  mkTest
-    "Doesn't suggest lambdacase without -XLambdaCase"
-    "T2" 11 25
-    [ (not, DestructLambdaCase, "")
-    ]
-
-  mkTest
-    "Doesn't suggest destruct if already destructed"
-    "ProvideAlreadyDestructed" 6 18
-    [ (not, Destruct, "x")
-    ]
-
-  mkTest
-    "...but does suggest destruct if destructed in a different branch"
-    "ProvideAlreadyDestructed" 9 7
-    [ (id, Destruct, "x")
-    ]
-
-  mkTest
-    "Doesn't suggest destruct on class methods"
-    "ProvideLocalHyOnly" 2 12
-    [ (not, Destruct, "mempty")
-    ]
-