search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

`--postfix-projections` do not make use of mixfix syntax #7318

Closed andreasabel closed 1 week ago

andreasabel commented 1 week ago

Consider the testcase for #2288:

record Setoid : Set₁ where
  field
    ∣_∣    : Set
    {{eq}} : Eq ∣_∣
open Setoid

NatSetoid : Setoid
∣ NatSetoid ∣ = Nat

The error with --no-postfix-projections is: 

No instance of type Eq ∣ NatSetoid ∣ ...

With --postfix-projections we get:

No instance of type Eq (NatSetoid .∣_∣)

This isn't pretty. Postfix notation should not kick in when we can actually use the mixfix-syntax.

A little doubt: the field ∣_∣ : Set is actually a hack, exploiting the questionable "feature" of Agda to blindly apply mixfix syntax even when outside the module it was defined in.

So maybe the current broken postfix printing is less wrong than the prefix printing.

Opinions?

andreasabel commented 1 week ago

Related: