Reassigning fixity/syntax during renaming import

[GoogleCodeExporter]

Singled out from issue #1194.

This no longer works, but maybe should, as the user has no means to change a fixity during import:

data Bool : Set where true false : Bool

module Product where

  infixr 4 _,_

  record _×_ (A B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B

module List where

  infixr 5 _∷_

  data List (A : Set) : Set where
    []  : List A
    _∷_ : A → List A → List A

open List
open Product using (_×_) renaming (_,_ to _∷_)

-- Non-empty lists.

List⁺ : Set → Set
List⁺ A = A × List A

test : List⁺ Bool
test = true ∷ false ∷ []

We could implement fuzzy fixities (:: has fixity 4-5), or extend the
"renaming" syntax to include fixities or syntax.

open Product using (_×_) renaming (_,_ to infixr 5 _∷_)

Original issue reported on code.google.com by andreas....@gmail.com on 6 Nov 2014 at 6:50

[GoogleCodeExporter]

See also issue #978.

Original comment by andreas....@gmail.com on 10 Nov 2014 at 8:42

[GoogleCodeExporter]

We can almost handle this situation without changing Agda:

  open Product using (_×_)

  infixr 5 _∷_

  pattern _∷_ x xs = Product._,_ x xs

  open List

  -- Non-empty lists.

  List⁺ : Set → Set
  List⁺ A = A × List A

  test : List⁺ Bool
  test = true ∷ false ∷ []

However, the last line is rejected:

  Ambiguous name _∷_. It could refer to any one of
    List._∷_ bound at [...]
    .Bug._∷_ bound at [...]

This looks like a bug to me. I think that pattern synonyms should be
interchangeable with constructors. Another instance of the bug:

  open List
  open Product using (_×_)

  infixr 5 _∷_

  pattern _∷_ x xs = Product._,_ x xs

  Multiple definitions of _∷_. Previous definition at
  [...]
  when scope checking the declaration
    pattern _∷_ x xs = Product._,_ x xs

Is there a reason for not allowing the two pieces of code above?

Original comment by nils.anders.danielsson on 10 Feb 2015 at 2:03

• Changed title: Pattern synonyms are not interchangeable with constructors
• Changed state: InfoNeeded
• Added labels: PatternSynonyms, Priority-Medium, Type-Defect
• Removed labels: Type-Enhancement

[GoogleCodeExporter]

I think that pattern synonyms should be interchangeable with constructors.

I've changed my mind. I don't want to explain what should happen if an overloaded pattern synonym expands to multiple expressions, each with multiple overloaded constructors.

I'm against fuzzy fixities, but perhaps it would be useful to be able to assign a new fixity when importing an operator.

Original comment by nils.anders.danielsson on 19 Feb 2015 at 3:53

• Changed title: Reassigning fixity/syntax during renaming import
• Added labels: Type-Enhancement
• Removed labels: Type-Defect

[nad]

The fix of #4316 has uncovered a bug related to the fix of this issue. To reproduce (using a recent version of Agda without the fix of #4316):

$ cd test/Succeed/ > /dev/null
$ rm -rf _build/
$ agda --no-libraries Issue1346.agda
Checking Issue1346 ([…]/test/Succeed/Issue1346.agda).
$ agda --no-libraries Issue1346Import.agda 
Checking Issue1346Import ([…]/test/Succeed/Issue1346Import.agda).
[…]/test/Succeed/Issue1346Import.agda:9,11-28
Don't know how to parse true ∷ false ∷ []. Could mean any one of:
  true ∷ (false ∷ [])
  true ∷ (false ∷ [])
  true ∷ (false ∷ [])
  (true ∷ false) ∷ []
Operators used in the grammar:
  ∷ (infixr operator, level 4) [_,_ ([…]/test/Succeed/Issue1346.agda:14,17-20)]
  ∷ (infixr operator, level 5) [_∷_ ([…]/test/Succeed/Issue1346.agda:25,5-8)]  
when scope checking true ∷ false ∷ []

The file Issue1346Import.agda type-checks without complaints if a different sequence of commands is used:

$ cd test/Succeed/ > /dev/null
$ rm -rf _build/
$ agda --no-libraries Issue1346Import.agda
Checking Issue1346Import ([…]/test/Succeed/Issue1346Import.agda).
 Checking Issue1346 ([…]/test/Succeed/Issue1346.agda).

[nad]

I added a .warn file to avoid complaints from Travis. However, given that the fix of #4316 is not used when Agda is compiled using versions of GHC prior to 8.4 I would expect that the test suite fails if someone runs it using, say, GHC 8.2.2.

[asr]

I would expect that the test suite fails if someone runs it using, say, GHC 8.2.2.

We run the test suite with all the GHC versions supported in the release branches.

[nad]

I have disabled the test case, and we should fix this issue before the release.

[andreasabel]

I looked at my code and it is correct as far as I can see. However, there is an underlying design issue with the handling of concrete/abstract names.

My theory why this issue surfaced with your refactoring of Import is the following:

1. Fixities (as well as concrete names) are stored in abstract names.
2. Abstract names with the same NameId are identified during serialization.
3. However, when a fixity is updated in an abstract name in ThingsInScope, the NameId does not change (as the NameId is semantic, a UID).
4. What particular version (meaning with what fixity and concrete name) of an abstract name is stored by the serializer, is random.
5. Thus, when going through serialization-deserialization, the fixity one gets for an abstract name can be randomly changed.

My general concerns with the design of concrete/abstract names are:

• Fixity is concerning the concrete syntax, thus it should be attached to concrete names not abstract names.
• An indirection for fixities would be good. Currently they are embedded into (abstract) names, but a map giving the fixity for a concrete name seems more principled. Concrete names would then also get some sort of ID.
• Alternatively, a concrete name would not just be a string, but a string with a fixity.

I guess at some point there was no need to distinguish between concrete name ID and abstract name ID, and this may have caused fixities to be attached to abstract names. But this breaks if one allows fixity of an operator to be changed in the same way as the concrete name may change.

One temporary fix for the issue would be to make the serializer sound, so that it no longer conflates different abstract names with the same NameId.

A more principled fix would separate fixities from abstract names and rethink how to organize the relation between concrete and abstract names. Note that this relation is n:m, meaning one concrete name can stand for different abstract names in a scope (AmbiguousQName), and one abstract name can have different concrete renderings (something we already struggle with heavily in the printer).

[andreasabel]

There might be already a hook in the serializer to have a more refined test for abstract name equality:

agda/src/full/Agda/TypeChecking/Serialise/Base.hs

Lines 73 to 78 in ea6675f

	-- | Two 'QName's are equal if their @QNameId@ is equal.
	type QNameId = [NameId]
	-- | Computing a qualified names composed ID.
	qnameId :: QName -> QNameId
	qnameId (QName (MName ns) n) = map nameId $ n:ns

UPDATE: adding fixity to this name identification did not yet do the job.

[UlfNorell]

How is this a regression? The reassignment feature has not been released.

[andreasabel]

Having fixities in the abstract names also breaks printing after changing the fixities:

postulate
  A B C : Set

module M where

  infixl 4 _+_
  infixl 6 _*_

  postulate
    _+_ _*_ : Set → Set → Set

  T : Set
  T = A + B * C

open M renaming (_*_ to infix 2 _*_)

test : T → A + B * C
test x = x

This prints:

A + B * C !=< A + B * C
when checking that the expression x has type A + B * C

[nad]

One of the test cases (test/Fail/Sections-1.agda) has not been reenabled.

[nad]

That test case is related to #4472.