Type a let destructuring a GADT without switch diagnostics (#9081)

* Type a let destructuring a GADT without switch diagnostics

Why:
    A `let` whose pattern contains a GADT constructor is typed as a
    one-case match, and that match took the diagnostic context of a
    `switch` in the source: a type error in the rest of the block said
    "But this switch is expected to return" and added the hint about
    switch branches, although the source has no switch. The match now
    carries `#let_gadt_pattern`, and its cases, like those of the match
    for an optional argument default, get function-style diagnostics.

Typedtree modified (let destructuring a GADT constructor):
Example:
    type rec any = Any('a, 'a => string): any
    let get = value => {
      let Any(x, f) = value
      f(x)
    }
Before (typed):
    expression
      Texp_match
      expression
        Texp_ident "value/1004"
      [
        <case>
          pattern
            Tpat_construct "Any"
            …
          expression
            Texp_apply
            …
      ]
After (typed):
    expression
      attribute "#let_gadt_pattern"
        []
      Texp_match
      expression
        Texp_ident "value/1004"
      [
        <case>
          pattern
            Tpat_construct "Any"
            …
          expression
            Texp_apply
            …
      ]

Decision modified (diagnostic context of a match's cases):
Before (text): `call_context` in `Typecore.type_expect_`
    match with @let.unwrap                    ↦ LetUnwrap
    match with #optional_arg_default          ↦ Function
    match typed for a let with a GADT pattern ↦ Switch
    any other match                           ↦ Switch
After (text):
    match with @let.unwrap                    ↦ LetUnwrap
    match with #optional_arg_default          ↦ Function
    match with #let_gadt_pattern              ↦ Function
    any other match                           ↦ Switch

Diagnostic modified (type error in the body of a let destructuring a GADT):
Example:
    type rec any = Any('a, 'a => string): any

    let get = value => {
      let Any(x, _) = value
      x
    }
Before (diagnostic):
    This has type: $a
    But this switch is expected to return: 'a
    $a is an existential type bound by the constructor Any.
    It is only known in the scope of the pattern that matches Any.

    All branches in a switch must return the same type.
    To fix this, change your branch to return the expected type.
After (diagnostic):
    This has type: $a
    But it's expected to have type: 'a
    $a is an existential type bound by the constructor Any.
    It is only known in the scope of the pattern that matches Any.

Fixes: #9069
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3
Claude-Session: https://claude.ai/code/session_01Kr4cjoUi2f5VpMvE6wT9bo
Signed-off-by: Christoph Knittel <ck@cca.io>
Signed-off-by: Cristiano Calcagno <cristianoc@users.noreply.github.com>

* Records show the changed operation before its consequences

The records skill asked for a block for each object a commit changes in
what the compiler does, and a record of #9081 met it with the diagnostic
alone, leaving the attribute the type checker adds to the synthesized
match in prose. A record now shows the representation, rule,
transformation or decision that changes, at its own level, and then its
consequences; a change the prose names is shown in a block, a change no
form prints is shown as a schematic, and a script or review fix that
changes behaviour gets blocks.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Cristiano Calcagno <cristianoc@users.noreply.github.com>

---------

Signed-off-by: Christoph Knittel <ck@cca.io>
Signed-off-by: Cristiano Calcagno <cristianoc@users.noreply.github.com>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Co-authored-by: Cristiano Calcagno <cristianoc@users.noreply.github.com>

Author: 3 people

.agents/skills/records/SKILL.md

@@ -177,10 +177,32 @@ The table lists the common kinds.
 ## What a commit holds
 
 Every commit says why it is made. A commit that changes what the compiler
-or a tool does gets one object block for each object it changes, with the
-smallest example that shows the change. A refactor, a test, a script or a
-review fix needs no block, only its subject and a line or two of prose; a
-review fix names the finding it answers.
+or a tool does shows each representation, rule, transformation or decision
+it changes, Before and After, at the level where it operates, then the
+representative consequences that show why it matters: the blocks go from
+the changed operation to what it affects, and one block serves both when
+the operation directly changes the output shown. Each change the prose
+names, such as an attribute the compiler adds or a case a decision takes,
+is also shown in a block. Each block has the smallest example that shows
+its change.
+
+- A printed form shows the change when one exposes it. Otherwise a block
+  shows a schematic, captioned with the function that implements it: an
+  inference rule for a changed typing judgment, a clause matrix and its
+  split for the match compiler, a mapping from inputs to results for a
+  decision, keeping the premises, priorities and side conditions that
+  matter.
+- Printing each form for the example before and after the commit finds
+  the layers it changes; the record keeps the excerpts that show the
+  changed operation and its distinct consequences.
+- When an error stops later forms from being printed, the internal forms
+  come from a related example that compiles, the diagnostic from one that
+  fails, and the prose says how they relate.
+
+A commit whose changes are only organization, tests or documentation
+needs no block, only its subject and a line or two of prose; a script or
+a review fix that changes behaviour gets blocks like any other. A review
+fix names the finding it answers.
 
 ## Rendering
 

changes/existential-let-context.polish.md

@@ -0,0 +1 @@
+- A type error in the body after a `let` that destructures a GADT constructor no longer talks about switch branches.

compiler/ml/typecore.ml

@@ -2644,6 +2644,8 @@ and type_expect_ ?deprecated_context ~context ?(recarg = Rejected) env sexp
       {
         sexp with
         pexp_desc = Pexp_match (sval, [Ast_helper.Exp.case spat sbody]);
+        pexp_attributes =
+          (mknoloc "#let_gadt_pattern", PStr []) :: sexp.pexp_attributes;
       }
       ty_expected
   | Pexp_let (rec_flag, spat_sexp_list, sbody) ->
@@ -2832,10 +2834,13 @@ and type_expect_ ?deprecated_context ~context ?(recarg = Rejected) env sexp
     in
     let call_context =
       (* Optional-default lowering synthesizes a match expression, but from the
-         user's point of view this is still part of a function definition. Use
-         function-style diagnostics instead of reporting a phantom switch. *)
+         user's point of view this is still part of a function definition. A
+         [let] destructuring a GADT constructor is typed as a one-case match,
+         whose body is the rest of the block. Use function-style diagnostics
+         for both instead of reporting a phantom switch. *)
       if has_attr "let.unwrap" then `LetUnwrap
-      else if has_attr "#optional_arg_default" then `Function
+      else if has_attr "#optional_arg_default" || has_attr "#let_gadt_pattern"
+      then `Function
       else `Switch
     in
     let val_cases, partial =

tests/build_tests/super_errors/expected/gadt_existential_let.res.expected

@@ -0,0 +1,14 @@
+
+  We've found a bug for you!
+  /.../fixtures/gadt_existential_let.res:5:3
+
+  3 │ let get = value => {
+  4 │   let Any(x, _) = value
+  5 │   x
+  6 │ }
+  7 │ 
+
+  This has type: $a
+  But it's expected to have type: 'a
+  $a is an existential type bound by the constructor Any.
+  It is only known in the scope of the pattern that matches Any.

tests/build_tests/super_errors/fixtures/gadt_existential_let.res

@@ -0,0 +1,6 @@
+type rec any = Any('a, 'a => string): any
+
+let get = value => {
+  let Any(x, _) = value
+  x
+}