From 3bb84540d6b91d0d46db5176627020d16226ffb2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 3 Jun 2021 18:09:17 -0700
Subject: [PATCH 1/7] Fix unification pertaining to evidence

---
 .../hls-tactics-plugin/src/Wingman/CodeGen.hs |  3 +--
 .../src/Wingman/Judgements/Theta.hs           | 23 +++++++++++++++----
 .../src/Wingman/LanguageServer.hs             |  4 ++--
 .../test/CodeAction/AutoSpec.hs               |  1 +
 .../AutoThetaMultipleUnification.expected.hs  | 21 +++++++++++++++++
 .../golden/AutoThetaMultipleUnification.hs    | 21 +++++++++++++++++
 6 files changed, 65 insertions(+), 8 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.expected.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.hs

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 8795f14944..cdd7ab4242 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -18,7 +18,6 @@ import           Data.Bool (bool)
 import           Data.Functor ((<&>))
 import           Data.Generics.Labels ()
 import           Data.List
-import           Data.Monoid (Endo(..))
 import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
@@ -67,7 +66,7 @@ destructMatches use_field_puns f scrut t jdg = do
             -- #syn_scoped
             method_hy = foldMap evidenceToHypothesis ev
             args = conLikeInstOrigArgTys' con apps
-        modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev
+        modify $ evidenceToSubst ev
         subst <- gets ts_unifier
 
         let names_in_scope = hyNamesInScope hy
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
index de2ef33911..809b4f4223 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
@@ -18,7 +18,7 @@ import qualified Data.Set as S
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
 import           Generics.SYB hiding (tyConName, empty)
-import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst)
+import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst, unionTCvSubst, emptyTCvSubst, TCvSubst)
 #if __GLASGOW_HASKELL__ > 806
 import           GhcPlugins (eqTyCon)
 #else
@@ -77,8 +77,8 @@ getEvidenceAtHole (unTrack -> dst)
 
 ------------------------------------------------------------------------------
 -- | Update our knowledge of which types are equal.
-evidenceToSubst :: Evidence -> TacticState -> TacticState
-evidenceToSubst (EqualityOfTypes a b) ts =
+hi :: Evidence -> TacticState -> TacticState
+hi (EqualityOfTypes a b) ts =
   let tyvars = S.fromList $ mapMaybe getTyVar_maybe [a, b]
       -- If we can unify our skolems, at least one is no longer a skolem.
       -- Removing them from this set ensures we can get a subtitution between
@@ -89,7 +89,22 @@ evidenceToSubst (EqualityOfTypes a b) ts =
   case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of
     Just subst -> updateSubst subst ts
     Nothing -> ts
