Remove unneeded parenthesis

[eldesh]

refs #202

Remove redundant parentheses from the type display.
No changes have been made to effect(can) as no decision was made about it.

Algorithm.

Define the precedence of the binding of each syntactic element as follows.

primitives > application > forall > pair > fun

Note

The primitives includes generic Int/Float. Then the type Foo String Int a means Foo String (Int a)

In the display, brackets are added if the priority of the current object is greater than the priority of its sub-element.
The following is pseudo code.

fn fmt_A(&self, ...) {
  self.fmt(..)) ; // print current construct A

  if A.priority() > self.part.priority()
    write("("));
  self.fmt_part();
  if A.priority() > self.part.priority()
    write("("));

  self.fmt(..)) ; // print current construct A
}

Result

For completeness_checking.rs the result is as follows:.
(,) is right-associative, so the parentheses are removed.

• before.

  completeness_checking.an:25:4 error: This pattern of type ((Int a), (Int b)) does not match the type ((Int a), ((Int b)), ((Int c)), (Int d)))) that is being matched on
  | (1, 2) -> 1

• after

  ...
  completeness_checking.an:25:4 error:. This pattern of type Int a, Int b does not match the type Int a, Int b, Int c, Int d that is being matched on
  | (1, 2) -> 1

For instantiation.rs the following applies.
(=>) is also right-associative, so (a => (b => e)) becomes a => b => e.

• before.

  add : (forall a b c d e f g h i. ((a - c => e can g) - (a - b => c can g) -> (a => (b => e can g) can h) can i))
  id : (forall a b. (a -> a can b))
  one : (forall a b c d. ((a => b can d) - a -> b can d))
  two1 : (forall a b c. ((b => b can c) - b -> b can c))
  two2 : ((a => a can c) => (a => a can c) can d)

• after.

  add : forall a b c d e f g h i. ((a - c => e can g) - (a - b => c can g) -> a => b => e can g can h can i)
  id : forall a b. (a -> a can b)
  one : forall a b c d. ((a => b can d) - a -> b can d)
  two1 : forall a b c. ((b => b can c) - b -> b can c)
  two2 : (a => a can c) => a => a can c can d

[jfecher]

This looks amazing! I only have one comment related to the precedence of Int a and Float a

[jfecher]

Suggested change

	TypeApplication(ctor, _) if ctor.is_polymorphic_int_type() => TypePriority::MAX,
	TypeApplication(ctor, _) if ctor.is_polymorphic_float_type() => TypePriority::MAX,

These cases should be removed I think. I haven't looked at it in a bit but I'm assuming these must have been included because of an existing parsing issue or similar but the intention was for Int a to parse like any other type application.

[eldesh]

Yes.
These branches give special treatment to polymorphic numeric types. If these branches were simply removed, the representation of concrete types such as I32 would always be accompanied by parentheses, as in (I32).

// removed `TypeApplication(ctor, _) if ctor.is_polymorphic_int_type() => TypePriority::MAX,`
examples/typechecking/bind.an: Actual stdout differs from expected stdout:
  1| add_one : forall a. (Maybe I32 -> Maybe I32 can a)
   | add_one : forall a. (Maybe (I32) -> Maybe (I32) can a)
..
  4| x : Maybe I32
   | x : Maybe (I32)

Is there any way to properly distinguish between these?

[jfecher]

Oh, good question! Yes, you can distinguish between them. So when you have Int I32 we try to display it as just I32 but internally it will still be TypeApplication(Type::Primitive(PrimitiveType::IntegerType), vec![i32 type]). So you can check for that case specifically by checking what the type variable a is bound to in Int a (if it is bound).

You can find code that checks for this case in fmt_type_application - the is_polymorphic_int_type check on the constructor. Then you can see how fmt_polymorphic_numeral afterward checks the type bindings on the first argument to see whether it is a type variable (unbound) or already bound to a type.

[eldesh]

The point raised have been corrected 💪

[jfecher]

Looks great, thank you!