Wingman: Properly destruct forall-quantified types (#2049)

* Properly destruct forall-quantified types

* Better haddock

Author: isovector

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
 
 
+------------------------------------------------------------------------------
+-- | Determine whether the given 'RdrName' exists as a 'VarPat' inside of @a@.
+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

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

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"

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 }
+

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 = _
+