@@ -482,10 +482,27 @@ data UnivSize
   | ULarge  -- ^ @(Prop/Set/SSet)ωᵢ@.
   deriving stock (Eq, Show)
 
--- | Blocked dependency (i.e. free zero variable) check, used in 'PiSort'
+-- | Blocked dependency (i.e. free zero variable) check, used in 'PiSort'.
+--
 --   For efficiency, we track whether the codomain sort has actually changed.
 --   If it hasn't, we can avoid duplicating work.
-data BlockedDepCheck t = CodomainSortOld t | CodomainSortSame
+data BlockedDepCheck t
+  = CodomainSortSame
+  -- ^ The codomain sort has not changed, so we can just do the dependency
+  --   check on the current codomain sort.
+  | CodomainSortOld t
+  -- ^ The codomain sort has changed, so we really need to do the dependency
+  --   check on the original codomain sort.
+  --
+  --   E.g. see #5810: @∀ t → Set (ℓ t)@ has codomain sort @Set (lsuc (ℓ t))@
+  --   but then after the substitution @ℓ ↦ λ _ → lzero@, the codomain sort
+  --   becomes @Set (lsuc lzero)@, which is no longer dependent on @t@.
+  --   To avoid a subject reduction problem, we have to remember that the
+  --   codomain sort before the substitution was @Set (lsuc (ℓ t))@.
+  --
+  --   The old codomain sort lives in its original context. In an ideal world,
+  --   we would store this context, but this does not appear very feasible
+  --   (without a significant refactor).
   deriving (Show, Functor, Foldable, Traversable, Generic)
 
 codomainSortOld :: t -> BlockedDepCheck t -> t
@@ -1639,7 +1656,7 @@ instance TermSize Sort where
     LockUniv  -> 1
     LevelUniv -> 1
     IntervalUniv -> 1
-    PiSort _ a s1 s2 -> 1 + tsize a + tsize s1 + tsize s2
+    PiSort _c a s1 s2 -> 1 + tsize a + tsize s1 + tsize s2
     FunSort s1 s2 -> 1 + tsize s1 + tsize s2
     UnivSort s -> 1 + tsize s
     MetaS _ es -> 1 + tsize es
@@ -1853,7 +1870,7 @@ instance Pretty t => Pretty (Abs t) where
 
 instance Pretty t => Pretty (BlockedDepCheck t) where
   pretty (CodomainSortOld s) = "CodomainSortOld" <+> pretty s