-evidenceToSubst HasInstance{} ts = ts
+hi HasInstance{} ts = ts
+
+substEvidence :: TCvSubst -> Evidence -> Evidence
+substEvidence subst (EqualityOfTypes ty ty') =
+  EqualityOfTypes (substTy subst ty) (substTy subst ty')
+substEvidence _ x = x
+
+allEvidenceToSubst :: [Evidence] -> TCvSubst
+allEvidenceToSubst [] = emptyTCvSubst
+allEvidenceToSubst (HasInstance{} : evs) = allEvidenceToSubst evs
+allEvidenceToSubst (eq@EqualityOfTypes{} : evs) =
+  let subst = ts_unifier $ hi eq defaultTacticState
+   in unionTCvSubst subst $ allEvidenceToSubst $ fmap (substEvidence subst) evs
+
+evidenceToSubst :: [Evidence] -> TacticState -> TacticState
+evidenceToSubst = updateSubst . allEvidenceToSubst
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index c7052a7070..0bc3d9b84e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -270,9 +270,9 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm
       already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs
       local_hy = spliceProvenance top_provs
                $ hypothesisFromBindings binds_rss binds
-      evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
+      evidence = traceIdX "evidence" $ getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
       cls_hy = foldMap evidenceToHypothesis evidence
-      subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState
+      subst = ts_unifier $ evidenceToSubst evidence defaultTacticState
   pure $
     ( disallowing AlreadyDestructed already_destructed
     $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
index 5c6b6efff5..bc1b7ef946 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
@@ -65,6 +65,7 @@ spec = do
     autoTest  6  8 "AutoThetaEqGADTDestruct"
     autoTest  6 10 "AutoThetaRefl"
     autoTest  6  8 "AutoThetaReflDestruct"
+    autoTest 19 30 "AutoThetaMultipleUnification"
 
   describe "known" $ do
     autoTest 25 13 "GoldenArbitrary"
diff --git a/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.expected.hs b/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.expected.hs
new file mode 100644
index 0000000000..446a4d73b3
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.expected.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+import Data.Kind
+
+data Nat = Z | S Nat
+
+data HList (ls :: [Type]) where
+  HNil :: HList '[]
+  HCons :: t -> HList ts -> HList (t ': ts)
+
+data ElemAt (n :: Nat) t (ts :: [Type]) where
+  AtZ :: ElemAt 'Z t (t ': ts)
+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
+
+lookMeUp :: ElemAt i ty tys -> HList tys -> ty
+lookMeUp AtZ (HCons t _) = t
+lookMeUp (AtS ea') (HCons t hl') = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.hs b/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.hs
new file mode 100644
index 0000000000..b0b520347d
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/AutoThetaMultipleUnification.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+import Data.Kind
+
+data Nat = Z | S Nat
+
+data HList (ls :: [Type]) where
+  HNil :: HList '[]
+  HCons :: t -> HList ts -> HList (t ': ts)
+
+data ElemAt (n :: Nat) t (ts :: [Type]) where
+  AtZ :: ElemAt 'Z t (t ': ts)
+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
+
+lookMeUp :: ElemAt i ty tys -> HList tys -> ty
+lookMeUp AtZ (HCons t hl') = _
+lookMeUp (AtS ea') (HCons t hl') = _
+

From 494b66a2c787bde0ea5f0b484c4c9a0a952b2633 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 3 Jun 2021 21:30:40 -0700
Subject: [PATCH 2/7] Cleanup interface; better names

---
 .../src/Wingman/Judgements/Theta.hs           | 61 +++++++++++--------
 .../src/Wingman/LanguageServer.hs             |  2 +-
 2 files changed, 38 insertions(+), 25 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
index 809b4f4223..d60526ee5b 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
@@ -12,12 +12,15 @@ module Wingman.Judgements.Theta
 
 import           Class (classTyVars)
 import           Control.Applicative (empty)
+import           Control.Lens (preview)
 import           Data.Maybe (fromMaybe, mapMaybe, maybeToList)
+import           Data.Generics.Sum (_Ctor)
 import           Data.Set (Set)
 import qualified Data.Set as S
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
-import           Generics.SYB hiding (tyConName, empty)
+import           Generics.SYB hiding (tyConName, empty, Generic)
+import           GHC.Generics
 import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst, unionTCvSubst, emptyTCvSubst, TCvSubst)
 #if __GLASGOW_HASKELL__ > 806
 import           GhcPlugins (eqTyCon)
@@ -40,7 +43,7 @@ data Evidence
   = EqualityOfTypes Type Type
     -- | We have an instance in scope
   | HasInstance PredType
-  deriving (Show)
+  deriving (Show, Generic)
 
 
 ------------------------------------------------------------------------------
@@ -75,36 +78,46 @@ getEvidenceAtHole (unTrack -> dst)
   . unTrack
 
 
-------------------------------------------------------------------------------
--- | Update our knowledge of which types are equal.
-hi :: Evidence -> TacticState -> TacticState
-hi (EqualityOfTypes a b) ts =
+mkSubst :: Set TyVar -> Type -> Type -> TCvSubst
+mkSubst skolems a b =
   let tyvars = S.fromList $ mapMaybe getTyVar_maybe [a, b]
       -- If we can unify our skolems, at least one is no longer a skolem.
       -- Removing them from this set ensures we can get a subtitution between
       -- the two. But it's okay to leave them in 'ts_skolems' in general, since
       -- they won't exist after running this substitution.
-      skolems = ts_skolems ts S.\\ tyvars
+      skolems' = skolems S.\\ tyvars
    in
-  case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of
-    Just subst -> updateSubst subst ts
-    Nothing -> ts
-hi HasInstance{} ts = ts
-
-substEvidence :: TCvSubst -> Evidence -> Evidence
-substEvidence subst (EqualityOfTypes ty ty') =
-  EqualityOfTypes (substTy subst ty) (substTy subst ty')
-substEvidence _ x = x
-
-allEvidenceToSubst :: [Evidence] -> TCvSubst
-allEvidenceToSubst [] = emptyTCvSubst
-allEvidenceToSubst (HasInstance{} : evs) = allEvidenceToSubst evs
-allEvidenceToSubst (eq@EqualityOfTypes{} : evs) =
-  let subst = ts_unifier $ hi eq defaultTacticState
-   in unionTCvSubst subst $ allEvidenceToSubst $ fmap (substEvidence subst) evs
+  case tryUnifyUnivarsButNotSkolems skolems' (CType a) (CType b) of
+    Just subst -> subst
+    Nothing -> emptyTCvSubst
+
+
+substPair :: TCvSubst -> (Type, Type) -> (Type, Type)
+substPair subst (ty, ty') = (substTy subst ty, substTy subst ty')
+
 
+------------------------------------------------------------------------------
+-- | Construct a substitution given a list of types that are equal to one
+-- another. This is more subtle than it seems, since there might be several
+-- equalities for the same type. We must be careful to push the accumulating
+-- substitution through each pair of types before adding their equalities.
+allEvidenceToSubst :: Set TyVar -> [(Type, Type)] -> TCvSubst
+allEvidenceToSubst _ [] = emptyTCvSubst
+allEvidenceToSubst skolems ((a, b) : evs) =
+  let subst = mkSubst skolems a b
+   in unionTCvSubst subst
+    $ allEvidenceToSubst skolems
+    $ fmap (substPair subst) evs
+
+------------------------------------------------------------------------------
+-- | Update our knowledge of which types are equal.
 evidenceToSubst :: [Evidence] -> TacticState -> TacticState
-evidenceToSubst = updateSubst . allEvidenceToSubst
+evidenceToSubst evs ts =
+  updateSubst
+    (allEvidenceToSubst (ts_skolems ts)
+      $ mapMaybe (preview $ _Ctor @"EqualityOfTypes")
+      $ evs)
+    ts
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 0bc3d9b84e..71400a8527 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -270,7 +270,7 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm
       already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs
       local_hy = spliceProvenance top_provs
                $ hypothesisFromBindings binds_rss binds
-      evidence = traceIdX "evidence" $ getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
+      evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
       cls_hy = foldMap evidenceToHypothesis evidence
       subst = ts_unifier $ evidenceToSubst evidence defaultTacticState
   pure $

From a2218df880f9cbd05122d8459f401cb32f5d704f Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 3 Jun 2021 21:58:13 -0700
Subject: [PATCH 3/7] Need to reapply the substituion after each arg

---
 .../hls-tactics-plugin/src/Wingman/Tactics.hs    | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index ed0f825b4f..ec7b7fd884 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -11,7 +11,7 @@ import           Control.Lens ((&), (%~), (<>~))
 import           Control.Monad (unless)
 import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader (ask))
-import           Control.Monad.State.Strict (StateT(..), runStateT)
+import           Control.Monad.State.Strict (StateT(..), runStateT, gets)
 import           Data.Bool (bool)
 import           Data.Foldable
 import           Data.Functor ((<&>))
@@ -160,7 +160,7 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do
   attemptWhen
       (rule $ destruct' False (\dc jdg ->
         buildDataCon False jdg dc $ snd $ splitAppTys g) hi)
-      (rule $ destruct' False (const subgoal) hi)
+      (rule $ destruct' False (const newSubgoal) hi)
     $ case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of
         (Just (gtc, _), Just (tytc, _)) -> gtc == tytc
         _ -> False
@@ -170,14 +170,14 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do
 -- | Case split, and leave holes in the matches.
 destruct :: HyInfo CType -> TacticsM ()
 destruct hi = requireConcreteHole $ tracing "destruct(user)" $
-  rule $ destruct' False (const subgoal) hi
+  rule $ destruct' False (const newSubgoal) hi
 
 
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches. Performs record punning.
 destructPun :: HyInfo CType -> TacticsM ()
 destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $
-  rule $ destruct' True (const subgoal) hi
+  rule $ destruct' True (const newSubgoal) hi
 
 
 ------------------------------------------------------------------------------
@@ -191,7 +191,7 @@ homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg ->
 -- | LambdaCase split, and leave holes in the matches.
 destructLambdaCase :: TacticsM ()
 destructLambdaCase =
-  tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const subgoal)
+  tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const newSubgoal)
 
 
 ------------------------------------------------------------------------------
@@ -335,7 +335,7 @@ destructAll :: TacticsM ()
 destructAll = do
   jdg <- goal
   let args = fmap fst
-           $ sort
+           $ sortOn snd
            $ mapMaybe (\(hi, prov) ->
               case prov of
                 TopLevelArgPrv _ idx _ -> pure (hi, idx)
@@ -345,7 +345,9 @@ destructAll = do
            $ filter (isAlgType . unCType . hi_type)
            $ unHypothesis
            $ jHypothesis jdg
-  for_ args destruct
+  for_ args $ \arg -> do
+    subst <- gets ts_unifier
+    destruct $ fmap (coerce substTy subst) arg
 
 --------------------------------------------------------------------------------
 -- | User-facing tactic to implement "Use constructor <x>"

From 0345066ec43961d825a9ca032e81f67c19d32fdc Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 3 Jun 2021 21:58:27 -0700
Subject: [PATCH 4/7] Reenable error debugging

---
 plugins/hls-tactics-plugin/src/Wingman/Plugin.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 95cb965f7f..6967f5ac5a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -121,7 +121,9 @@ tacticCmd tac pId state (TacticParams uri range var_name)
 
         timingOut (cfg_timeout_seconds cfg * seconds) $ join $
           case runTactic hj_ctx hj_jdg t of
-            Left _ -> Left TacticErrors
+            Left errs ->  do
+              traceMX "errs" errs
+              Left TacticErrors
             Right rtr ->
               case rtr_extract rtr of
                 L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->

From 14e747a61a84a1df24290bd93ed109ad626b6cbd Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 3 Jun 2021 22:01:00 -0700
Subject: [PATCH 5/7] Add destruct_all evidence test

---
 .../test/CodeAction/DestructAllSpec.hs        |  1 +
 .../DestructAllGADTEvidence.expected.hs       | 21 +++++++++++++++++++
 .../test/golden/DestructAllGADTEvidence.hs    | 20 ++++++++++++++++++
 3 files changed, 42 insertions(+)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.hs

diff --git a/plugins/hls-tactics-plugin/test/CodeAction/DestructAllSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/DestructAllSpec.hs
index 89579f7ba9..488fb3ebad 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/DestructAllSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/DestructAllSpec.hs
@@ -34,4 +34,5 @@ spec = do
     destructAllTest 4 23 "DestructAllMany"
     destructAllTest 2 18 "DestructAllNonVarTopMatch"
     destructAllTest 2 18 "DestructAllFunc"
+    destructAllTest 19 18 "DestructAllGADTEvidence"
 
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs
new file mode 100644
index 0000000000..b0b520347d
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+import Data.Kind
+
+data Nat = Z | S Nat
+
+data HList (ls :: [Type]) where
+  HNil :: HList '[]
+  HCons :: t -> HList ts -> HList (t ': ts)
+
+data ElemAt (n :: Nat) t (ts :: [Type]) where
+  AtZ :: ElemAt 'Z t (t ': ts)
+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
+
+lookMeUp :: ElemAt i ty tys -> HList tys -> ty
+lookMeUp AtZ (HCons t hl') = _
+lookMeUp (AtS ea') (HCons t hl') = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.hs
new file mode 100644
index 0000000000..3ac66d5444
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+import Data.Kind
+
+data Nat = Z | S Nat
+
+data HList (ls :: [Type]) where
+  HNil :: HList '[]
+  HCons :: t -> HList ts -> HList (t ': ts)
+
+data ElemAt (n :: Nat) t (ts :: [Type]) where
+  AtZ :: ElemAt 'Z t (t ': ts)
+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
+
+lookMeUp :: ElemAt i ty tys -> HList tys -> ty
+lookMeUp ea hl = _
+

From 2dd4f5d833b04ac906e2d817c09323d49b0b9b4b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 4 Jun 2021 07:06:24 -0700
Subject: [PATCH 6/7] Fix tests that were accidentally sorted incorrectly

---
 .../test/golden/DestructAllMany.expected.hs   | 30 +++++++++----------
 .../test/golden/MetaMaybeAp.expected.hs       |  2 +-
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs
index 27e3c93ae0..c443ed795e 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs
@@ -2,26 +2,26 @@ data ABC = A | B | C
 
 many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> ()
 many () (Left a) False Nothing A = _
-many () (Left a) False (Just abc') A = _
-many () (Right b') False Nothing A = _
-many () (Right b') False (Just abc') A = _
-many () (Left a) True Nothing A = _
-many () (Left a) True (Just abc') A = _
-many () (Right b') True Nothing A = _
-many () (Right b') True (Just abc') A = _
 many () (Left a) False Nothing B = _
+many () (Left a) False Nothing C = _
+many () (Left a) False (Just abc') A = _
 many () (Left a) False (Just abc') B = _
-many () (Right b') False Nothing B = _
-many () (Right b') False (Just abc') B = _
+many () (Left a) False (Just abc') C = _
+many () (Left a) True Nothing A = _
 many () (Left a) True Nothing B = _
+many () (Left a) True Nothing C = _
+many () (Left a) True (Just abc') A = _
 many () (Left a) True (Just abc') B = _
-many () (Right b') True Nothing B = _
-many () (Right b') True (Just abc') B = _
-many () (Left a) False Nothing C = _
-many () (Left a) False (Just abc') C = _
+many () (Left a) True (Just abc') C = _
+many () (Right b') False Nothing A = _
+many () (Right b') False Nothing B = _
 many () (Right b') False Nothing C = _
+many () (Right b') False (Just abc') A = _
+many () (Right b') False (Just abc') B = _
 many () (Right b') False (Just abc') C = _
-many () (Left a) True Nothing C = _
-many () (Left a) True (Just abc') C = _
+many () (Right b') True Nothing A = _
+many () (Right b') True Nothing B = _
 many () (Right b') True Nothing C = _
+many () (Right b') True (Just abc') A = _
+many () (Right b') True (Just abc') B = _
 many () (Right b') True (Just abc') C = _
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.expected.hs
index 8e40c9fa3f..e0b60b74fa 100644
--- a/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.expected.hs
@@ -1,5 +1,5 @@
 maybeAp :: Maybe (a -> b) -> Maybe a -> Maybe b
 maybeAp Nothing Nothing = Nothing
-maybeAp (Just _) Nothing = Nothing
 maybeAp Nothing (Just _) = Nothing
+maybeAp (Just _) Nothing = Nothing
 maybeAp (Just fab) (Just a) = Just (fab a)

From 7bb6f49e31b45cf990b779d260edc633cd77ac65 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 4 Jun 2021 11:56:47 -0700
Subject: [PATCH 7/7] FIx evidence when splitting GADTs

---
 .../hls-tactics-plugin/src/Wingman/CodeGen.hs   | 17 ++++++++++++++++-
 .../test/CodeAction/AutoSpec.hs                 |  2 ++
 .../AutoThetaSplitUnification.expected.hs       | 17 +++++++++++++++++
 .../test/golden/AutoThetaSplitUnification.hs    | 17 +++++++++++++++++
 .../test/golden/MessageCantUnify.hs             |  8 ++++++++
 5 files changed, 60 insertions(+), 1 deletion(-)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.expected.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MessageCantUnify.hs

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index cdd7ab4242..e8b57a96eb 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -251,7 +251,22 @@ buildDataCon
     -> [Type]             -- ^ Type arguments for the data con
     -> RuleM (Synthesized (LHsExpr GhcPs))
 buildDataCon should_blacklist jdg dc tyapps = do
-  let args = conLikeInstOrigArgTys' dc tyapps
+  args <- case dc of
+    RealDataCon dc' -> do
+      let (skolems', theta, args) = dataConInstSig dc' tyapps
+      modify $ \ts ->
+        evidenceToSubst (foldMap mkEvidence theta) ts
+          & #ts_skolems <>~ S.fromList skolems'
+      pure args
+    _ ->
+      -- If we have a 'PatSyn', we can't continue, since there is no
+      -- 'dataConInstSig' equivalent for 'PatSyn's. I don't think this is
+      -- a fundamental problem, but I don't know enough about the GHC internals
+      -- to implement it myself.
+      --
+      -- Fortunately, this isn't an issue in practice, since 'PatSyn's are
+      -- never in the hypothesis.
+      throwError $ TacticPanic "Can't build Pattern constructors yet"
   ext
       <- fmap unzipTrace
        $ traverse ( \(arg, n) ->
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
index bc1b7ef946..72b04e2f90 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
@@ -66,6 +66,7 @@ spec = do
     autoTest  6 10 "AutoThetaRefl"
     autoTest  6  8 "AutoThetaReflDestruct"
     autoTest 19 30 "AutoThetaMultipleUnification"
+    autoTest 16  9 "AutoThetaSplitUnification"
 
   describe "known" $ do
     autoTest 25 13 "GoldenArbitrary"
@@ -83,4 +84,5 @@ spec = do
 
   describe "messages" $ do
     mkShowMessageTest allFeatures Auto "" 2 8 "MessageForallA" TacticErrors
+    mkShowMessageTest allFeatures Auto "" 7 8 "MessageCantUnify" TacticErrors
 
diff --git a/plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.expected.hs b/plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.expected.hs
new file mode 100644
index 0000000000..e680f0265c
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.expected.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+data A = A
+data B = B
+data X = X
+data Y = Y
+
+
+data Pairrow ax by  where
+  Pairrow :: (a -> b) -> (x -> y) -> Pairrow '(a, x) '(b, y)
+
+test2 :: (A -> B) -> (X -> Y) -> Pairrow '(A, X) '(B, Y)
+test2 = Pairrow
+
diff --git a/plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.hs b/plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.hs
new file mode 100644
index 0000000000..e6ceeb1bcd
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/AutoThetaSplitUnification.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+data A = A
+data B = B
+data X = X
+data Y = Y
+
+
+data Pairrow ax by  where
+  Pairrow :: (a -> b) -> (x -> y) -> Pairrow '(a, x) '(b, y)
+
+test2 :: (A -> B) -> (X -> Y) -> Pairrow '(A, X) '(B, Y)
+test2 = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MessageCantUnify.hs b/plugins/hls-tactics-plugin/test/golden/MessageCantUnify.hs
new file mode 100644
index 0000000000..713f686338
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MessageCantUnify.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE DataKinds, GADTs #-}
+
+data Z ab where
+  Z :: (a -> b) -> Z '(a, b)
+
+test :: Z ab
+test = _
+