Fix misleading error message in pattern constructor type-checking (#6126)

[mmustafasenoglu]

Summary

When a pattern constructor receives an argument of the wrong type, the error message previously said "The Nth argument to f" where f was the enclosing function (e.g., b). It now correctly says "The Nth argument to Constructor" referring to the data constructor being matched.

Fixes #6126

Problem

Given:

type X = X
type Y k = Y X

a = b cases Y (3,4) -> "c"
b : (a -> b) -> c
b = todo "whatever"

The error said: "The 1st argument to b has type Tuple but expected X"

But b is irrelevant — it should say "The 1st argument to Y has type Tuple but expected X"

Solution

4 files changed:

1. Context.hs: Added InPatternApply ConstructorReference to the PathElement ADT, and wrapped the pattern constructor subtype check (checkPattern for Pattern.Constructor) with scope (InPatternApply ref).

2. Extractor.hs: Added inPatternApply subsequence extractor to match the new path element.

3. TypeError.hs: Added patternCtor :: Maybe ConstructorReference field to FunctionApplication, and created a new applyingPatternConstructor extractor that chains through the InPatternApply element in the error path.

4. PrintError.hs: Updated the FunctionApplication error rendering to use showConstructor when patternCtor is Just, displaying the constructor name instead of the enclosing function name.

Key insight

The SubseqExtractor monad requires strict adjacency (startB == endA + 1) between consecutive path elements. Adding InPatternApply between InSubtype and InCheck breaks the existing applyingFunction extractor chain, so a separate extractor was needed. The allErrors list tries applyingPatternConstructor before applyingFunction; the former matches when InPatternApply is present, the latter matches for regular function application errors.

Testing

• Added transcript test: fix-6126-pattern-constructor-error.md
• No Haskell toolchain available in this environment — build and test locally before merge

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

[mmustafasenoglu]

Rebased onto current trunk and resolved the conflict in Context.hs — the GADT principality rework touched the same code, so the InPatternApply scope now wraps all three subtype calls in the constructor case. CI needs approval to run on this fork PR, appreciate it when someone has a moment.