address review feedback

src/full/Agda/TypeChecking/DiscrimTree.hs

@@ -107,13 +107,6 @@ tickExplore tm = whenProfile Profile.Instances do
     DontCare{} -> tick "explore: DontCare"
     _ -> pure ()
 
--- | Checks whether the given abstraction could have been 'NoAbs'.
-isNoAbs :: Abs Term -> Maybe Term
-isNoAbs (NoAbs _ b) = Just b
-isNoAbs (Abs _ b)
-  | not (0 `freeIn` b) = Just (strengthen __IMPOSSIBLE__ b)
-  | otherwise          = Nothing
-
 -- | Split a term into a 'Key' and some arguments. The 'Key' indicates
 -- whether or not the 'Term' is in head-normal form, and provides a
 -- quick way to match on the head.

src/full/Agda/TypeChecking/DiscrimTree/Types.hs

@@ -104,8 +104,11 @@ instance Null (DiscrimTree a) where
     EmptyDT -> True
     _       -> False
 
--- | Merge a pair of discrimination trees. This function performs a few
--- optimisations.
+-- | Merge a pair of discrimination trees. This function tries to build
+-- the minimal discrimination tree that yields the union of the inputs'
+-- results, though it does so slightly naïvely, without considerable
+-- optimisations (e.g. it does not turn single-alternative 'CaseDT's
+-- into 'DoneDT's).
 mergeDT :: Ord a => DiscrimTree a -> DiscrimTree a -> DiscrimTree a
 mergeDT EmptyDT    x = x
 mergeDT (DoneDT s) x = case x of
@@ -115,11 +118,10 @@ mergeDT (DoneDT s) x = case x of
 mergeDT (CaseDT i bs els) x = case x of
   EmptyDT  -> CaseDT i bs els
   DoneDT s -> CaseDT i bs (mergeDT (DoneDT s) els)
-  CaseDT j bs' els'
-    | i == j -> CaseDT j (Map.unionWith mergeDT bs bs') (mergeDT els els')
-    | i < j -> CaseDT i bs (mergeDT els (CaseDT j bs' els'))
-    | j < i -> CaseDT j bs' (mergeDT els' (CaseDT i bs els))
-    | otherwise -> __IMPOSSIBLE__
+  CaseDT j bs' els' -> case compare i j of
+    EQ -> CaseDT j (Map.unionWith mergeDT bs bs') (mergeDT els els')
+    LT -> CaseDT i bs (mergeDT els (CaseDT j bs' els'))
+    GT -> CaseDT j bs' (mergeDT els' (CaseDT i bs els))
 
 instance Ord a => Semigroup (DiscrimTree a) where
   (<>) = mergeDT

src/full/Agda/TypeChecking/InstanceArguments.hs

@@ -456,7 +456,7 @@ findInstance' m cands = do
           reportSDoc "tc.instance" 15 $
             text ("findInstance 5: refined candidates: ") <+>
             prettyTCM (List.map candidateTerm cs)
-          whenProfile Profile.Instances $ tick "findInstance: too many candidates"
+          whenProfile Profile.Instances $ tick "findInstance: multiple candidates"
           return (Just (cs, neverUnblock))
 
 insidePi :: Type -> (Type -> TCM a) -> TCM a

src/full/Agda/TypeChecking/Substitute.hs

@@ -857,6 +857,7 @@ instance Subst Term where
 
 -- András 2023-09-25: we can only put this here, because at the original definition site there's no Subst Term instance.
 {-# SPECIALIZE lookupS :: Substitution' Term -> Nat -> Term #-}
+{-# SPECIALIZE isNoAbs :: Abs Term -> Maybe Term #-}
 
 instance Subst BraveTerm where
   type SubstArg BraveTerm = BraveTerm

src/full/Agda/TypeChecking/Substitute/Class.hs

@@ -93,6 +93,16 @@ strengthen err = applySubst (strengthenS err 1)
 substUnder :: Subst a => Nat -> SubstArg a -> a -> a
 substUnder n u = applySubst (liftS n (singletonS 0 u))
 
+-- | Checks whether the variable bound by the abstraction is actually
+-- used, and, if /not/, returns the term within, 'strengthen'ed to live in
+-- the context /outside/ the abstraction.
+-- See also 'Agda.TypeChecking.Free.isBinderUsed'.
+isNoAbs :: (Free a, Subst a) => Abs a -> Maybe a
+isNoAbs (NoAbs _ b) = Just b
+isNoAbs (Abs _ b)
+  | not (0 `freeIn` b) = Just (strengthen __IMPOSSIBLE__ b)
+  | otherwise          = Nothing
+
 -- ** Identity instances
 
 instance Subst QName where