From a653039e888009b90aae671fc15947ce05b1b142 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 28 Jul 2021 11:08:42 -0700
Subject: [PATCH 1/2] Properly destruct forall-quantified types

---
 .../src/Wingman/CaseSplit.hs                  | 26 +++++++++++++++----
 plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 17 ++++++++----
 .../test/CodeAction/AutoSpec.hs               |  1 +
 .../golden/AutoForallClassMethod.expected.hs  | 12 +++++++++
 .../test/golden/AutoForallClassMethod.hs      | 12 +++++++++
 5 files changed, 58 insertions(+), 10 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoForallClassMethod.expected.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoForallClassMethod.hs

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
index c0ce1b1e29..6f93dc9bcd 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
@@ -30,10 +30,14 @@ mkFirstAgda pats body                = AgdaMatch pats body
 -- | Transform an 'AgdaMatch' whose body is a case over a bound pattern, by
 -- splitting it into multiple matches: one for each alternative of the case.
 agdaSplit :: AgdaMatch -> [AgdaMatch]
-agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
-  (pat, body) <- matches
-  -- TODO(sandy): use an at pattern if necessary
-  pure $ AgdaMatch (rewriteVarPat var pat pats) $ unLoc body
+agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches))
+  -- Ensure the thing we're destructing is actually a pattern that's been
+  -- bound.
+  | containsVar var pats
+  = do
+    (pat, body) <- matches
+    -- TODO(sandy): use an at pattern if necessary
+    pure $ AgdaMatch (rewriteVarPat var pat pats) $ unLoc body
 agdaSplit x = [x]
 
 
@@ -53,6 +57,19 @@ wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case
   (x :: Pat GhcPs)                                                    -> x
 
 
+------------------------------------------------------------------------------
+-- | Replace a 'VarPat' with the given @'Pat' GhcPs@.
+containsVar :: Data a => RdrName -> a -> Bool
+containsVar name = everything (||) $
+  mkQ False (\case
+    VarPat _ (L _ var) -> eqRdrName name var
+    (_ :: Pat GhcPs)   -> False
+      )
+  `extQ` \case
+    HsRecField lbl _ True ->  eqRdrName name $ unLoc $ rdrNameFieldOcc $ unLoc lbl
+    (_ :: HsRecField' (FieldOcc GhcPs) (PatCompat GhcPs)) -> False
+
+
 ------------------------------------------------------------------------------
 -- | Replace a 'VarPat' with the given @'Pat' GhcPs@.
 rewriteVarPat :: Data a => RdrName -> Pat GhcPs -> a -> a
@@ -68,7 +85,6 @@ rewriteVarPat name rep = everywhere $
     (x :: HsRecField' (FieldOcc GhcPs) (PatCompat GhcPs)) -> x
 
 
-
 ------------------------------------------------------------------------------
 -- | Construct an 'HsDecl' from a set of 'AgdaMatch'es.
 splitToDecl
diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index 3f1dbdbbbc..f3b82f9835 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -91,11 +91,15 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 ------------------------------------------------------------------------------
 -- | Get the data cons of a type, if it has any.
 tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
-tacticsGetDataCons ty | Just _ <- algebraicTyCon ty =
-  splitTyConApp_maybe ty <&> \(tc, apps) ->
-    ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc
-    , apps
-    )
+tacticsGetDataCons ty
+  | Just (_, ty') <- tcSplitForAllTy_maybe ty
+  = tacticsGetDataCons ty'
+tacticsGetDataCons ty
+  | Just _ <- algebraicTyCon ty
+  = splitTyConApp_maybe ty <&> \(tc, apps) ->
+      ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc
+      , apps
+      )
 tacticsGetDataCons _ = Nothing
 
 ------------------------------------------------------------------------------
@@ -132,6 +136,9 @@ getRecordFields dc =
 ------------------------------------------------------------------------------
 -- | Is this an algebraic type?
 algebraicTyCon :: Type -> Maybe TyCon
+algebraicTyCon ty
+  | Just (_, ty') <- tcSplitForAllTy_maybe ty
+  = algebraicTyCon ty'
 algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))
   | tycon == intTyCon    = Nothing
   | tycon == floatTyCon  = Nothing
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
index c776e2015a..f1f1e83a66 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
@@ -48,6 +48,7 @@ spec = do
     autoTest  2 19 "AutoInfixApplyMany"
     autoTest  2 25 "AutoInfixInfix"
     autoTest 19 12 "AutoTypeLevel"
+    autoTest 11  9 "AutoForallClassMethod"
 
     failing "flaky in CI" $
       autoTest 2 11 "GoldenApplicativeThen"
diff --git a/plugins/hls-tactics-plugin/test/golden/AutoForallClassMethod.expected.hs b/plugins/hls-tactics-plugin/test/golden/AutoForallClassMethod.expected.hs
new file mode 100644
index 0000000000..5846428ee7
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/AutoForallClassMethod.expected.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE ExplicitForAll        #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+import Data.Functor.Contravariant
+
+class Semigroupal cat t1 t2 to f where
+  combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y'))
+
+comux :: forall p a b c d. Semigroupal Op (,) (,) (,) p => p (a, c) (b, d) -> (p a b, p c d)
+comux = case combine of { (Op f) -> f }
+
diff --git a/plugins/hls-tactics-plugin/test/golden/AutoForallClassMethod.hs b/plugins/hls-tactics-plugin/test/golden/AutoForallClassMethod.hs
new file mode 100644
index 0000000000..9ee00c9255
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/AutoForallClassMethod.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE ExplicitForAll        #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+import Data.Functor.Contravariant
+
+class Semigroupal cat t1 t2 to f where
+  combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y'))
+
+comux :: forall p a b c d. Semigroupal Op (,) (,) (,) p => p (a, c) (b, d) -> (p a b, p c d)
+comux = _
+

From 75e440f18e827f3a229adfe69df56de13e3dd9a3 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 28 Jul 2021 11:12:07 -0700
Subject: [PATCH 2/2] Better haddock

---
 plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
index 6f93dc9bcd..e93af82e50 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
@@ -58,7 +58,7 @@ wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case
 
 
 ------------------------------------------------------------------------------
--- | Replace a 'VarPat' with the given @'Pat' GhcPs@.
+-- | Determine whether the given 'RdrName' exists as a 'VarPat' inside of @a@.
 containsVar :: Data a => RdrName -> a -> Bool
 containsVar name = everything (||) $
   mkQ False (\case