-  pretty CodomainSortSame = "CodomainSortSame"
+  pretty CodomainSortSame    = "CodomainSortSame"
 
 instance (Pretty t, Pretty e) => Pretty (Dom' t e) where
   pretty dom = pLock <+> pTac <+> pDom dom (pretty (getModality dom) <+> pretty (unDom dom))
 
@@ -830,7 +830,7 @@ instance ExtractCalls Sort where
       Univ _ t       -> terUnguarded $ extract t  -- no guarded levels
       -- We ignore calls in the blocked dependency check (these will vanish
       -- after the 'PiSort' reduces)
-      PiSort _ a s1 s2 -> extract (a, s1, s2)
+      PiSort _c a s1 s2 -> extract (a, s1, s2)
       FunSort s1 s2 -> extract (s1, s2)
       UnivSort s -> extract s
       MetaS x es -> return empty
 
@@ -2065,8 +2065,8 @@ equalSort s1 s2 = do
                 CodomainSortSame -> funSortEquals propEnabled s s1 s2M blocker
                 CodomainSortOld s2Old -> liftReduce
                   (inLargeEnoughContext s2Old $ forceNonDepSort s2Old) >>= \case
-                   (NotFree, _) -> funSortEquals propEnabled s s1 s2M blocker
-                   (MaybeFree _, _) -> postpone
+                    (NotFree, _) -> funSortEquals propEnabled s s1 s2M blocker
+                    (MaybeFree _, _) -> postpone
            -- Otherwise: postpone
            | otherwise -> postpone
 
 
@@ -211,7 +211,7 @@ instance Free Sort where
         LockUniv       -> ret $ mempty
         LevelUniv      -> ret $ mempty
         IntervalUniv   -> ret $ mempty
-        PiSort c a s1 s2 -> ret $
+        PiSort _c a s1 s2 -> ret $
           -- We ignore variables in the blocked dependency check
           underFlexRig (Flexible mempty) (freeVars $ unDom a) <>
           underFlexRig WeaklyRigid (freeVars (s1, s2))
 
@@ -240,12 +240,12 @@ instance ForceNotFree Sort where
   -- away without forceNotFreeR here.
   forceNotFree' s = expand \ret -> case s of
     Univ u l       -> ret $ Univ u <$> forceNotFree' l
-    PiSort a b c d   -> ret do
+    PiSort c a s1 s2 -> ret do
       -- We ignore variables in the blocked dependency check
-      b        <- underFlexRig (Flexible mempty) (forceNotFree' b)
-      (!c, !d) <- underFlexRig WeaklyRigid
-        ((,) <$> forceNotFree' c <*> forceNotFree' d)
-      pure $ PiSort a b c d
+      a        <- underFlexRig (Flexible mempty) (forceNotFree' a)
+      (!s1, !s2) <- underFlexRig WeaklyRigid
+        ((,) <$> forceNotFree' s1 <*> forceNotFree' s2)
+      pure $ PiSort c a s1 s2
     FunSort a b    -> ret $ FunSort <$> forceNotFree' a <*> forceNotFree' b
     UnivSort s     -> ret $ UnivSort <$> underFlexRig WeaklyRigid (forceNotFree' s)
     MetaS x es     -> ret $ MetaS x <$> underFlexRig (Flexible (singleton x)) (forceNotFree' es)
 
@@ -155,7 +155,7 @@ instance UsableRelevance Sort where
     LockUniv -> return True
     LevelUniv -> return True
     IntervalUniv -> return True
-    PiSort c a s1 s2 -> usableRel rel (a,s1,s2)
+    PiSort _c a s1 s2 -> usableRel rel (a,s1,s2)
     FunSort s1 s2 -> usableRel rel (s1,s2)
     UnivSort s -> usableRel rel s
     MetaS x es -> usableRel rel es
 
@@ -770,7 +770,7 @@ instance Occurs Sort where
   metaOccurs !m !s = do
     s <- instantiate s
     case s of
-      PiSort _ a s1 s2 -> do
+      PiSort _c a s1 s2 -> do
         -- We ignore occurrences in the blocked dependency check (these will
         -- vanish after 'PiSort' reduces)
         metaOccurs m a
 
@@ -801,11 +801,21 @@ getVarInfo x =
                       -- TODO: It would be worthwhile investigating who wants to access
                       -- an out-of-scope variable.
 
--- | Create a dummy context large enough for the given thing to be well-scoped
+-- | Change to a dummy context large enough for the given thing to be
+--   well-scoped
 --   (Very hacky, should only be used if there is no alternative)
 inLargeEnoughContext :: (ReadTCState m, MonadAddContext m, Free a)
   => a -> m b -> m b
 inLargeEnoughContext t c = do
   let len = 1 + foldl' max 0 (freeVarList t)
   let dummies = replicate len __DUMMY_DOM__
   inTopContext $ addContext dummies c
+
+-- | Run the continuation on the old codomain sort, in an appropriate context
+codomainSortOldM :: (ReadTCState m, MonadAddContext m) =>
+  Dom Type -> Sort -> BlockedDepCheck Sort -> (Sort -> m a) -> m a
+codomainSortOldM dom s2 CodomainSortSame c = do
+  addContext dom $ c s2
+codomainSortOldM dom s2 (CodomainSortOld s2Old) c = do
+  inLargeEnoughContext s2Old $ c s2Old
+
@@ -469,19 +469,18 @@ instance Reduce Sort where
           Blocked b (c, s1 , s2Abs) -> return $!
             blockedOn b $ PiSort c a s1 s2Abs
           NotBlocked _ (c, s1 , s2Abs) -> do
-            let s2Old = codomainSortOld (unAbs s2Abs) c
+            let dom = El s1 <$> a
             -- In theory we should just call piSort' here. However, we also want
             -- to reduce the codomain sort to make it non-dependent when
             -- possible. So we use forceNonDep and in case we are dealing with a
             -- proper Abs we call piSortAbs directly.
-            let dom = El s1 <$> a
-            inLargeEnoughContext s2Old (forceNonDepSort s2Old) >>= \case
+            codomainSortOldM dom (unAbs s2Abs) c forceNonDepSort >>= \case
               -- If the codomain sort is non-dependent, we reduce to a FunSort
               (NotFree, s2Old) -> do
                 -- We need to obtain a strengthened version of the codomain sort
                 s2 <- case c of
                   CodomainSortSame -> pure s2Old
-                  CodomainSortOld _ ->
+                  CodomainSortOld{} ->
                     addContext dom (forceNonDepSort $! unAbs s2Abs) >>= \case
                       (NotFree, s2) -> pure s2
                       -- If 's2Old' is non dependent, then 's2' must also be
@@ -1668,18 +1667,18 @@ instance InstantiateFull Sort where
   instantiateFull' s = do
     s <- instantiate' s
     case s of
-      Univ u n   -> Univ u <$!> instantiateFull' n
+      Univ u n         -> Univ u <$!> instantiateFull' n
       PiSort c a s1 s2 -> uncurry4 piSortM' =<< instantiateFull' (c, a, s1, s2)
-      FunSort s1 s2 -> uncurry funSortM =<< instantiateFull' (s1, s2)
-      UnivSort s -> univSort <$!> instantiateFull' s
-      Inf _ _    -> return s
-      SizeUniv   -> return s
-      LockUniv   -> return s
-      LevelUniv  -> return s
-      IntervalUniv -> return s
-      MetaS x es -> MetaS x <$!> instantiateFull' es
-      DefS d es  -> DefS d <$!> instantiateFull' es
-      DummyS{}   -> return s
+      FunSort s1 s2    -> uncurry funSortM =<< instantiateFull' (s1, s2)
+      UnivSort s       -> univSort <$!> instantiateFull' s
+      Inf _ _          -> return s
+      SizeUniv         -> return s
+      LockUniv         -> return s
+      LevelUniv        -> return s
+      IntervalUniv     -> return s
+      MetaS x es       -> MetaS x <$!> instantiateFull' es
+      DefS d es        -> DefS d <$!> instantiateFull' es
+      DummyS{}         -> return s
 
 instance (Free a, InstantiateFull a)
       => InstantiateFull (BlockedDepCheck a) where
 
@@ -988,7 +988,7 @@ instance Subst a => Subst (Sort' a) where
             -- is stable under injective substitutions
             then CodomainSortSame
             else CodomainSortOld $! unAbs s2
-          CodomainSortOld _ -> c
+          CodomainSortOld{} -> c
     FunSort s1 s2  -> FunSort (applySubst rho s1) (applySubst rho s2)
     UnivSort s     -> UnivSort $ applySubst rho s
     MetaS x es     -> MetaS x $! subE rho es