Special treatment of attribute followed by underscore in pretty-printer

[nad]

Why is the following code used to print things with certain attributes?

agda/src/full/Agda/Syntax/Concrete/Pretty.hs

Lines 82 to 95 in fc4e2fa

	prettyRelevance :: LensRelevance a => a -> Doc -> Doc
	prettyRelevance a d =
	if render d == "_" then d else pretty (getRelevance a) <> d
	prettyQuantity :: LensQuantity a => a -> Doc -> Doc
	prettyQuantity a d =
	if render d == "_" then d else pretty (getQuantity a) <+> d
	prettyErased :: Erased -> Doc -> Doc
	prettyErased = prettyQuantity . asQuantity
	prettyCohesion :: LensCohesion a => a -> Doc -> Doc
	prettyCohesion a d =
	if render d == "_" then d else pretty (getCohesion a) <+> d

I think this code is based on code for irrelevance added by @andreasabel back in 2010 in a commit (8fd48ca) with the following commit message:

Added DontCare to Internal and Abstract syntax to print erased stuff more nicely as underscore instead of Prop.

I'm guessing that the original motivation no longer applies, and I doubt that this motivation ever applied for @0. Furthermore it might be inefficient to call render d in this way (depending on how lazy render is). Could the special treatment of "_" be removed?

[nad]

I removed the special treatment of "_" and ran make fail, and one test case was affected. Now λ (@0 _) → Set is printed as λ (@0 _) → Set instead of as λ (_) → Set. The old behaviour is incorrect.