Wingman: Use awareness of skolems when filtering GADT data constructors

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

@@ -52,16 +52,21 @@ destructMatches
 destructMatches use_field_puns f scrut t jdg = do
   let hy = jEntireHypothesis jdg
       g  = jGoal jdg
-  case tacticsGetDataCons $ unCType t of
+  skolems <- gets ts_skolems
+  case tacticsGetDataCons Destruction skolems $ unCType t of
     Nothing -> cut -- throwError $ GoalMismatch "destruct" g
     Just (dcs, apps) ->
       fmap unzipTrace $ for dcs $ \dc -> do
+        let (skolems', theta, args) = dataConInstSig dc apps
+        modify $ \ts ->
+          evidenceToSubst (foldMap mkEvidence theta) ts
+            & #ts_skolems <>~ S.fromList skolems'
+
         let con = RealDataCon dc
-            ev = concatMap mkEvidence $ dataConInstArgTys dc apps
+            ev = concatMap mkEvidence $ dataConInstArgTys dc args
             -- We explicitly do not need to add the method hypothesis to
             -- #syn_scoped
             method_hy = foldMap evidenceToHypothesis ev
-            args = conLikeInstOrigArgTys' con apps
         ctx <- ask
 
         let names_in_scope = hyNamesInScope hy
@@ -86,11 +91,11 @@ destructMatches use_field_puns f scrut t jdg = do
 
 ------------------------------------------------------------------------------
 -- | Generate just the 'Match'es for a case split on a specific type.
-destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
+destructionFor :: S.Set TyVar -> Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
 -- TODO(sandy): In an ideal world, this would be the same codepath as
 -- 'destructMatches'. Make sure to change that if you ever change this.
-destructionFor hy t = do
-  case tacticsGetDataCons t of
+destructionFor skolems hy t = do
+  case tacticsGetDataCons Destruction skolems t of
     Nothing -> Nothing
     Just ([], _) -> Nothing
     Just (dcs, apps) -> do
@@ -210,6 +215,7 @@ destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement
 destruct' use_field_puns f hi jdg = do
   when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic
   let term = hi_name hi
+  -- TODO(sandy): THIS NEEDS TO INTRODUCE SKOLEMS TOO
   ext
       <- destructMatches
            use_field_puns

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

@@ -65,7 +65,9 @@ emptyCaseInteraction = Interaction $
             range = realSrcSpanToRange $ unTrack ss
         matches <-
           liftMaybe $
-            destructionFor
+          -- TODO(sandy): This needs a judgment in order to correctly compute
+          -- the skolems! But we don't have a judgement yet :(
+            destructionFor mempty
               (foldMap (hySingleton . occName . fst) bindings)
               ty
         edits <- liftMaybe $ hush $
@@ -146,7 +148,9 @@ emptyCaseScrutinees state nfp = do
           . fmap (scrutinzedType <=< sequence)
           . traverse (typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg')
           $ scrutinee
-      case null $ tacticsGetDataCons ty of
+      -- TODO(sandy): This needs a judgment in order to correctly compute the
+      -- skolems! But we don't have a judgement yet :(
+      case null $ tacticsGetDataCons Destruction mempty ty of
         True -> pure empty
         False ->
           case ss of

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

@@ -18,9 +18,26 @@ import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Compat.Util
 import           GHC.SourceGen (lambda)
 import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
+import           GhcPlugins (Role (Nominal))
+import           OccName
+import           PrelNames (eqTyConKey, heqTyConKey)
+import           TcRnMonad
+import           TcType
+import           TyCoRep
+import           Type
+import           TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon)
+import           Unify
+import           Unique
+import           Var
 import           Wingman.StaticPlugin (pattern MetaprogramSyntax)
 import           Wingman.Types
 
+#if __GLASGOW_HASKELL__ == 810
+import Predicate
+#elif __GLASGOW_HASKELL__ >= 900
+import GHC.Core.Predicate
+#endif
+
 
 tcTyVar_maybe :: Type -> Maybe Var
 tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty'
@@ -72,17 +89,60 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 
 ------------------------------------------------------------------------------
 -- | Get the data cons of a type, if it has any.
-tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
-tacticsGetDataCons ty
+tacticsGetDataCons :: DataConMatchMode -> Set TyVar -> Type -> Maybe ([DataCon], [Type])
+tacticsGetDataCons mm skolems ty
   | Just (_, ty') <- tcSplitForAllTyVarBinder_maybe ty
-  = tacticsGetDataCons ty'
-tacticsGetDataCons ty
+  = tacticsGetDataCons mm skolems ty'
+tacticsGetDataCons mm skolems ty
   | Just _ <- algebraicTyCon ty
   = splitTyConApp_maybe ty <&> \(tc, apps) ->
-      ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc
+      ( filter (not . tacticsDataConCantMatch mm skolems apps) $ tyConDataCons tc
       , apps
       )
-tacticsGetDataCons _ = Nothing
+tacticsGetDataCons _ _ _ = Nothing
+
+
+data DataConMatchMode = Construction | Destruction
+  deriving (Eq, Ord, Show, Enum, Bounded)
+
+------------------------------------------------------------------------------
+-- | Directly ripped from GHC; minor changes to allow for skolems.
+tacticsDataConCantMatch :: DataConMatchMode -> Set TyVar -> [Type] -> DataCon -> Bool
+-- Returns True iff the data con *definitely cannot* match a
+--                  scrutinee of type (T tys)
+--                  where T is the dcRepTyCon for the data con
+tacticsDataConCantMatch mm skolems tys con
+  | null inst_theta   = False   -- Common
+  | otherwise         = typesCantMatch (concatMap predEqs inst_theta)
+  where
+    (_, inst_theta, _) = dataConInstSig con tys
+
+    -- TODO: could gather equalities from superclasses too
+    predEqs pred = case classifyPredType pred of
+                     EqPred NomEq ty1 ty2         -> [(ty1, ty2)]
+                     ClassPred eq args
+                       | eq `hasKey` eqTyConKey
+                       , [_, ty1, ty2] <- args    -> [(ty1, ty2)]
+                       | eq `hasKey` heqTyConKey
+                       , [_, _, ty1, ty2] <- args -> [(ty1, ty2)]
+                     _                            -> []
+
+
+    typesCantMatch :: [(Type,Type)] -> Bool
+    -- See Note [Pruning dead case alternatives]
+    typesCantMatch prs = any (uncurry cant_match) prs
+      where
+        cant_match :: Type -> Type -> Bool
+        cant_match t1 t2 = case tcUnifyTysFG (isSkolem skolems) [t1] [t2] of
+          SurelyApart -> True
+          MaybeApart _ ->
+            -- TODO(sandy): I don't know if ths logic is reasonable.
+            -- I experimented until the tests went green, but I have to admit
+            -- it's hella suspicious.
+            case mm of
+              Construction -> True
+              Destruction -> False
+          Unifiable _ -> False
 
 ------------------------------------------------------------------------------
 -- | Instantiate all of the quantified type variables in a type with fresh
@@ -346,12 +406,15 @@ expandTyFam :: Context -> Type -> Type
 expandTyFam ctx = snd . normaliseType  (ctxFamInstEnvs ctx) Nominal
 
 
+isSkolem :: Set TyVar -> TyVar -> BindFlag
+isSkolem skolems = bool BindMe Skolem . flip S.member skolems
+
 ------------------------------------------------------------------------------
 -- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.
 tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst
 tryUnifyUnivarsButNotSkolems skolems goal inst =
   case tcUnifyTysFG
-         (bool BindMe Skolem . flip S.member skolems)
+         (isSkolem skolems)
          [unCType inst]
          [unCType goal] of
     Unifiable subst -> pure subst

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

@@ -5,6 +5,7 @@ import           Control.Lens hiding (Context)
 import           Data.Bool
 import           Data.Char
 import           Data.Coerce
+import           Data.Foldable (toList)
 import           Data.Generics.Product (field)
 import           Data.Map (Map)
 import qualified Data.Map as M
@@ -470,3 +471,17 @@ isAlreadyDestructed _ = False
 expandDisallowed :: Provenance -> Provenance
 expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv
 expandDisallowed prv                   = prv
+
+
+------------------------------------------------------------------------------
+-- | Compute the skolems in scope for a given judgement.
+skolemsForJudgment :: Judgement -> Set TyVar
+skolemsForJudgment jdg
+  = S.fromList
+  $ foldMap (tyCoVarsOfTypeWellScoped . unCType)
+  $ (:) (jGoal jdg)
+  $ fmap hi_type
+  $ toList
+  $ hyByName
+  $ jHypothesis jdg
+

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

@@ -25,7 +25,7 @@ import           Wingman.AbstractLSP.Types
 import           Wingman.Auto
 import           Wingman.GHC
 import           Wingman.Judgements
-import           Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons)
+import           Wingman.Machinery (useNameFromHypothesis, allDataConsAreCovered)
 import           Wingman.Metaprogramming.Parser (parseMetaprogram)
 import           Wingman.Tactics
 import           Wingman.Types
@@ -116,7 +116,8 @@ commandProvider DestructPun =
       provide DestructPun $ T.pack $ occNameString occ
 commandProvider Homomorphism =
   requireHoleSort (== Hole) $
-  filterBindingType homoFilter $ \occ _ ->
+  withSkolems $ \skolems ->
+  filterBindingType (homoFilter skolems) $ \occ _ ->
     provide Homomorphism $ T.pack $ occNameString occ
 commandProvider DestructLambdaCase =
   requireHoleSort (== Hole) $
@@ -126,7 +127,8 @@ commandProvider DestructLambdaCase =
 commandProvider HomomorphismLambdaCase =
   requireHoleSort (== Hole) $
   requireExtension LambdaCase $
-    filterGoalType (liftLambdaCase False homoFilter) $
+  withSkolems $ \skolems ->
+    filterGoalType (liftLambdaCase False $ homoFilter skolems) $
       provide HomomorphismLambdaCase ""
 commandProvider DestructAll =
   requireHoleSort (== Hole) $
@@ -136,12 +138,13 @@ commandProvider DestructAll =
         False -> mempty
 commandProvider UseDataCon =
   requireHoleSort (== Hole) $
+  withSkolems $ \skolems ->
   withConfig $ \cfg ->
     filterTypeProjection
         ( guardLength (<= cfg_max_use_ctor_actions cfg)
         . fromMaybe []
         . fmap fst
-        . tacticsGetDataCons
+        . tacticsGetDataCons Construction skolems
         ) $ \dcon ->
       provide UseDataCon
         . T.pack
@@ -264,7 +267,17 @@ filterTypeProjection p tp tpd =
 ------------------------------------------------------------------------------
 -- | Get access to the 'Config' when building a 'TacticProvider'.
 withConfig :: (Config -> TacticProvider) -> TacticProvider
-withConfig tp tpd = tp (le_config $ tpd_lspEnv tpd) tpd
+withConfig = withs $ le_config . tpd_lspEnv
+
+
+withSkolems :: (S.Set TyVar -> TacticProvider) -> TacticProvider
+withSkolems = withs $ skolemsForJudgment . tpd_jdg
+
+
+------------------------------------------------------------------------------
+-- | Use something from the TPD to construct a 'TacticProvider'.
+withs :: (TacticProviderData -> a) -> (a -> TacticProvider) -> TacticProvider
+withs f tp tpd = tp (f tpd) tpd
 
 
 ------------------------------------------------------------------------------
@@ -284,11 +297,9 @@ 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 codomain domain =
-  case uncoveredDataCons domain codomain of
-    Just s -> S.null s
-    _ -> False
+homoFilter :: S.Set TyVar -> Type -> Type -> Bool
+homoFilter skolems codomain domain =
+  maybe False id $ allDataConsAreCovered skolems domain codomain
 
 
 ------------------------------------------------------------------------------

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

@@ -31,7 +31,7 @@ import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           System.Timeout (timeout)
 import           Wingman.Context (getInstance)
-import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars)
+import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars, DataConMatchMode(..))
 import           Wingman.Judgements
 import           Wingman.Simplify (simplify)
 import           Wingman.Types
