Andreas Abel

Welcome back, Ulf! > > My opinion is that `f {_} a` should behave exactly like `f a` > > I'm pretty sure we've had this discussion before (for `f...

What about tactics in record fields then, @UlfNorell ? We currently support them even when the fields are not hidden. - #5712 https://github.com/agda/agda/blob/3b98c183052565193573af8bfa1e83c18a9b5faa/test/Succeed/Issue5712.agda#L8-L19

> What does "support" mean in this case? Do you have an example where the tactic runs? Yes, this one, derived from #5358: ```agda open import Agda.Builtin.Unit open import Agda.Builtin.Bool...

@UlfNorell In the syntactic approach you favor (rather than a more semantic one like _metavariable with attached tactic_), it seems you cannot curry functions with tactic arguments. E.g. this fails:...

> In that case it makes sense to not given an error, no? We're only suggesting the error because explicit tactic arguments are pointless. Not sure, it would be more...

I started working on the new `UselessTactic` warning on https://github.com/agda/agda/tree/issue-6781, but will finish it only after #6784 which fixes the ranges of tactic attributes so that we can have correct...

The latter error has several clones: https://github.com/agda/agda/blob/a7edb851ddbd2eff62fab399542a22fdb68b909e/src/full/Agda/TypeChecking/Coverage/Cubical.hs#L1008-L1015 https://github.com/agda/agda/blob/a7edb851ddbd2eff62fab399542a22fdb68b909e/src/full/Agda/TypeChecking/Primitive/Cubical.hs#L1046-L1052

Any luck yet, @plt-amy ?

Possibly missing `applyWhen optExperimentalIrrelevance irrToNonStrict` on the codomain here? https://github.com/agda/agda/blob/1c449e23b1db2462e8bd6959f423898a8fdc361f/src/full/Agda/TypeChecking/Irrelevance.hs#L238-L241

> Possibly missing `applyWhen optExperimentalIrrelevance irrToNonStrict` on the codomain here? This lets the data definition through, but trying to use it the `conSplitModalityCheck` barks at us. @plt-amy says this is...