Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unify type signature declaration syntax #3178

Open
wants to merge 8 commits into
base: main
Choose a base branch
from

Conversation

lukaszcz
Copy link
Collaborator

@lukaszcz lukaszcz commented Nov 18, 2024

field {A} {{M A}} (arg1 arg2 : A) : List A
  • For constructors, this introduces an ambiguity between record and GADT syntax with names. For example,
ctr {
  A : Type
}

can be confused by the parser with initial part of GADT type signature:

ctr {A : Type} : A -> C A

For now, this is resolved by preferring the record syntax. Hence, it's currently not possible to use type signatures with implicit arguments for constructors. Ultimately, the @ in record syntax should be made mandatory, which would resolve the ambiguity:

ctr@{
  A : Type
}

@lukaszcz lukaszcz added enhancement New feature or request syntax labels Nov 18, 2024
@lukaszcz lukaszcz added this to the 0.6.9 milestone Nov 18, 2024
@lukaszcz lukaszcz self-assigned this Nov 18, 2024
@lukaszcz lukaszcz marked this pull request as ready for review November 19, 2024 12:08
@lukaszcz lukaszcz requested review from janmasrovira and paulcadman and removed request for janmasrovira November 19, 2024 12:09
@paulcadman paulcadman force-pushed the uniform-type-declaration-syntax branch from e8cddc4 to 8990702 Compare November 19, 2024 17:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request syntax
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Unify syntax for named arguments in traits, instances, and functions
1 participant