Skip to content

Conversation

tiif
Copy link
Member

@tiif tiif commented Mar 18, 2025

Opened a draft so it is easier to fetch and push to this branch.

@tiif tiif marked this pull request as draft March 18, 2025 15:09
@nikomatsakis nikomatsakis marked this pull request as ready for review August 20, 2025 22:27
use formality_prove::Env;
use formality_rust::{
grammar::{Fn, FnBoundData},
grammar::{Fn, FnBody, FnBoundData, MaybeFnBody},
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ignore this, I'm making a test :)

@tiif
Copy link
Member Author

tiif commented Sep 16, 2025

Revisited this, I think there are still more stuff needed to properly model this. It might be ok to just rebase and land this, but the syntax we use here is definitely not the friendliest to the reader >:)

This has happened a while ago, so to recap, we defined the subset relationship between const, runtime and associated effect.

How the test currently looks like for

 const fn foo<T>()
 where 
   T: Default,
 {
     <T as Default>::default();
 }

is

fn foo() -> () random_keyword do const {
     (AssociatedEffect(Default()))
}

Improvements

  1. Now that we already have some basic support for minirust bodies (yay!), technically we can just support fully qualified path in function body, similar to what we did for ValueExpression::Fn, but the type checking for fully qualifed path might be more involved.

  2. It'd be nice to match the syntax that is planned to be used, and write something similar to

const fn default<T: [const] Default>() -> T {
    T::default()
}

but we might need to do a small refactoring to make this happen.
3. Fix the parser bug that requires us to add random_keyword to make the grammar work :)

@tiif tiif mentioned this pull request Oct 8, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants