content: {-# LANGUAGE NondecreasingIndentation #-}
  
  module Agda.TypeChecking.Coverage.Cubical where
  
  import Prelude hiding (null, (!!))  -- do not use partial functions like !!
  
  import Control.Monad.Except ( runExceptT )
  
  import qualified Data.Set as Set
  import Data.IntSet (IntSet)
  import qualified Data.IntSet as IntSet
  
  import Agda.Syntax.Common
  import Agda.Syntax.Position
  import Agda.Syntax.Internal hiding (DataOrRecord)
  import Agda.Syntax.Internal.Pattern
  import Agda.Syntax.Common.Pretty (prettyShow)
  
  import Agda.TypeChecking.Constraints () -- instance MonadConstraint TCM
  import Agda.TypeChecking.Coverage.Match
  import Agda.TypeChecking.Coverage.SplitClause
  import Agda.TypeChecking.Coverage.SplitTree
  import Agda.TypeChecking.Datatypes (getDatatypeArgs)
  import Agda.TypeChecking.Irrelevance
  import Agda.TypeChecking.Monad
  import Agda.TypeChecking.Names
  import Agda.TypeChecking.Pretty
  import Agda.TypeChecking.Primitive hiding (Nat)
  import Agda.TypeChecking.Reduce
  import Agda.TypeChecking.Substitute
  import Agda.TypeChecking.Telescope
  import Agda.TypeChecking.Telescope.Path
  
  import Agda.Utils.Either ( fromRight )
  import Agda.Utils.Functor
  import Agda.Utils.List
  import Agda.Utils.List1 ( pattern (:|) )
  import qualified Agda.Utils.List1 as List1
  import Agda.Utils.Maybe
  import Agda.Utils.Monad
  import Agda.Utils.Null
  import Agda.Utils.Permutation
  import Agda.Utils.Singleton
  import Agda.Utils.Size
  
  import Agda.Utils.Impossible
  
  
  createMissingIndexedClauses :: QName
                              -> Arg Nat
                              -> BlockingVar
                              -> SplitClause
                              -> [(SplitTag,(SplitClause,IInfo))]
                              -> [Clause]
                              -> TCM ([(SplitTag,CoverResult)],[Clause])
  createMissingIndexedClauses f n x old_sc scs cs = do
    let infos = [(c,i) | (SplitCon c, (_,TheInfo i)) <- scs ]
    case scs of
      xs | info:_ <- infos -> do
           reportSDoc "tc.cover.indexed" 20 $ text "size (xs,infos):" <+> pretty (size xs,size infos)
           reportSDoc "tc.cover.indexed" 20 $ text "xs :" <+> pretty (map fst xs)
  
           unless (size xs == 1 + size infos) $
              reportSDoc "tc.cover.indexed" 20 $ text "missing some infos"
              -- Andrea: what to do when we only managed to build a unification proof for some of the constructors?
           Constructor{conData} <- theDef <$> getConstInfo (fst info)
           Datatype{dataPars = pars, dataIxs = nixs, dataTranspIx} <- theDef <$> getConstInfo conData
           hcomp <- fromMaybe __IMPOSSIBLE__ <$> getName' builtinHComp
           trX <- fromMaybe __IMPOSSIBLE__ <$> pure dataTranspIx
           trX_cl <- createMissingTrXTrXClause trX f n x old_sc
           hcomp_cl <- createMissingTrXHCompClause trX f n x old_sc
           (trees,cls) <- fmap unzip . forM infos $ \ (c,i) -> do
             cl <- createMissingTrXConClause trX f n x old_sc c i
             return $ ((SplitCon c , SplittingDone (size $ clauseTel cl)) , cl)
           let extra = [ (SplitCon trX, SplittingDone $ size $ clauseTel trX_cl)
                                             , (SplitCon hcomp, SplittingDone $ size $ clauseTel hcomp_cl)
                                             ]
                   --  = [ (SplitCon trX, SplittingDone $ size $ clauseTel trX_cl) ]
               extraCl = [trX_cl, hcomp_cl]
                   --  = [trX_cl]
           let clauses = cls ++ extraCl
           let tree = SplitAt (n <&> (+ (pars + nixs + 1))) StrictSplit $
                                             trees
                                          ++ extra
               res = CoverResult
                 { coverSplitTree      = tree
                 , coverUsedClauses    = let l = length cs in IntSet.fromAscList [l .. l + length clauses - 1]
                 , coverMissingClauses = []
                 , coverPatterns       = clauses
                 , coverNoExactClauses = IntSet.empty
                 }
           reportSDoc "tc.cover.indexed" 20 $
             "tree:" <+> pretty tree
           addClauses f clauses
           return ([(SplitCon trX, res)], cs ++ clauses)
      xs | otherwise -> return ([], cs)
  
  covFillTele :: QName -> Abs Telescope -> Term -> Args -> Term -> TCM [Term]
  covFillTele func tel face d j = do
    ed_f <- liftTCM $ runExceptT $ trFillTel tel face d j
    case ed_f of
      Right d_f -> pure $ map unArg d_f
      Left failed_t -> typeError $ CannotGenerateTransportClause func failed_t
  
  createMissingTrXTrXClause :: QName -- ^ trX
                              -> QName -- ^ f defined
                              -> Arg Nat
                              -> BlockingVar
                              -> SplitClause
                              -> TCM Clause
  createMissingTrXTrXClause q_trX f n x old_sc = do
    let
     old_tel = scTel old_sc
     old_ps = fromSplitPatterns $ scPats old_sc
     old_t = fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
  
    reportSDoc "tc.cover.trx.trx" 20 $ "trX-trX clause for" <+> prettyTCM f
    reportSDoc "tc.cover.trx.trx" 20 $ nest 2 $ vcat $
      [ "old_tel:" <+> prettyTCM old_tel
      , "old_ps :" <+> addContext old_tel (prettyTCM $ patternsToElims old_ps)
      , "old_t  :" <+> addContext old_tel (prettyTCM old_t)
      ]
  
    -- TODO: redo comments, the strategy changed.
    -- old_tel = Γ1, (x : D η v), Δ
    -- α = boundary(old_ps)
    -- Γ1, (x : D η v), Δ ⊢ f old_ps : old_t [ α ↦ (f old_ps)[α] ]
  
    -- α' = boundary(old_ps[x = pat])
    -- Γ1, φ : I, p : Path X(η) _ v, ψ : I, q : Path X(η) _ (p i0), x0 : D η (q i0) ⊢ pat := trX p φ (trX q ψ x0) : D η v
  
    -- Ξ = Γ1, φ : I, p : Path X(η) _ v, ψ : I, q : Path X(η) _ (p i0), x0 : D η (q i0), Δ[x = pat]
  
    -- Ξ ⊢ w1 := f old_ps[γ1,x = pat,δ] : old_t[γ1,x = pat,δ] -- the case we are defining. can only be used if specialized.
  
    -- Ξ ⊢ rhs : old_t[γ1,x = pat,δ] [ α' ↦ w1[α']
                                  -- , φ  ↦ w1[φ = i1, p = refl]
                                  -- , ψ  ↦ w1[ψ = i1, q = refl]
                                  -- ]
    -- Ξ ⊢ q2 := tr (i. Path X(η) (q i0) (p i)) φ q : Path X(η) (q i0) (p i1)
    -- Ξ ⊢ pat_rec[0] = pat : D η v
    -- Ξ ⊢ pat_rec[1] = trX q2 (φ ∧ ψ) x0 : D η v
    -- Ξ ⊢ pat-rec[i] := trX (\ j → p (i ∨ j)) (i ∨ φ) (trX (q2_f i) (ψ ∧ (φ ∨ ~ i)) t)
  
    -- Ξ ⊢ δ_f[1] = tr (i. Δ[γ1,x = pat_rec[i]]) (φ ∧ ψ) δ
    -- Ξ ⊢ w0 := f old_ps[γ1,x = pat_rec[1] ,δ_f[1]] : old_t[γ1,x = pat_rec[1],δ_f[1]]
    -- Ξ ⊢ rhs := tr (i. old_t[γ1,x = pat_rec[~i], δ_f[~i]]) (φ ∧ ψ) w0 -- TODO plus sides.
  
    interval <- elInf primInterval
    iz <- primIZero
    io <- primIOne
    tHComp <- primHComp
    tNeg <- primINeg
    let neg i = pure tNeg <@> i
    let min i j = cl primIMin <@> i <@> j
    let max i j = cl primIMax <@> i <@> j
    let
      old_tel = scTel old_sc
      old_ps' = AbsN (teleNames old_tel) $ fromSplitPatterns $ scPats old_sc
      old_ps = pure $ old_ps'
      old_ty = pure $ AbsN (teleNames old_tel) $ fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
    -- old_tel = Γ(x: D η v)Δ
    -- Γ1, (x : D η v)  ⊢ delta = (δ : Δ)
      (gamma1x,delta') = splitTelescopeAt (size old_tel - blockingVarNo x) old_tel
      delta = pure $ AbsN (teleNames gamma1x) $ delta'
      gamma1_size = (size gamma1x - 1)
      (gamma1,ExtendTel dType' _) = splitTelescopeAt gamma1_size gamma1x
  
    old_sides <- forM old_ps' $ \ ps -> do
      let vs = iApplyVars ps
      let tm = Def f $ patternsToElims ps
      xs <- forM vs $ \ v ->
          -- have to reduce these under the appropriate substitutions, otherwise non-normalizing(?)
            fmap (var v,) . reduce $ (inplaceS v iz `applySubst` tm, inplaceS v io `applySubst` tm)
      return $ concatMap (\(v,(l,r)) -> [(tNeg `apply` [argN v],l),(v,r)]) xs
    let
      gamma1ArgNames = teleArgNames gamma1
      deltaArgNames = teleArgNames delta'
    (params,xTel,dT) <- addContext gamma1 $ do
      Just (d, ps, _is) <- getDatatypeArgs . unDom =<< reduce dType'
      def <- getConstInfo d
      let dTy = defType def
      let Datatype{dataSort = s} = theDef def
      TelV tel _ <- telView dTy
      let params = AbsN (teleNames gamma1) ps
          xTel = AbsN (teleNames gamma1) (tel `apply` ps)
  
      dT <- runNamesT [] $ do
            s <- open $ AbsN (teleNames tel) s
            bindNArg (teleArgNames gamma1) $ \ g1 -> do
            bindNArg (teleArgNames $ unAbsN xTel) $ \ x -> do
            params <- pure params `applyN` (fmap unArg <$> g1)
            x      <- sequence x
            s <- s `applyN` map (pure . unArg) (params ++ x)
            pure $ El s $ Def d [] `apply` (params ++ x)
      return $ (params, xTel,dT)
  
    let
      xTelI = pure $ expTelescope interval <$> xTel
      xTelIArgNames = teleArgNames (unAbsN xTel) -- same names
  
    -- Γ1, φ, p, ψ, q, x0 ⊢ pat := trX p φ (trX q ψ x0)
    let trX' = bindNArg gamma1ArgNames $ \ g1 -> do
               bindNArg ([defaultArg "phi"] ++ xTelIArgNames) $ \ phi_p -> do
               bindNArg [defaultArg "x0"] $ \ x0 -> do
               param_args <- fmap (map (setHiding Hidden . fmap (unnamed . dotP))) $
                 pure params `applyN` (fmap unArg <$> g1)
               (phi, p) <- fromMaybe __IMPOSSIBLE__ . uncons <$> sequence phi_p
               x0 <- sequence x0
               pure $ DefP defaultPatternInfo q_trX $ param_args ++ p ++ [phi] ++ x0
        trX = (fmap . fmap . fmap) patternToTerm <$> trX'
    let pat' =
              bindN (map unArg gamma1ArgNames) $ \ g1 -> do
              bindN (map unArg $ ([defaultArg "phi"] ++ xTelIArgNames)) $ \ phi_p -> do
              bindN (map unArg $ ([defaultArg "psi"] ++ xTelIArgNames)) $ \ psi_q -> do
              bindN (map unArg $ [defaultArg "x0"]) $ \ x0 -> do
              -- (phi:p) <- sequence phi_p
              -- (psi:q) <- sequence psi_q
              -- x0 <- sequence x0
              let trX = trX' `applyN` g1
              trX `applyN` phi_p `applyN` [trX `applyN` psi_q `applyN` x0]
            --  pure $ trX $ p ++ [phi, defaultArg $ unnamed $ trX $ q ++ [psi] ++ x0]
        pat = (fmap . fmap . fmap . fmap) patternToTerm <$> pat'
    let deltaPat g1 phi p psi q x0 =
          delta `applyN` (g1 ++ [pat `applyN` g1 `applyN` (phi:p) `applyN` (psi:q) `applyN` [x0]])
    -- Ξ
    cTel <- runNamesT [] $
      abstractN (pure gamma1) $ \ g1 -> do
      abstractT "φ" (pure interval) $ \ phi -> do
      abstractN (xTelI `applyN` g1) $ \ p -> do
      abstractT "ψ" (pure interval) $ \ psi -> do
      abstractN (xTelI `applyN` g1) $ \ q -> do
      abstractT "x0" (pure dT `applyN` g1 `applyN` for q (\ f -> f <@> pure iz)) $ \ x0 -> do
      deltaPat g1 phi p psi q x0
  
    ps_ty_rhs <- runNamesT [] $ do
      bindN (map unArg gamma1ArgNames) $ \ g1 -> do
      bind "φ" $ \ phi -> do
      bindN (map unArg xTelIArgNames) $ \ p -> do
      bind "ψ" $ \ psi -> do
      bindN (map unArg xTelIArgNames) $ \ q -> do
      bind "x0" $ \ x0 -> do
      bindN (map unArg deltaArgNames) $ \ d -> do
      let
        ps :: NamesT TCM NAPs
        ps = old_ps `applyN` (g1
                            ++ [pat' `applyN` g1 `applyN` (phi:p) `applyN` (psi:q) `applyN` [x0]]
                            ++ d)
  
        rhsTy = old_ty `applyN` (g1
                            ++ [pat `applyN` g1 `applyN` (phi:p) `applyN` (psi:q) `applyN` [x0]]
                            ++ d)
  
      xTel <- (open =<<) $ pure xTel `applyN` g1
      q4_f <- (open =<<) $ bind "i" $ \ i -> lamTel $ bind "j" $ \ j -> do
        ty <- bind "i" $ \ _ -> xTel
        face <- max phi $ max (neg j) (neg i)
        base <- map defaultArg <$> appTel (sequence q) j
        u  <- liftM2 (,) (max j psi) $ bind "h" $ \ h -> do
                appTel (sequence p) (min j (min h i))
        xs <- fromRight __IMPOSSIBLE__ <$> do lift $ runExceptT $ transpSysTel' False ty [u] face base
        pure $ map unArg xs
      -- Ξ ⊢ pat_rec[0] = pat : D η v
      -- Ξ ⊢ pat_rec[1] = trX q4 (φ ∧ ψ) x0 : D η v
      -- Ξ ⊢ pat-rec[i] := trX (\ j → p (i ∨ j)) (i ∨ φ) (trX (q4_f i) (ψ ∧ (φ ∨ ~ i)) t)
      pat_rec <- (open =<<) $ bind "i" $ \ i -> do
            p_conn <- (mapM open =<<) $ lamTel $ bind "i" $ \ j -> sequence p `appTel` max i j
            q4_f' <- (mapM open =<<) $ absApp <$> q4_f <*> i
            trX `applyN` g1 `applyN` (max i phi:p_conn)
                `applyN` [trX `applyN` g1 `applyN` (min psi (max phi (neg i)):q4_f') `applyN` [x0]]
  
      let mkBndry args = do
              args1 <- (mapM open =<<) $ (absApp <$> args <*> pure io)
              -- faces ought to be constant on "j"
              faces <- pure (fmap (map fst) old_sides) `applyN` args1
              us <- forM (mapM (map snd) old_sides) $ \ u -> do
                    lam "j" $ \ j -> ilam "o" $ \ _ -> do
                      args <- (mapM open =<<) $ (absApp <$> args <*> j)
                      pure u `applyN` args
              forM (zip faces us) $ \ (phi,u) -> liftM2 (,) (open phi) (open u)
      let mkComp pr = bind "i" $ \ i -> do
            d_f <- (open =<<) $ bind "j" $ \ j -> do
              tel <- bind "j" $ \ j -> delta `applyN` (g1 ++ [pr `applyN` [i,j]])
              face <- min phi psi `max` (min i (max phi psi))
              j <- j
              d <- map defaultArg <$> sequence d
              lift $ covFillTele f tel face d j
            let args = bind "j" $ \ j -> do
                  g1 <- sequence g1
                  x <- pr `applyN` [i,neg j]
                  ys <- absApp <$> d_f <*> neg j
                  pure $ g1 ++ x:ys
            ty <- (open =<<) $ bind "j" $ \ j -> do
                 args <- (mapM open =<<) $ absApp <$> args <*> j
                 fmap unDom $ old_ty `applyN` args
            let face = max i (min phi psi)
            base <- (open =<<) $ do
              args' <- (mapM open =<<) $ absApp <$> args <*> pure iz
              fmap (Def f) $ (fmap patternsToElims <$> old_ps) `applyN` args'
            sys <- mkBndry args
            transpSys ty sys face base
  
      -- Ξ ⊢ δ_f[1] = tr (i. Δ[γ1,x = pat_rec[i]]) (φ ∧ ψ) δ
      -- Ξ ⊢ w0 := f old_ps[γ1,x = pat_rec[1] ,δ_f[1]] : old_t[γ1,x = pat_rec[1],δ_f[1]]
      -- Ξ ⊢ rhs := tr (i. old_t[γ1,x = pat_rec[~i], δ_f[~i]]) (φ ∧ ψ) w0 -- TODO plus sides.
      syspsi <- (open =<<) $ lam "i" $ \ i -> ilam "o" $ \ _ -> do
        c <- mkComp $ bindN ["i","j"] $ \ [i,j] -> do
          res <- bind "k" $ \ k -> do
            let phi_k = max phi (neg k)
            let p_k = for p $ \ p -> lam "h" $ \ h -> p <@> (min k h)
            data_ty <- pure dT `applyN` g1 `applyN` for p (\ p -> p <@> k)
            line1 <- trX `applyN` g1 `applyN` (phi_k:p_k) `applyN` [x0]
  
            line2 <- trX `applyN` g1
                         `applyN` (max phi_k j      : for p_k (\ p -> lam "h" $ \ h -> p <@> (max h j)))
                         `applyN`
                    [trX `applyN` g1
                         `applyN` (max phi_k (neg j): for p_k (\ p -> lam "h" $ \ h -> p <@> (min h j)))
                         `applyN` [x0]]
            pure (data_ty, [line1, line2])
          case res of
            Abs n (data_ty, [line1, line2]) -> do
              data_ty <- open $ Abs n data_ty
              line1   <- open $ Abs n line1
              line2   <- open $ Abs n line2
              let sys = [(neg i, lam "k" $ \ k -> ilam "o" $ \ _ -> absApp <$> line2 <*> k)
                        ,(neg j `max` j `max` i `max` phi, lam "k" $ \ k -> ilam "o" $ \ _ -> absApp <$> line1 <*> k)
                        ]
              transpSys data_ty sys (pure iz) x0
            _ -> __IMPOSSIBLE__
        absApp <$> pure c <*> i
      sysphi <- (open =<<) $ lam "i" $ \ i -> ilam "o" $ \ o -> do
        c <- mkComp $ bindN ["i","j"] $ \ _ij -> do
          trX `applyN` g1 `applyN` (psi:q) `applyN` [x0]
        absApp <$> pure c <*> i
      syse <- mkBndry $ bind "j" $ \ _ -> sequence $ g1 ++ [absApp <$> pat_rec <*> pure iz] ++ d
      let sys = syse ++ [(phi,sysphi)] ++ [(psi,syspsi)]
      w0 <- (open =<<) $ do
        let w = mkComp (bindN ["i","j"] $ \ [_i, j] -> absApp <$> pat_rec <*> j)
        absApp <$> w <*> pure iz
      let rhs = hcomp (unDom <$> rhsTy) sys w0
      (,,) <$> ps <*> rhsTy <*> rhs
    let (ps,ty,rhs) = unAbsN $ unAbs $ unAbsN $ unAbs $ unAbsN $ unAbs $ unAbsN $ ps_ty_rhs
    reportSDoc "tc.cover.trx.trx" 20 $ "trX-trX clause for" <+> prettyTCM f
    let c = Clause { clauseLHSRange  = noRange
                   , clauseFullRange = noRange
                   , clauseTel       = cTel
                   , namedClausePats = ps
                   , clauseBody      = Just rhs
                   , clauseType      = Just $ Arg (getArgInfo ty) (unDom ty)
                   , clauseCatchall    = empty
                   , clauseRecursive   = YesRecursive
                   , clauseUnreachable = Just False
                   , clauseEllipsis    = NoEllipsis
                   , clauseWhereModule = Nothing
                   }
    debugClause "tc.cover.trx.trx" c
    return $ c
  createMissingTrXHCompClause :: QName
                              -> QName
                              -> Arg Nat
                              -> BlockingVar
                              -> SplitClause
                              -> TCM Clause
  createMissingTrXHCompClause q_trX f n x old_sc = do
    let
     old_tel = scTel old_sc
     old_ps = fromSplitPatterns $ scPats old_sc
     old_t = fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
  
    reportSDoc "tc.cover.trx.hcomp" 20 $ "trX-hcomp clause for" <+> prettyTCM f
    reportSDoc "tc.cover.trx.hcomp" 20 $ nest 2 $ vcat $
      [ "old_tel:" <+> prettyTCM old_tel
      , "old_ps :" <+> addContext old_tel (prettyTCM $ patternsToElims old_ps)
      , "old_t  :" <+> addContext old_tel (prettyTCM old_t)
      ]
  
    -- old_tel = Γ1, (x : D η v), Δ
    -- α = boundary(old_ps)
    -- Γ1, (x : D η v), Δ ⊢ f old_ps : old_t [ α ↦ (f old_ps)[α] ]
  
    -- α' = boundary(old_ps[x = pat])
    -- Γ1, φ : I, p : Path X(η) _ v, ψ : I, u : I -> [ψ] → D η (p i0), u0 : D η (p i0) ⊢ pat := trX p φ (hcomp ψ u u0) : D η v
  
    -- Ξ = Γ1, φ : I, p : Path X(η) _ v, ψ : I, u : ..., u0 : D η (p i0), Δ[x = pat]
  
    -- Ξ ⊢ w1 := f old_ps[γ1,x = pat,δ] : old_t[γ1,x = pat,δ] -- the case we are defining. can only be used if specialized.
  
    -- Ξ ⊢ rhs : old_t[γ1,x = pat,δ] [ α' ↦ w1[α']
                                  -- , φ  ↦ w1[φ = i1, p = refl]   = f old_ps[γ1,x = hcomp ψ u u0    ,δ]
                                  -- , ψ  ↦ w1[ψ = i1]             = f old_ps[γ1,x = trX p φ (u i1 _),δ]
                                  -- ]
  
    -- Ξ ⊢ q2 := tr (i. Path X(η) (q i0) (p i)) φ q : Path X(η) (q i0) (p i1)
    -- Ξ ⊢ pat_rec[0] = pat : D η v
    -- Ξ ⊢ pat_rec[1] = trX q2 (φ ∧ ψ) x0 : D η v
    -- Ξ ⊢ pat-rec[i] := trX (\ j → q (i ∨ j)) (i ∨ φ) (trX (q2_f i) (ψ ∧ (φ ∨ ~ i)) t)
  
    -- Ξ ⊢ δ_f[1] = tr (i. Δ[γ1,x = pat_rec[i]]) (φ ∧ ψ) δ : Δ[γ1,x = pat_rec[1]]
    -- Ξ ⊢ w0 := f old_ps[γ1,x = pat_rec[1] ,δ_f[1]] : old_t[γ1,x = pat_rec[1],δ_f[1]]
    -- Ξ ⊢ rhs := tr (i. old_t[γ1,x = pat_rec[~i], δ_f[~i]]) (φ ∧ ψ) w0 -- TODO plus sides.
  
    q_hcomp <- fromMaybe __IMPOSSIBLE__ <$> getName' builtinHComp
    let
     old_tel = scTel old_sc
     old_ps = fromSplitPatterns $ scPats old_sc
     old_t = fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
  
    reportSDoc "tc.cover.trx.trx" 20 $ "trX-trX clause for" <+> prettyTCM f
    reportSDoc "tc.cover.trx.trx" 20 $ nest 2 $ vcat $
      [ "old_tel:" <+> prettyTCM old_tel
      , "old_ps :" <+> addContext old_tel (prettyTCM $ patternsToElims old_ps)
      , "old_t  :" <+> addContext old_tel (prettyTCM old_t)
      ]
  
    -- TODO: redo comments, the strategy changed.
    -- old_tel = Γ1, (x : D η v), Δ
    -- α = boundary(old_ps)
    -- Γ1, (x : D η v), Δ ⊢ f old_ps : old_t [ α ↦ (f old_ps)[α] ]
  
    -- α' = boundary(old_ps[x = pat])
    -- Γ1, φ : I, p : Path X(η) _ v, ψ : I, q : Path X(η) _ (p i0), x0 : D η (q i0) ⊢ pat := trX p φ (trX q ψ x0) : D η v
  
    -- Ξ = Γ1, φ : I, p : Path X(η) _ v, ψ : I, q : Path X(η) _ (p i0), x0 : D η (q i0), Δ[x = pat]
  
    -- Ξ ⊢ w1 := f old_ps[γ1,x = pat,δ] : old_t[γ1,x = pat,δ] -- the case we are defining. can only be used if specialized.
  
    -- Ξ ⊢ rhs : old_t[γ1,x = pat,δ] [ α' ↦ w1[α']
                                  -- , φ  ↦ w1[φ = i1, p = refl]
                                  -- , ψ  ↦ w1[ψ = i1, q = refl]
                                  -- ]
    -- Ξ ⊢ q2 := tr (i. Path X(η) (q i0) (p i)) φ q : Path X(η) (q i0) (p i1)
    -- Ξ ⊢ pat_rec[0] = pat : D η v
    -- Ξ ⊢ pat_rec[1] = trX q2 (φ ∧ ψ) x0 : D η v
    -- Ξ ⊢ pat-rec[i] := trX (\ j → p (i ∨ j)) (i ∨ φ) (trX (q2_f i) (ψ ∧ (φ ∨ ~ i)) t)
  
    -- Ξ ⊢ δ_f[1] = tr (i. Δ[γ1,x = pat_rec[i]]) (φ ∧ ψ) δ
    -- Ξ ⊢ w0 := f old_ps[γ1,x = pat_rec[1] ,δ_f[1]] : old_t[γ1,x = pat_rec[1],δ_f[1]]
    -- Ξ ⊢ rhs := tr (i. old_t[γ1,x = pat_rec[~i], δ_f[~i]]) (φ ∧ ψ) w0 -- TODO plus sides.
  
    interval <- elInf primInterval
    iz <- primIZero
    io <- primIOne
    tHComp <- primHComp
    tNeg <- primINeg
    let neg i = pure tNeg <@> i
    let min i j = cl primIMin <@> i <@> j
    let max i j = cl primIMax <@> i <@> j
    let
      old_tel = scTel old_sc
      old_ps' = AbsN (teleNames old_tel) $ fromSplitPatterns $ scPats old_sc
      old_ps = pure $ old_ps'
      old_ty = pure $ AbsN (teleNames old_tel) $ fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
    -- old_tel = Γ(x: D η v)Δ
    -- Γ1, (x : D η v)  ⊢ delta = (δ : Δ)
      (gamma1x,delta') = splitTelescopeAt (size old_tel - blockingVarNo x) old_tel
      delta = pure $ AbsN (teleNames gamma1x) $ delta'
      gamma1_size = (size gamma1x - 1)
      (gamma1,ExtendTel dType' _) = splitTelescopeAt gamma1_size gamma1x
  
    old_sides <- forM old_ps' $ \ ps -> do
      let vs = iApplyVars ps
      let tm = Def f $ patternsToElims ps
      xs <- forM vs $ \ v ->
          -- have to reduce these under the appropriate substitutions, otherwise non-normalizing(?)
            fmap (var v,) . reduce $ (inplaceS v iz `applySubst` tm, inplaceS v io `applySubst` tm)
      return $ concatMap (\(v,(l,r)) -> [(tNeg `apply` [argN v],l),(v,r)]) xs
    let
      gamma1ArgNames = teleArgNames gamma1
      deltaArgNames = teleArgNames delta'
    (params,xTel,dT) <- addContext gamma1 $ do
      Just (d, ps, _is) <- getDatatypeArgs . unDom =<< reduce dType'
      def <- getConstInfo d
      let dTy = defType def
      let Datatype{dataSort = s} = theDef def
      TelV tel _ <- telView dTy
      let params = AbsN (teleNames gamma1) ps
          xTel = AbsN (teleNames gamma1) (tel `apply` ps)
  
      dT <- runNamesT [] $ do
            s <- open $ AbsN (teleNames tel) s
            bindNArg (teleArgNames gamma1) $ \ g1 -> do
            bindNArg (teleArgNames $ unAbsN xTel) $ \ x -> do
            params <- pure params `applyN` (fmap unArg <$> g1)
            x      <- sequence x
            s <- s `applyN` map (pure . unArg) (params ++ x)
            pure $ El s $ Def d [] `apply` (params ++ x)
      return $ (params, xTel,dT)
  
    let
      xTelI = pure $ expTelescope interval <$> xTel
      xTelIArgNames = teleArgNames (unAbsN xTel) -- same names
  
    -- Γ1, φ, p, ψ, q, x0 ⊢ pat := trX p φ (trX q ψ x0)
    let trX' = bindNArg gamma1ArgNames $ \ g1 -> do
               bindNArg ([defaultArg "phi"] ++ xTelIArgNames) $ \ phi_p -> do
               bindNArg [defaultArg "x0"] $ \ x0 -> do
               param_args <- fmap (map (setHiding Hidden . fmap (unnamed . dotP))) $
                 pure params `applyN` (fmap unArg <$> g1)
               (phi, p) <- fromMaybe __IMPOSSIBLE__ . uncons <$> sequence phi_p
               x0 <- sequence x0
               pure $ DefP defaultPatternInfo q_trX $ param_args ++ p ++ [phi] ++ x0
        trX = (fmap . fmap . fmap) patternToTerm <$> trX'
    let
      hcompD' g1 v =
          bindNArg [argH "psi",argN "u", argN "u0"] $ \ x0 -> do
          x0 <- sequence x0
          LEl l t <- fromMaybe __IMPOSSIBLE__ <.> toLType =<< do pure dT `applyN` g1 `applyN` v
          let ty = map (fmap (unnamed . dotP) . argH) [Level l,t]
          pure $ DefP defaultPatternInfo q_hcomp $ ty ++ x0
    hcompD <- runNamesT [] $
              bindN (map unArg $ gamma1ArgNames) $ \ g1 -> do
              bindN (teleNames $ unAbsN $ xTel) $ \ v -> do
              fmap patternToTerm <$> hcompD' g1 v
    let pat' =
              bindN (map unArg gamma1ArgNames) $ \ g1 -> do
              bindN1 (fmap unArg (defaultArg "phi" :| xTelIArgNames)) $ \ phi_p -> do
              bindN ["psi","u","u0"] $ \ x0 -> do
              let trX = trX' `applyN` g1
              let p0 = for (List1.tail phi_p) $ \ p -> p <@> pure iz
              trX `applyN` (List1.toList phi_p) `applyN` [hcompD' g1 p0 `applyN` x0]
        pat = (fmap . fmap . fmap) patternToTerm <$> pat'
    let deltaPat g1 phi p x0 =
          delta `applyN` (g1 ++ [pat `applyN` g1 `applyN` (phi:p) `applyN` x0])
    -- Ξ
    cTel <- runNamesT [] $
      abstractN (pure gamma1) $ \ g1 -> do
      abstractT "φ" (pure interval) $ \ phi -> do
      abstractN (xTelI `applyN` g1) $ \ p -> do
      let p0 = for p $ \ p -> p <@> pure iz
      let ty = pure dT `applyN` g1 `applyN` p0
      abstractT "ψ" (pure interval) $ \ psi -> do
      abstractT "u" (pure interval --> pPi' "o" psi (\ _ -> ty)) $ \ u -> do
      abstractT "u0" ty $ \ u0 -> do
      deltaPat g1 phi p [psi,u,u0]
  
    ps_ty_rhs <- runNamesT [] $ do
      bindN (map unArg gamma1ArgNames) $ \ g1 -> do
      bind "φ" $ \ phi -> do
      bindN (map unArg xTelIArgNames) $ \ p -> do
      bind "ψ" $ \ psi -> do
      bind "u" $ \ u -> do
      bind "u0" $ \ u0 -> do
      bindN (map unArg deltaArgNames) $ \ d -> do
      let
        x0 :: Vars TCM
        x0 = [psi,u,u0]
        ps :: NamesT TCM NAPs
        ps = old_ps `applyN` (g1
                            ++ [pat' `applyN` g1 `applyN` (phi:p) `applyN` x0]
                            ++ d)
  
        rhsTy = old_ty `applyN` (g1
                            ++ [pat `applyN` g1 `applyN` (phi:p) `applyN` x0]
                            ++ d)
  
      xTel <- (open =<<) $ pure xTel `applyN` g1
      -- Ξ ⊢ pat-rec[i] := trX .. (hfill ... (~ i))
      pat_rec <- (open =<<) $ bind "i" $ \ i -> do
            let tr x = trX `applyN` g1 `applyN` (phi:p) `applyN` [x]
            let p0 = for p $ \ p -> p <@> pure iz
            tr (hcomp (pure dT `applyN` g1 `applyN` p0)
                      [(psi,lam "j" $ \ j -> u <@> (min j (neg i)))
                      ,(i  ,lam "j" $ \ _ -> ilam "o" $ \ _ -> u0)]
                      u0)
      --   args : (i.old_tel)  -> ...
      let mkBndry args = do
              args1 <- (mapM open =<<) $ (absApp <$> args <*> pure io)
              -- faces ought to be constant on "j"
              faces <- pure (fmap (map fst) old_sides) `applyN` args1
              us <- forM (mapM (map snd) old_sides) $ \ u -> do
                    lam "j" $ \ j -> ilam "o" $ \ _ -> do
                      args <- (mapM open =<<) $ (absApp <$> args <*> j)
                      pure u `applyN` args
              forM (zip faces us) $ \ (phi,u) -> liftM2 (,) (open phi) (open u)
      rhs <- do
        d_f <- (open =<<) $ bind "j" $ \ j -> do
          tel <- bind "j" $ \ j -> delta `applyN` (g1 ++ [absApp <$> pat_rec <*> j])
          let face = iz
          j <- j
          d <- map defaultArg <$> sequence d
          lift $ covFillTele f tel face d j
        let args = bind "j" $ \ j -> do
              g1 <- sequence g1
              x <- absApp <$> pat_rec <*> neg j
              ys <- absApp <$> d_f <*> neg j
              pure $ g1 ++ x:ys
        ty <- (open =<<) $ bind "j" $ \ j -> do
             args <- (mapM open =<<) $ absApp <$> args <*> j
             fmap unDom $ old_ty `applyN` args
        let face = pure iz
        othersys <- (open =<<) $ lam "j" $ \ j -> ilam "o" $ \ _ -> do
          args' <- (mapM open =<<) $ absApp <$> args <*> j
          fmap (Def f) $ (fmap patternsToElims <$> old_ps) `applyN` args'
        sys <- mkBndry args
        let
          -- we could specialize all of sysphi/syspsi/base to compute
          -- away trX or the hcomp respectively, should lead to
          -- smaller/more efficient terms.
          --
          -- we could also ditch sysphi completely,
          -- as the computation rule for hcomp would achieve the same.
          sysphi = othersys
          syspsi = othersys
        base <- (open =<<) $ do
          args' <- (mapM open =<<) $ absApp <$> args <*> pure iz
          fmap (Def f) $ (fmap patternsToElims <$> old_ps) `applyN` args'
        transpSys ty ((phi,sysphi):(psi,syspsi):sys) face base
      (,,) <$> ps <*> rhsTy <*> pure rhs
    let (ps,ty,rhs) = unAbsN $ unAbs $ unAbs $ unAbs $ unAbsN $ unAbs $ unAbsN $ ps_ty_rhs
    reportSDoc "tc.cover.trx.hcomp" 20 $ "trX-hcomp clause for" <+> prettyTCM f
    let c = Clause { clauseLHSRange  = noRange
                   , clauseFullRange = noRange
                   , clauseTel       = cTel
                   , namedClausePats = ps
                   , clauseBody      = Just rhs
                   , clauseType      = Just $ Arg (getArgInfo ty) (unDom ty)
                   , clauseCatchall    = empty
                   , clauseRecursive   = YesRecursive
                   , clauseUnreachable = Just False
                   , clauseEllipsis    = NoEllipsis
                   , clauseWhereModule = Nothing
                   }
    debugClause "tc.cover.trx.hcomp" c
    return c
  createMissingTrXConClause :: QName -- trX
                              -> QName -- f defined
                              -> Arg Nat
                              -> BlockingVar
                              -> SplitClause
                              -> QName -- constructor name
                              -> UnifyEquiv
                              -> TCM Clause
  createMissingTrXConClause q_trX f n x old_sc c (UE gamma gamma' xTel u v rho tau leftInv) = do
    reportSDoc "tc.cover.trxcon" 20 $ "trX-con clause for" <+> prettyTCM f <+> "with con" <+> prettyTCM c
    reportSDoc "tc.cover.trxcon" 20 $ nest 2 $ vcat $
      [ "gamma" <+> prettyTCM gamma
      , "gamma'" <+> prettyTCM gamma'
      , "xTel" <+> addContext gamma (prettyTCM xTel)
      , "u"  <+> addContext gamma (prettyTCM u)
      , "v"  <+> addContext gamma (prettyTCM v)
      , "rho" <+> addContext gamma' (prettyTCM rho)
      ]
  
    Constructor{conSrcCon = chead} <- theDef <$> getConstInfo c
  
    -- = TheInfo $ UE delta1' eqTel (map unArg conIxs) (map unArg givenIxs) rho0 tau leftInv
  
    -- η : Params_D ⊢ c : (a : Args(η)) → D η (ξ(η,a))
  
    -- scTel old_sc = Γ1, (x : D η v), Δ
    -- Γ1, (x : D η v), Δ ⊢ f old_ps : old_t [α(γ1,x,δ) ↦ e(γ1,x,δ)]
  
    -- Γ = Γ1, a : Args(η)
    -- Γ ⊢ u = ξ(η,a)
    -- Γ ⊢ c a : D η u
  
    -- Γ' ⊢ ρ : Γ
  
    -- Γ' ⊢ u[ρ] = v[ρ] : X(η)[ρ]
  
    -- Γ' ⊢ c a[ρ] : (D η v)[ρ]
  
    -- Γ' ⊢ ρx := ρ,x = c a[ρ] : Γ,(x : D η v)
  
    -- Γ',Δ[ρx] ⊢ old_t[ρx]
    -- Γ',Δ[ρx] ⊢ f old_ps[ρx] : old_t[ρx] [α[ρx] ↦ e[γ1,x,δ][ρx]]
  
    -- Γ,(φ : I),(p : Path X(η) u v) ⊢ τ : Γ'
  
    -- Γ,(φ : I),(p : Path X(η) u v) ⊢ [ρx][τ] = [ρ[τ], x = c a[ρ[τ]]] : Γ,(x : D η v)
  
    -- Γ,(φ : I),(p : Path X(η) u v) ⊢ leftInv : ρ[τ],i1,refl ≡ idS : Γ,(φ : I),(p : Path X(η) u v)
  
    -- Γ,(φ : I),(p : Path X(η) u v)| (i : I) ⊢ leftInv i : Γ,(φ : I),(p : Path X(η) u v)
  
    -- Γ,(φ : I),(p : Path X(η) u v) ⊢ leftInv i0 = ρ[τ],i1,refl : Γ,(φ : I),(p : Path X(η) u v)
    -- Γ,(φ : I),(p : Path X(η) u v) ⊢ leftInv i1 = γ   ,φ ,p    : Γ,(φ : I),(p : Path X(η) u v)
    --                                 leftInv[φ = i1][i] = idS
  
    -- Γ,(φ : I),(p : Path X(η) u v),Δ[ρx][τ] ⊢ τ' = liftS |Δ[ρx]| τ : Γ',Δ[ρx]
  
    -- Γ,(φ : I),(p : Path X(η) u v),Δ[ρx][τ] ⊢
    --            w := f old_ps[γ1[ρ[τ]],x = c a[ρ[τ]],δ] : old_t[ρx][τ'] = old_t[γ1[ρ[τ]],x = c a[ρ[τ]],δ]
  
    -- Γ,(φ : I),(p : Path X(η) u v),Δ[ρx][τ], α(γ1,x,δ)[ρx][τ'] ⊢ w = e(γ1,x,δ)[ρx][τ']
  
    -- Γ,(φ : I),(p : Path X(η) u v) ⊢ pat := trX p φ (c a) : D η v
  
  
    -- Ξ := Γ,(φ : I),(p : Path X(η) u v),(δ : Δ[x = pat])
  
    -- Ξ ⊢ δ_f[1] = trTel (i. Δ[γ1[leftInv (~ i)], pat[leftInv (~i)]]) φ δ : Δ[ρ[τ], x = c a[ρ[τ]]]
  
    -- Ξ ⊢ w[δ_f[1]] : old_t[γ1[ρ[τ]],x = c a[ρ[τ]],δ_f[1]]
    -- Ξ, α(γ1,x,δ)[ρx][τ'][δ = δ_f[1]] ⊢ w[δ_f[1]] = e(γ1,x,δ)[ρx][τ'][δ_f[1]]
  
    -- Ξ, α(γ1[ρ[τ]],c a[ρ[τ]],δ_f[1]) ⊢ w[δ_f[1]] = e(γ1[ρ[τ]],c a[ρ[τ]],δ_f[1])
  
    -- Recap:
    -- Γ1, (x : D η v), Δ ⊢ f old_ps : old_t [α(γ1,x,δ) ↦ e(γ1,x,δ)]
    -- Ξ := Γ,(φ : I),(p : Path X(η) u v),(δ : Δ[x = pat])
    -- Ξ ⊢ δ_f[1] := trTel (i. Δ[γ1[leftInv (~ i)], pat[leftInv (~i)]]) φ δ : Δ[ρ[τ], x = c a[ρ[τ]]]
    -- Γ,(φ : I),(p : Path X(η) u v),Δ[ρx][τ] ⊢
    --            w := f old_ps[γ1[ρ[τ]],x = c a[ρ[τ]],δ] : old_t[ρx][τ'] = old_t[γ1[ρ[τ]],x = c a[ρ[τ]],δ]
    -- Γ,(φ : I),(p : Path X(η) u v) ⊢ pat := trX p φ (c a) : D η v
  
  
    -- Ξ ⊢ ?rhs : old_t[γ1,x = pat,δ] [α(γ1,pat,δ) ↦ e(γ1,pat,δ)
    --                               ,φ           ↦ w
    --                               ]
  
    -- ?rhs := transp (i. old_t[γ1[leftInv i],x = pat[leftInv i], δ_f[~i]]) φ (w[δ_f[1]])
  
    -- we shall consider α(γ1,pat,δ) = α(γ1[ρ[τ]],c a[ρ[τ]],δ_f[1])
    -- also rather than (p : Path X(η) u v) we'll have (p : I -> X(η)), same as the type of trX.
  
    iz <- primIZero
    interval <- elInf primInterval
    let
        old_tel = scTel old_sc
        old_ps = pure $ AbsN (teleNames old_tel) $ fromSplitPatterns $ scPats old_sc
        old_ty = pure $ AbsN (teleNames old_tel) $ fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
    -- old_tel = Γ(x: D η v)Δ
    -- Γ1, (x : D η v)  ⊢ delta = (δ : Δ)
        (gamma1x,delta') = splitTelescopeAt (size old_tel - blockingVarNo x) old_tel
    let
      gammaArgNames = teleArgNames gamma
      deltaArgNames = teleArgNames delta'
    let
      xTelI = pure $ AbsN (teleNames gamma) $ expTelescope interval xTel
      delta = pure $ AbsN (teleNames gamma1x) $ delta'
      gamma1_size = (size gamma1x - 1)
      (gamma1,ExtendTel dType' _) = splitTelescopeAt gamma1_size gamma1x
    params <- addContext gamma1 $ do
      Just (_d, ps, _is) <- getDatatypeArgs . unDom =<< reduce dType'
      return $ AbsN (teleNames gamma1) ps
    -- Γ, φ , p ⊢ pat := trX p φ (c a)
    let pat' =
              bindNArg gammaArgNames $ \ g1_args -> do
              bindNArg ([defaultArg "phi"] ++ teleArgNames xTel) $ \ phi_p -> do
              let (g1,args) = splitAt gamma1_size g1_args
              (phi, p) <- fromMaybe __IMPOSSIBLE__ . uncons <$> sequence phi_p
              args <- sequence args
              let cargs = defaultArg $ unnamed $ ConP chead noConPatternInfo args
              -- Amy (2022-11-06): Set the parameters to quantity-0.
              param_args <- fmap (map (setQuantity (Quantity0 Q0Inferred) . setHiding Hidden . fmap (unnamed . dotP))) $
                pure params `applyN` take gamma1_size (fmap unArg <$> g1_args)
              pure $ DefP defaultPatternInfo q_trX $ param_args ++ p ++ [phi,cargs]
        pat = (fmap . fmap) patternToTerm <$> pat'
        pat_left' = (fmap . fmap) (Abs "i" . (applySubst leftInv)) <$> pat
        g1_left' = bindN (map unArg gammaArgNames) $ \ g1_args -> do
                  bindN (map unArg $ [defaultArg "phi"] ++ teleArgNames xTel) $ \ phi_p -> do
                  g1 <- sequence $ take gamma1_size g1_args :: NamesT TCM [Term]
                  pure $ Abs "i" (applySubst leftInv g1)
  
    gamma <- return $ pure gamma
    let deltaPat g1_args phi p =
          delta `applyN` (take gamma1_size g1_args ++ [pat `applyN` g1_args `applyN` (phi:p)])
    let neg i = cl primINeg <@> i
    -- Ξ
    cTel <- runNamesT [] $
      abstractN gamma $ \ g1_args -> do
      abstractT "φ" (pure interval) $ \ phi -> do
      abstractN (xTelI `applyN` g1_args) $ \ p -> do
      deltaPat g1_args phi p
    ps_ty_rhs <- runNamesT [] $ do
      bindN (map unArg gammaArgNames) $ \ g1_args -> do
      bind "phi" $ \ phi -> do
      bindN (teleNames xTel) $ \ p -> do
      bindN (map unArg $ deltaArgNames) $ \ d -> do
      let
        g1_left = g1_left' `applyN` g1_args `applyN` (phi:p)
        pat_left = pat_left' `applyN` g1_args `applyN` (phi:p)
        g1 :: Vars TCM
        g1 = take gamma1_size g1_args
  
        args :: Vars TCM
        args = drop gamma1_size g1_args
  
        ps :: NamesT TCM NAPs
        ps = old_ps `applyN` (g1 ++ [pat' `applyN` g1_args `applyN` (phi:p)] ++ d)
  
        rhsTy = old_ty `applyN` (g1 ++ [pat `applyN` g1_args `applyN` (phi:p)] ++ d)
  
      -- (i. Δ[γ1[leftInv (~ i)], pat[leftInv (~i)]])
      delta_f <- (open =<<) $ bind "i" $ \ i -> do
        let ni = neg i
        dargs <- (mapM open =<<) $ do
          xs <- absApp <$> g1_left <*> ni
          y <- absApp <$> pat_left <*> ni
          return $ xs ++ [y]
        delta `applyN` dargs
  
      --  trFillTel (i. Δ[γ1[leftInv (~ i)], pat[leftInv (~i)]]) φ δ
      d_f <- (open =<<) $ bind "i" $ \ i -> do
        delta_f <- delta_f
        phi <- phi
        d <- map defaultArg <$> sequence d
        i <- i
        lift $ covFillTele f delta_f phi d i
  
      -- w = Def f (old_ps[g1_left[i],pat_left[i],d_f[~ i]])
      w <- (open =<<) $ bind "i" $ \ i -> do
        psargs <- (mapM open =<<) $ do
          xs <- absApp <$> g1_left <*> i
          y <- absApp <$> pat_left <*> i
          zs <- absApp <$> d_f <*> neg i
          return $ xs ++ [y] ++ zs
        ps <- (fmap patternsToElims <$> old_ps) `applyN` psargs
        pure $ Def f ps
  
  
      -- (i. old_t[γ1[leftInv i],x = pat[leftInv i], δ_f[~i]])
      ty <- (open =<<) $ bind "i" $ \ i -> do
        tyargs <- (mapM open =<<) $ do
          xs <- absApp <$> g1_left <*> i
          y <- absApp <$> pat_left <*> i
          zs <- absApp <$> d_f <*> neg i
          return $ xs ++ [y] ++ zs
        fmap unDom $ old_ty `applyN` tyargs
  
      sys <- do
        sides <- do
          neg <- primINeg
          io <- primIOne
          vs <- iApplyVars <$> ps
          tm <- w
          xs <- forM vs $ \ v ->
              -- have to reduce these under the appropriate substitutions, otherwise non-normalizing(?)
                fmap (var v,) . reduce $ (inplaceS v iz `applySubst` tm, inplaceS v io `applySubst` tm)
          return $ concatMap (\(v,(l,r)) -> [(neg `apply` [argN v],l),(v,r)]) xs
        forM sides $ \ (psi,u') -> do
          u' <- open u'
          u <- lam "i" $ \ i -> ilam "o" $ \ o -> absApp <$> u' <*> i
          (,) <$> open psi <*> open u
  
      let rhs = transpSys ty sys phi (absApp <$> w <*> pure iz)
  
      (,,) <$> ps <*> rhsTy <*> rhs
  
    let (ps,ty,rhs) = unAbsN $ unAbsN $ unAbs $ unAbsN $ ps_ty_rhs
    qs <- mapM (fmap (fromMaybe __IMPOSSIBLE__) . getName') [builtinINeg, builtinIMax, builtinIMin]
    rhs <- addContext cTel $
             locallyReduceDefs (OnlyReduceDefs (Set.fromList $ q_trX : qs)) $ normalise rhs
    let cl = Clause { clauseLHSRange  = noRange
                    , clauseFullRange = noRange
                    , clauseTel       = cTel
                    , namedClausePats = ps
                    , clauseBody      = Just rhs
                    , clauseType      = Just $ Arg (getArgInfo ty) (unDom ty)
                    , clauseCatchall    = empty
                    , clauseRecursive   = YesRecursive
                    , clauseUnreachable = Just False
                    , clauseEllipsis    = NoEllipsis
                    , clauseWhereModule = Nothing
                    }
  
  
    debugClause "tc.cover.trxcon" cl
  
    reportSDoc "tc.cover.trxcon" 20 $ vcat $
      [ "clause:"
      ,  nest 2 $ prettyTCM . QNamed f $ cl
      ]
  
    let mod =
          setRelevance irrelevant $  -- See #5611.
          getModality $ fromMaybe __IMPOSSIBLE__ $ scTarget old_sc
    -- we follow what `cover` does when updating the modality from the target.
    applyModalityToContext mod $ do
      unlessM (hasQuantity0 <$> viewTC eQuantity) $ do
      reportSDoc "tc.cover.trxcon" 20 $ text "testing usable at mod: " <+> pretty mod
      addContext cTel $ usableAtModality IndexedClause mod rhs
  
    return cl
  
  {-
    OLD leftInv case
    -- Γ,(φ : I),(p : Path A u v) ⊢ leftInv : ρ[τ] ≡ wkS 2 : Γ
    -- Γ,(φ : I),(p : Path A u v)(i : I) ⊢ leftInv i : Γ
    -- Γ,(φ : I),(p : Path A u v) ⊢ leftInv i0 = ρ[τ] : Γ
    -- Γ,(φ : I),(p : Path A u v) ⊢ leftInv i1 = wkS 2 : Γ
    -- leftInv[φ = i1][i] = wkS 2
  
    -- Γ,(φ : I),(p : Path A u v),Δ[ρ,x = refl][τ] ⊢ τ' = liftS |Δ[ρ,x = refl]| τ : Γ',Δ[ρ,x = refl]
  
    -- Γ,(φ : I),(p : Path A u v),Δ[ρ,x = refl][τ] ⊢ w = f old_ps[ρ,x = refl][τ'] : old_t[ρ,x = refl][τ']
  
    -- Γ,(φ : I),(p : Path A u v) | (i : I) ⊢ μ = ⟨ (φ ∨ ~ i) , (\ j → p (i ∧ j)) ⟩ : Id A u (p i) =?= (Id A u v)[leftInv (~ i)]
                                    μ[0] = ⟨ 1 , (\ _ → u[ρ[τ]]) ⟩
                                    μ[1] = ⟨ φ , p               ⟩
    -- Γ,(φ : I),(p : Path A u v),(δ : Δ[x = ⟨ φ , p ⟩]) ⊢ vecTransp (i. Δ[leftInv (~ i),μ[i]]) φ δ : Δ[ρ[τ], x = refl u[ρ[τ]]]
  -}
  
  -- | Append an hcomp clause to the clauses of a function.
  createMissingHCompClause
    :: QName
         -- ^ Function name.
    -> Arg Nat -- ^ index of hcomp pattern
    -> BlockingVar -- ^ Blocking var that lead to hcomp split.
    -> SplitClause -- ^ Clause before the hcomp split
    -> SplitClause
         -- ^ Clause to add.
    -> [Clause]
     -> TCM ([(SplitTag,CoverResult)], [Clause])
  createMissingHCompClause f n x old_sc (SClause tel ps _sigma' _cps (Just t)) cs = setCurrentRange f $ do
    reportSDoc "tc.cover.hcomp" 20 $ addContext tel $ text "Trying to create right-hand side of type" <+> prettyTCM t
    reportSDoc "tc.cover.hcomp" 30 $ addContext tel $ text "ps = " <+> prettyTCMPatternList (fromSplitPatterns ps)
    reportSDoc "tc.cover.hcomp" 30 $ text "tel = " <+> prettyTCM tel
  
    io      <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIOne
    iz      <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIZero
    let
      cannotCreate :: MonadTCError m => Doc -> Closure (Abs Type) -> m a
      cannotCreate doc t = do
        typeError . SplitError $ CannotCreateMissingClause f (tel,fromSplitPatterns ps) doc t
    let old_ps = patternsToElims $ fromSplitPatterns $ scPats old_sc
        old_t  = fromJust $ scTarget old_sc
        old_tel = scTel old_sc
        -- old_tel = Γ(x:H)Δ
        -- Γ(x:H)Δ ⊢ old_t
        -- vs = iApplyVars old_ps
        -- [ α ⇒ b ] = [(i,f old_ps (i=0),f old_ps (i=1)) | i <- vs]
  
        -- Γ(x:H)(δ : Δ) ⊢ [ α ⇒ b ]
        -- Γ(x:H)Δ ⊢ f old_ps : old_t [ α ⇒ b ]
        -- Γ,φ,u,u0,Δ(x = hcomp φ u u0) ⊢ rhs_we_define : (old_t[ α ⇒ b ])(x = hcomp φ u u0)
  
        -- Extra assumption:
        -- tel = Γ,φ,u,u0,Δ(x = hcomp φ u u0),Δ'
        -- ps = old_ps[x = hcomp φ u u0],ps'
        -- with Δ' and ps' introduced by fixTarget.
        -- So final clause will be:
        -- tel ⊢ ps ↦ rhs_we_define{wkS ..} ps'
  
        getLevel t = do
          s <- reduce $ getSort t
          case s of
            Type l -> pure (Level l)
  
            -- Impossible since we only have HITs in Type:
            s -> do
              reportSDoc "tc.cover.hcomp" 20 $ vcat
                [ "sort of blocking variable when creating hcomp clause is not Type"
                , nest 2 ("t =" <+> prettyTCM t)
                , nest 2 ("s =" <+> prettyTCM s)
                , ""
                , "clause:"
                , nest 2 $ prettyTCM (QNamed f empty{ clauseTel = tel, namedClausePats = fromSplitPatterns ps })
                ]
              __IMPOSSIBLE__
  
        -- Γ ⊢ hdelta = (x : H)(δ : Δ)
        (gamma,hdelta@(ExtendTel hdom delta)) = splitTelescopeAt (size old_tel - (blockingVarNo x + 1)) old_tel
  
        -- Γ,φ,u,u0,Δ(x = hcomp φ u u0) ⊢
        (working_tel,_deltaEx) = splitTelescopeAt (size gamma + 3 + size delta) tel
  
        -- Γ,φ,u,u0,(x:H)(δ : Δ) ⊢ rhoS : Γ(x:H)(δ : Δ)
        {- rhoS = liftS (size hdelta) $ raiseS 3 -}
        vs = iApplyVars (scPats old_sc)
  
    -- Γ(x:H)(δ : Δ) ⊢ [ α ⇒ b ] = [(i,f old_ps (i=0),f old_ps (i=1)) | i <- vs]
    alphab <- forM vs $ \ i -> do
                 let
                   -- Γ(x:H)(δ : Δ) ⊢
                   tm = Def f old_ps
                 -- TODO only reduce IApply _ _ (0/1), as to avoid termination problems
                 (l,r) <- reduce (inplaceS i iz `applySubst` tm, inplaceS i io `applySubst` tm)
                 return $ (var i, (l, r))
  
  
  
    cl <- do
      (ty,rhs) <- addContext working_tel $ do
        -- Γ(x:H)Δ ⊢ g = f old_ps : old_t [ α ⇒ b ]
        -- Γ(x:H)(δ : Δ) ⊢ [ α ⇒ b ]
        -- Γ,φ,u,u0 ⊢ Δf = i.Δ[x = hfill φ u u0 i]
        -- Γ,φ,u,u0,δ : Δ(x = hcomp φ u u0) ⊢ δ_fill     = i.tFillTel (i. Δf[~i]) δ (~ i) : i.Δf[i]
        -- Γ,φ,u,u0,δ : Δ(x = hcomp φ u u0) ⊢ old_t_fill = i.old_t[x = hfill φ u u0 i, δ_fill[i]]
        -- Γ,φ,u,u0,δ : Δ(x = hcomp φ u u0) ⊢ comp (\ i. old_t_fill[i])
        --                 (\ i. [ φ ↦ g[x = hfill φ u u0 i,δ_fill[i]] = g[u i,δ_fill[i]]
        --                         α ↦ b[x = hfill φ u u0 i,δ_fill[i]]
        --                        ])
        --                 (g[x = u0,δ_fill[0]]) : old_t[x = hcomp φ u u0,δ]
  
        runNamesT [] $ do
            tPOr <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinPOr
            tIMax <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIMax
            tIMin <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIMin
            tINeg <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinINeg
            tHComp <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinHComp
            tTrans <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinTrans
            extra_ps <- open $ patternsToElims $ fromSplitPatterns $ drop (length old_ps) ps
            let
              ineg j = pure tINeg <@> j
              imax i j = pure tIMax <@> i <@> j
              trFillTel' a b c d = do
                m <- trFillTel <$> a <*> b <*> c <*> d
                x <- lift $ runExceptT m
                case x of
                  Left bad_t -> cannotCreate "Cannot transport with type family:" bad_t
                  Right args -> return args
            comp <- mkCompLazy "hcompClause"
            let
              hcomp la bA phi u u0 = pure tHComp <#> la <#> bA
                                                 <#> phi
                                                 <@> u
                                                 <@> u0
  
              hfill la bA phi u u0 i = hcomp la bA
                                                 (pure tIMax <@> phi <@> (pure tINeg <@> i))
                                                 (lam "j" $ \ j -> pure tPOr <#> la <@> phi <@> (pure tINeg <@> i) <#> ilam "o" (\ _ -> bA)
                                                       <@> ilam "o" (\ o -> u <@> (pure tIMin <@> i <@> j) <..> o)
                                                       <@> ilam "o" (\ _ -> u0)
                                                     )
                                                 u0
            -- Γ,φ,u,u0,(δ : Δ(x = hcomp φ u u0)) ⊢ hcompS : Γ(x:H)(δ : Δ)
            hcompS <- lift $ do
              hdom <- pure $ raise 3 hdom
              let
                [phi,u,u0] = map (pure . var) [2,1,0]
                htype = pure $ unEl . unDom $ hdom
                lvl = getLevel $ unDom hdom
              hc <- pure tHComp <#> lvl <#> htype
                                        <#> phi
                                        <@> u
                                        <@> u0
              return $ liftS (size delta) $ hc `consS` raiseS 3
            -- Γ,φ,u,u0,Δ(x = hcomp phi u u0) ⊢ raise 3+|Δ| hdom
            hdom <- pure $ raise (3 + size delta) hdom
            htype <- open $ unEl . unDom $ hdom
            lvl <- open =<< (lift . getLevel $ unDom hdom)
  
            -- Γ,φ,u,u0,Δ(x = hcomp phi u u0) ⊢
            let vr = open . raise (size delta) . var
            phi <- vr 2
            u   <- vr 1
            u0  <- vr 0
            -- Γ,x,Δ ⊢ f old_ps
            -- Γ ⊢ abstract hdelta (f old_ps)
            g <- open $ raise (3 + size delta) $ abstract hdelta (Def f old_ps)
            old_t <- open $ raise (3 + size delta) $ abstract hdelta (unDom old_t)
            let bapp a x = lazyAbsApp <$> a <*> x
            (delta_fill :: NamesT TCM (Abs Args)) <- (open =<<) $ do
              -- Γ,φ,u,u0,Δ(x = hcomp phi u u0) ⊢ x.Δ
              delta <- open $ raise (3 + size delta) delta
              -- Γ,φ,u,u0,Δ(x = hcomp phi u u0) ⊢ i.Δ(x = hfill phi u u0 (~ i))
              deltaf <- open =<< bind "i" (\ i ->
                             (delta `bapp` hfill lvl htype phi u u0 (ineg i)))
              -- Γ,φ,u,u0,Δ(x = hcomp phi u u0) ⊢ Δ(x = hcomp phi u u0) = Δf[0]
              args <- (open =<<) $ teleArgs <$> (lazyAbsApp <$> deltaf <*> pure iz)
              bind "i" $ \ i -> addContext ("i" :: String) $ do -- for error messages.
                -- Γ,φ,u,u0,Δ(x = hcomp phi u u0),(i:I) ⊢ ... : Δ(x = hfill phi u u0 i)
                trFillTel' deltaf (pure iz) args (ineg i)
            let
              apply_delta_fill i f = apply <$> f <*> (delta_fill `bapp` i)
              call v i = apply_delta_fill i $ g <@> v
            ty <- do
                  return $ \ i -> do
                      v <- hfill lvl htype phi u u0 i
                      hd <- old_t
                      args <- delta_fill `bapp` i
                      lift $ piApplyM hd $ Arg (domInfo hdom) v : args
            ty_level <- do
              t <- bind "i" $ \ x -> ty x
              s <- reduce $ getSort (absBody t)
              reportSDoc "tc.cover.hcomp" 20 $ text "ty_level, s = " <+> prettyTCM s
              case s of
                Type l -> open =<< lam "i" (\ _ -> pure $ Level l)
                _      -> do cl <- liftTCM (buildClosure t)
                             liftTCM (cannotCreate "Cannot compose with type family:" cl)
  
            let
              pOr_ty i phi psi u0 u1 = pure tPOr <#> (ty_level <@> i)
                                                 <@> phi <@> psi
                                                 <#> ilam "o" (\ _ -> unEl <$> ty i) <@> u0 <@> u1
            alpha <- do
              vars <- mapM (open . applySubst hcompS . fst) alphab
              return $ foldr (imax . (\ v -> v `imax` ineg v)) (pure iz) vars
  
            -- Γ,φ,u,u0,Δ(x = hcomp φ u u0) ⊢ b : (i : I) → [α] -> old_t[x = hfill φ u u0 i,δ_fill[i]]
            b <- do
               sides <- forM alphab $ \ (psi,(side0,side1)) -> do
                  psi <- open $ hcompS `applySubst` psi
                  let f = open . raise (3 + size delta) . abstract hdelta
                  side0 <- f side0
                  side1 <- f side1
                  return $ (ineg psi `imax` psi, \ i -> pOr_ty i (ineg psi) psi (ilam "o" $ \ _ -> apply_delta_fill i $ side0 <@> hfill lvl htype phi u u0 i)
                                                              (ilam "o" $ \ _ -> apply_delta_fill i $ side1 <@> hfill lvl htype phi u u0 i))
               let recurse []           i = __IMPOSSIBLE__
                   recurse [(psi,u)]    i = u i
                   recurse ((psi,u):xs) i = pOr_ty i psi (foldr (imax . fst) (pure iz) xs) (u i) (recurse xs i)
               return $ recurse sides
  
            ((,) <$> ty (pure io) <*>) $ do
              comp ty_level
                 (lam "i" $ fmap unEl . ty)
                             (phi `imax` alpha)
                             (lam "i" $ \ i ->
                                 let rhs = (ilam "o" $ \ o -> call (u <@> i <..> o) i)
                                 in if null alphab then rhs else
                                     pOr_ty i phi alpha rhs (b i)
                             )
                             (call u0 (pure iz))
      reportSDoc "tc.cover.hcomp" 20 $ text "old_tel =" <+> prettyTCM tel
      let n = size tel - (size gamma + 3 + size delta)
      reportSDoc "tc.cover.hcomp" 20 $ text "n =" <+> text (show n)
      (TelV deltaEx t,bs) <- telViewUpToPathBoundary' n ty
      rhs <- pure $ raise n rhs `applyE` teleElims deltaEx bs
  
      cxt <- getContextTelescope
      reportSDoc "tc.cover.hcomp" 30 $ text "cxt = " <+> prettyTCM cxt
      reportSDoc "tc.cover.hcomp" 30 $ text "tel = " <+> prettyTCM tel
      reportSDoc "tc.cover.hcomp" 20 $ addContext tel $ text "t = " <+> prettyTCM t
      reportSDoc "tc.cover.hcomp" 20 $ addContext tel $ text "rhs = " <+> prettyTCM rhs
  
      return $ Clause { clauseLHSRange  = noRange
                      , clauseFullRange = noRange
                      , clauseTel       = tel
                      , namedClausePats = fromSplitPatterns ps
                      , clauseBody      = Just $ rhs
                      , clauseType      = Just $ defaultArg t
                      , clauseCatchall    = empty
                      , clauseRecursive   = MaybeRecursive     -- TODO: can it be recursive?
                      , clauseUnreachable = Just False  -- missing, thus, not unreachable
                      , clauseEllipsis    = NoEllipsis
                      , clauseWhereModule = Nothing
                      }
    addClauses f [cl]  -- Important: add at the end.
    let result = CoverResult
            { coverSplitTree      = SplittingDone (size (clauseTel cl))
            , coverUsedClauses    = IntSet.singleton (length cs)
            , coverMissingClauses = []
            , coverPatterns       = [cl]
            , coverNoExactClauses = IntSet.empty
            }
    hcompName <- fromMaybe __IMPOSSIBLE__ <$> getName' builtinHComp
    return ([(SplitCon hcompName, result)], cs ++ [cl])
  createMissingHCompClause _ _ _ _ (SClause _ _ _ _ Nothing) _ = __IMPOSSIBLE__
  