Skip to content

Remove TCore type from Laurel HighType#1412

Open
keyboardDrummer-bot wants to merge 4 commits into
reviewed-kbd-will-merge-to-mainfrom
remove-tcore-from-laurel
Open

Remove TCore type from Laurel HighType#1412
keyboardDrummer-bot wants to merge 4 commits into
reviewed-kbd-will-merge-to-mainfrom
remove-tcore-from-laurel

Conversation

@keyboardDrummer-bot

Copy link
Copy Markdown
Collaborator

Summary

Remove the TCore variant from HighType in Laurel. Wherever TCore was created, UserDefined is now used instead.

Changes

  • LaurelAST.lean: Removed the TCore (s: String) variant from the HighType inductive type.
  • LaurelTypes.lean: Replaced .TCore "unknown" with .UserDefined "unknown" in computeExprType.
  • HeapParameterization.lean: Removed TCore match arms from boxDestructorName, boxConstructorName, and boxConstructorDef — the existing UserDefined branches handle these cases.
  • FilterPrelude.lean: Removed the TCore case from collectHighTypeNamesUserDefined already adds the type name.
  • CoreGroupingAndOrdering.lean: Removed TCore case from collectTypeRefsUserDefined already returns [name.text].
  • InferHoleTypes.lean: Removed TCore from the fallback pattern in hole type inference.
  • LaurelToCoreTranslator.lean: Removed TCore case; updated UserDefined fallback to return .tcons name.text [] (preserving the old TCore translation behavior) instead of .tcons "Composite" [].
  • Grammar/ConcreteToAbstractTreeTranslator.lean: coreType grammar rule now creates .UserDefined name.
  • Grammar/AbstractToConcreteTreeTranslator.lean: Removed TCore serialization case (covered by UserDefined).
  • Grammar/LaurelGrammar.st: Updated comment.

Testing

Full lake build succeeds with no errors.

Closes #1411

@keyboardDrummer

Copy link
Copy Markdown
Contributor

@keyboardDrummer-bot please remove CoreType from the grammar as well.

@keyboardDrummer
keyboardDrummer changed the base branch from main to reviewed-kbd-will-merge-to-main June 25, 2026 14:13
@keyboardDrummer

Copy link
Copy Markdown
Contributor

@keyboardDrummer-bot please rebase this on top of new target branch, reviewer-..

@keyboardDrummer-bot

Copy link
Copy Markdown
Collaborator Author

@keyboardDrummer I can't find a branch starting with reviewer-. The only similar branch is reviewed-kbd-will-merge-to-main, which is already the current base of this PR. Could you provide the full branch name you'd like me to rebase onto?

@keyboardDrummer

Copy link
Copy Markdown
Contributor

Yes please rebase the commits from this PR, which is just 6c73bbd, onto reviewed-kbd-will-merge-to-main

@keyboardDrummer

Copy link
Copy Markdown
Contributor

Yes please rebase the commits from this PR, which is just 6c73bbd, onto reviewed-kbd-will-merge-to-main

@keyboardDrummer-bot can you do this?

Remove the TCore variant from HighType. All former TCore usages now
produce UserDefined instead. The coreType grammar rule is preserved
for backward compatibility but now creates UserDefined.

In LaurelToCoreTranslator, the UserDefined fallback case now uses
name.text (matching old TCore behavior) instead of hardcoded
"Composite".

Closes #1411
@keyboardDrummer-bot
keyboardDrummer-bot force-pushed the remove-tcore-from-laurel branch from a51997b to 31bdc58 Compare June 25, 2026 16:01
@keyboardDrummer-bot

Copy link
Copy Markdown
Collaborator Author

Done. I rebased the single commit 6c73bbd onto reviewed-kbd-will-merge-to-main (now 31bdc582).

There were merge conflicts in three files due to the .TBv n cases that were added to the base branch after the original commit. I resolved them by keeping the .TBv n arms and removing the .TCore arms, which is consistent with the intent of this change.

When one branch of an if-then-else has type TVoid (e.g. pass statement
or empty block), it should not conflict with the other branch's type.
Previously this worked because TCore types (now removed) were gradual
and consistent with everything including TVoid. With TCore removed,
TVoid vs UserDefined types triggered a false incompatible-types error.

Fix by short-circuiting the consistency check: if either branch is
TVoid, the if-then-else result is TVoid (used for effect only).
@keyboardDrummer
keyboardDrummer marked this pull request as ready for review June 26, 2026 07:41
@keyboardDrummer
keyboardDrummer requested a review from a team as a code owner June 26, 2026 07:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Remove the Core type from Laurel

2 participants