@@ -90,16 +90,9 @@ runTactic
     -> TacticsM ()  -- ^ Tactic to use
     -> IO (Either [TacticError] RunTacticResults)
 runTactic duration ctx jdg t = do
-    let skolems = S.fromList
-                $ foldMap (tyCoVarsOfTypeWellScoped . unCType)
-                $ (:) (jGoal jdg)
-                $ fmap hi_type
-                $ toList
-                $ hyByName
-                $ jHypothesis jdg
-        tacticState =
+    let tacticState =
           defaultTacticState
-            { ts_skolems = skolems
+            { ts_skolems = skolemsForJudgment jdg
             }
 
     let stream = hoistListT (flip runReaderT ctx . unExtractM)
@@ -417,9 +410,11 @@ getCurrentDefinitions = do
 -- 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)
+allDataConsAreCovered :: S.Set TyVar -> Type -> Type -> Maybe Bool
+allDataConsAreCovered skolems domain codomain = do
+  (g_dcs, _) <- tacticsGetDataCons Destruction skolems codomain
+  (hi_dcs, _) <- tacticsGetDataCons Construction skolems domain
+  let constructable = S.fromList (coerce hi_dcs)
+      destructable = S.fromList (coerce g_dcs)
+  pure $ S.isSubsetOf @(Uniquely DataCon) destructable constructable