From f642ef9ed501db7a8cb121eb7635cd9f3eb2476e Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 22 Nov 2023 14:18:22 +0000
Subject: [PATCH] [ cleanup ] remove dead code MkSeqConstraint

---
 src/Core/Unify.idr      | 21 ---------------------
 src/Core/UnifyState.idr | 17 -----------------
 2 files changed, 38 deletions(-)

diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr
index 475e633a4e..e7e75033c3 100644
--- a/src/Core/Unify.idr
+++ b/src/Core/Unify.idr
@@ -1419,27 +1419,6 @@ retry mode c
                       (\err => do defs <- get Ctxt
                                   empty <- clearDefs defs
                                   throw (WhenUnifying loc (gamma defs) env !(quote empty env x) !(quote empty env y) err))
-              Just (MkSeqConstraint loc env xsold ysold)
-                  => do defs <- get Ctxt
-                        xs <- traverse (continueNF defs env) xsold
-                        ys <- traverse (continueNF defs env) ysold
-                        cs <- unifyArgs mode loc env xs ys
-                        case constraints cs of
-                             [] => do deleteConstraint c
-                                      pure cs
-                             _ => pure cs
-  where
-    definedN : Name -> Core Bool
-    definedN n@(NS _ (MN _ _)) -- a metavar will only ever be a MN
-        = do defs <- get Ctxt
-             Just gdef <- lookupCtxtExact n (gamma defs)
-                  | _ => pure False
-             case definition gdef of
-                  Hole _ _ => pure (invertible gdef)
-                  BySearch _ _ _ => pure False
-                  Guess _ _ _ => pure False
-                  _ => pure True
-    definedN _ = pure True
 
 delayMeta : {vars : _} ->
             LazyReason -> Nat -> Term vars -> Term vars -> Term vars
diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr
index 24c8b36122..7943a4a80c 100644
--- a/src/Core/UnifyState.idr
+++ b/src/Core/UnifyState.idr
@@ -29,15 +29,6 @@ data Constraint : Type where
                     (env : Env Term vars) ->
                     (x : NF vars) -> (y : NF vars) ->
                     Constraint
-     -- An unsolved sequence of constraints, arising from arguments in an
-     -- application where solving later constraints relies on solving earlier
-     -- ones
-     MkSeqConstraint : {vars : _} ->
-                       FC ->
-                       (env : Env Term vars) ->
-                       (xs : List (NF vars)) ->
-                       (ys : List (NF vars)) ->
-                       Constraint
      -- A resolved constraint
      Resolved : Constraint
 
@@ -608,12 +599,6 @@ checkValidHole base (idx, (fc, n))
                                 xnf <- quote empty env x
                                 ynf <- quote empty env y
                                 throw (CantSolveEq fc (gamma defs) env xnf ynf)
-                          MkSeqConstraint fc env (x :: _) (y :: _) =>
-                             do put UST ({ guesses := empty } ust)
-                                empty <- clearDefs defs
-                                xnf <- quote empty env x
-                                ynf <- quote empty env y
-                                throw (CantSolveEq fc (gamma defs) env xnf ynf)
                           _ => pure ()
               _ => traverse_ checkRef !(traverse getFullName
                                         ((keys (getRefs (Resolved (-1)) (type gdef)))))
@@ -724,8 +709,6 @@ dumpHole str n hole
                          "\t    from " ++ show !(toFullNames !(quote empty env x))
                             ++ " =?= " ++ show !(toFullNames !(quote empty env y))
                             ++ if lazy then "\n\t(lazy allowed)" else ""
-                  Just (MkSeqConstraint _ _ xs ys) =>
-                       logString str n $ "\t\t" ++ show xs ++ " =?= " ++ show ys
 
 export
 dumpConstraints : {auto u : Ref UST UState} ->