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.

Sign up for GitHub

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

Jump to bottom

Printer prefers (longer) qualified over (shorter) unqualified name #3240

Open
andreasabel opened this issue Sep 25, 2018 · 1 comment
Open

Printer prefers (longer) qualified over (shorter) unqualified name #3240

andreasabel opened this issue Sep 25, 2018 · 1 comment
Labels
import Issues to do with importing modules modules Issues relating to the module system scope Issues relating to scope checking type: enhancement Issues and pull requests about possible improvements ux: printing Issues relating to how terms are printed for display
Milestone
icebox

Comments

@andreasabel
Copy link
Member

andreasabel commented Sep 25, 2018 •
edited
Loading

The printer prefers (longer) qualified over (shorter) unqualified name, even if the former is unambiguous.

open import Agda.Builtin.Equality using (_≡_) 
module Eq = Agda.Builtin.Equality

test : ∀{A : Set} (a : A) → a ≡ a
test a = {!!}

-- Goal displayed as
-- ?0 : a Eq.≡ a

-- EXPECTED:
-- ?0 : a ≡ a

This effectively discourages me from qualified imports in the style of

module Eq = Agda.Builtin.Equality
@andreasabel andreasabel added modules Issues relating to the module system scope Issues relating to scope checking ux: printing Issues relating to how terms are printed for display import Issues to do with importing modules labels Sep 25, 2018
@andreasabel andreasabel added this to the 2.6.0 milestone Sep 25, 2018
@UlfNorell
Copy link
Member

In this particular case the more natural qualified import would be

open import Agda.Builtin.Equality as Eq using (_≡_)

in which case you get the expected behaviour.

Printing of names from module applications is done by generating a display form for the right-hand side (Agda.Builtin.Equality) to the left-hand side (Eq). At the moment I don't believe there is any heuristics for deciding whether not using the display form would be a better idea.

When there are actual arguments in the module application it's not at all clear what the best choice is:

open import Agda.Builtin.Nat

module M (A : Set) where
  postulate T : Set

open M
module MNat = M Nat

foo : MNat.T
foo = {!!} -- display as MNat.T or T Nat ?

@jespercockx jespercockx added the type: enhancement Issues and pull requests about possible improvements label Nov 15, 2018
@jespercockx jespercockx modified the milestones: 2.6.0, 2.6.1 Nov 15, 2018
@jespercockx jespercockx modified the milestones: 2.6.1, icebox Oct 9, 2019
@jespercockx jespercockx mentioned this issue Jul 7, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
import Issues to do with importing modules modules Issues relating to the module system scope Issues relating to scope checking type: enhancement Issues and pull requests about possible improvements ux: printing Issues relating to how terms are printed for display
Projects
None yet
Milestone
icebox
Development

No branches or pull requests
3 participants
@UlfNorell @andreasabel @jespercockx