Codecov Report

Merging #851 (7f3d97b) into main (6c6215d) will decrease coverage by 0.86%.
The diff coverage is 47.23%.

@@             Coverage Diff              @@
##               main     #851      +/-   ##
============================================
- Coverage     82.69%   81.83%   -0.87%     
- Complexity     3295     3319      +24     
============================================
  Files           279      287       +8     
  Lines         10332    10545     +213     
  Branches       1226     1263      +37     
============================================
+ Hits           8544     8629      +85     
- Misses         1118     1241     +123     
- Partials        670      675       +5     

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

I still think the error message is not very helpful. Is there a way to show the exact expression that is problematic?

Ideally, I would appreciate an error message that can help you understand what's wrong in the type checker without debugging the source code of the compiler.

I still think the error message is not very helpful. Is there a way to show the exact expression that is problematic?

Ideally, I would appreciate an error message that can help you understand what's wrong in the type checker without debugging the source code of the compiler.

I think sourcepos of the ctor definition is enough for user to understand what's wrong in most cases

I still think the error message is not very helpful. Is there a way to show the exact expression that is problematic?

Ideally, I would appreciate an error message that can help you understand what's wrong in the type checker without debugging the source code of the compiler.

I think sourcepos of the ctor definition is enough for user to understand what's wrong in most cases

What if there are 3 mutually recursive data types with each of them 2-10 constructors?

Aya is going to self host and the definition of Term will be inductive-inductively defined together with contexts and type formers. Every introduction and elimination rule is a constructor. This is a real-world example.

What if there are 3 mutually recursive data types with each of them 2-10 constructors?

I think it still should be a very rare case to trigger an error and see a hardly understandable error message.

might implement more detailed error message in future prs

What if there are 3 mutually recursive data types with each of them 2-10 constructors?

I think it still should be a very rare case to trigger an error and see a hardly understandable error message.

might implement more detailed error message in future prs

It's exactly when the code gets complicated do people need to look at error messages. So, I would prefer higher quality ones.

I think positivity with the presence of HITs will be more complex. See agda/agda#6336