Add Note [No alternatives lint check]

in a follow up to #10180.

compiler/coreSyn/CoreLint.hs

@@ -657,6 +657,7 @@ lintCoreExpr e@(Case scrut var alt_ty alts) =
      ; alt_ty   <- lintInTy alt_ty
      ; var_ty   <- lintInTy (idType var)
 
+     -- See Note [No alternatives lint check]
      ; when (null alts) $
      do { checkL (not (exprIsHNF scrut))
           (ptext (sLit "No alternatives for a case scrutinee in head-normal form:") <+> ppr scrut)
@@ -715,6 +716,18 @@ kind coercions and produce the following substitution which is to be
 applied in the type variables:
   k_ag   ~~>   * -> *
 
+Note [No alternatives lint check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Case expressions with no alternatives are odd beasts, and worth looking at
+in the linter.
+
+Certainly, it would be terribly wrong if the scrutinee was already in head
+normal form. That is the first check.
+
+Furthermore, we should be able to see why GHC believes the scrutinee is
+diverging for sure. That is the second check. see #10180.
+
 ************************************************************************
 *                                                                      *
 \subsection[lintCoreArgs]{lintCoreArgs}

compiler/coreSyn/CoreUtils.hs

@@ -2108,7 +2108,10 @@ rhsIsStatic platform is_dynamic_name cvt_integer rhs = is_static False rhs
 ************************************************************************
 -}
 
--- | True if the type has no non-bottom elements
+-- | True if the type has no non-bottom elements, e.g. when it is an empty
+-- datatype, or a GADT with non-satisfiable type parameters, e.g. Int :~: Bool.
+--
+-- See Note [No alternatives lint check] for one use of this function.
 isEmptyTy :: Type -> Bool
 isEmptyTy ty
     -- Data types with no constructors are empty