Error message regression for nested inductive types

Description

The error message for certain invalid nested inductive types got much worse in recent nightlies.

Context

This arose while updating the language reference.

Steps to Reproduce

1. Open a file in a Lean nightly from on or after 2025-06-21
2. 2. Enter the following code:

   import Std.Data.HashMap
   
   open Std
   
   structure Maze where
     description : String
     passages : HashMap String Maze
   

3. Observe the error message

Expected behavior:
An error message that says something about nested occurrences, like the one emitted on 2025-06-20 and earlier:

(kernel) arg #1 of '_nested.Std.HashMap_1.mk' contains a non valid occurrence of the datatypes being declared

This message is not phrased in terms of what the user actually wrote, but rather internal elaboration artifacts, and it doesn't mention "nested inductive types", but it is at least a reasonable search term and can be improved from here.

Actual behavior:

A more confusing and less specific error message:

(kernel) application type mismatch
  DHashMap.Raw.WF inner
argument has type
  _nested.Std.DHashMap.Raw_3
but function has type
  (DHashMap.Raw String fun x => Maze) → Prop

This message makes it much harder diagnose the issue.

Versions

Nightlies from 2025-06-21 and later

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the issue with the supplied Maze and HashMap example in a Lean nightly from 2025-06-21 or later, then compare its diagnostic with the output from 2025-06-20 or earlier. Done means the nested inductive type error is specific and useful rather than exposing confusing internal elaboration artifacts.