Only show unifiable ctors

Author: isovector

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs

@@ -22,7 +22,7 @@ import           Data.Maybe
 import           Data.Monoid
 import qualified Data.Text as T
 import           Data.Traversable
-import           DataCon (dataConName)
+import           DataCon (dataConName, dataConCannotMatch)
 import           Development.IDE.GHC.Compat
 import           GHC.Generics
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
@@ -80,9 +80,7 @@ commandProvider UseDataCon =
     requireFeature FeatureUseDataCon $
       filterTypeProjection
           ( guardLength (<= cfg_max_use_ctor_actions cfg)
-          . fromMaybe []
-          . fmap fst
-          . tacticsGetDataCons
+          . useCtorFilter
           ) $ \dcon ->
         provide UseDataCon
           . T.pack
@@ -231,3 +229,14 @@ destructFilter :: Type -> Type -> Bool
 destructFilter _ (algebraicTyCon -> Just _) = True
 destructFilter _ _                          = False
 
+
+------------------------------------------------------------------------------
+-- | Only show data cons in "Use constructor" if they can unify with the goal
+useCtorFilter :: Type -> [DataCon]
+useCtorFilter ty
+  | Just (dcs, apps) <- tacticsGetDataCons ty = do
+      dc <- dcs
+      guard $ not $ dataConCannotMatch apps dc
+      pure dc
+useCtorFilter _ = []
+

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

@@ -80,7 +80,7 @@ spec = do
     describe "provider" $ do
       mkTest
         "Suggests all data cons for Either"
-        "ConProviders.hs" 3 6
+        "ConProviders.hs" 5 6
         [ (id, UseDataCon, "Left")
         , (id, UseDataCon, "Right")
         , (not, UseDataCon, ":")
@@ -89,9 +89,16 @@ spec = do
         ]
       mkTest
         "Suggests no data cons for big types"
-        "ConProviders.hs" 9 17 $ do
+        "ConProviders.hs" 11 17 $ do
           c <- [1 :: Int .. 10]
           pure $ (not, UseDataCon, T.pack $ show c)
+      mkTest
+        "Suggests only matching data cons for GADT"
+        "ConProviders.hs" 20 12
+        [ (id, UseDataCon, "IntGADT")
+        , (id, UseDataCon, "VarGADT")
+        , (not, UseDataCon, "BoolGADT")
+        ]
 
     describe "golden" $ do
       useTest "(,)"   "UseConPair.hs"  2 8

plugins/hls-tactics-plugin/test/golden/ConProviders.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE GADTs #-}
+
 -- Should suggest Left and Right, but not []
 t1 :: Either a b
 t1 = _
@@ -8,3 +10,12 @@ data ManyConstructors = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10
 noCtorsIfMany :: ManyConstructors
 noCtorsIfMany = _
 
+
+data GADT a where
+  IntGADT  :: GADT Int
+  BoolGADT :: GADT Bool
+  VarGADT  :: GADT a
+
+gadtCtor :: GADT Int
+gadtCtor = _
+