Wingman: Ensure homomorphic destruct covers all constructors in the domain

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/Tactics.hs

@@ -198,8 +198,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/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")
-    ]
-

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

@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs      #-}
+{-# LANGUAGE LambdaCase #-}
+
+data GADT a where
+  B1 :: GADT Bool
+  B2 :: GADT Bool
+  Int :: GADT Int
+  Var :: GADT a
+
+
+hasHomo :: GADT Bool -> GADT a
+hasHomo g = _
+
+cantHomo :: GADT a -> GADT Int
+cantHomo g = _
+
+hasHomoLam :: GADT Bool -> GADT a
+hasHomoLam = _
+
+cantHomoLam :: GADT a -> GADT Int
+cantHomoLam = _
+