Polymorphic equality

[GuoDCZ]

#1252.

Enable polymorphic equal / not equal comparison for:

• Int, Bool, Float, String: Compare value
• Tuple & List: Pairwise comparison. For List, also check internal type consistency
• Sum: Same as Ocaml
  We disallow comparison of inconsistent types and types contain arrow:
• Dynamic / Static raised Inconsistent when inconsistent types of both side is detected.
• Dynamic / Static raised CompareArrow when either a primitive is an arrow or a compound type contains an arrow
  • A Sum type raise CompareArrow if any entry contains an arrow argument.

Front-end tests:

test 1 == 2 end;
test 1. == 1. end;
test false!= false end;
test "str" == "str" end;
test [1,2,3] != [2,1] end;
test (false, "") == (false, "") end;
type T = +A+B(Int) in
test A == B(1) end;
test A == A end;
test B(2) == B(1) end;
#Static Error: type inconsistency#
1 == 1.;
"" == false;
("1", false) == (1, true);
[1.] == [1];
#Internal Inconsistency also counts#
[1, false] == [1, false];
type T1 = +B+C in
A == C;
#Static Error: type contains arrow#
string_compare == string_compare;
let f = fun x -> x in
f == f;
let a = (1, [f]) in
a == a; 
let a : +A+B(Int->Int) =   in
a == a;
let a : rec R -> A(Int->Int) + R =   in
a == a;
let a = typfun A -> fun x : A -> x in
a == a;
type T2 = +A(Int->Int)+B in
B == B

[cyrus-]

@GuoDCZ let's better handle functions:

• there should be a static error on an equivalence where either side has arrow type
• there should be a dynamic error if at run-time, either side evaluates to a function or cast to arrow type

[GuoDCZ]

@cyrus- just to make sure I got the idea.

When we refer to static error, does it mean something like:

If so, I don't think Info.t.error_inconsistent fit our situation. I am thinking about introducing a new synthesis mode Mode.t.SynEqual, who raises a new error Info.t.error_unexpectedArrow when finding an arrow type. Because it may influence existing code base, IDK if it's OK to do so.

[cyrus-]

Yes. I'm not sure you need a new synthesis mode, but a new error definitely makes sense.

[Negabinary]

I think equality with holes should probably not evaluate - e.g. 2 == ? should stay as 2 == ? rather than evaluate with the unknown, because it's possible the unknown will eventually be filled with the number 2.

[GuoDCZ]

When comparing types that contain an Arrow in static stages, it results in a dynamic error handled within Elaborator.re. However, there is an exception as followings: if the type contains a constructor with Arrow argument, comparing it also requires comparing Arrow, which should not happened. This can only be found out in dynamic stage.

[cyrus-]

We should statically prevent comparison at any sum type where any constructor has an argument that contains an arrow type (recursively including in components of sums and products).

[cyrus-]

We will still need run-time checking as well I suppose, due to polymorphism (we may not know the type it is instantiated with statically), but let's give errors here as early as possible.

[GuoDCZ]

Comments for last commit:

• prevent comparison at any sum type where any constructor has an argument that contains an arrow type
• If A static error is found, Transistor will do nothing but Indet (to avoid duplicate error msg), otherwise make dynamic checks. Errors are found as early as possible.

Remaining Issues:

1. We may create a ListLit of different types without static/dynamic error. And the following comparison happens. If this is not intended, maybe we should handle it in ListLit?
   

let a : ? = 1. in
[1, a] == [1, a]

2. In Hazel type keyword is just alias. In DHExp, Constructor(_) | Ap(Constructor(_),_) have no access to the original sum type. I don't know how to trace its sum type dynamically if errors are not caught in static phase. e.g. Types hided by holes.

type B = +A+B(Int->Int) in
let a : ? = A in
let b : ? = B in
a == b

Good news are we can proper handle sum types if the types are known in static stage.
3. IfThenElse has a similar case when branches types are found and checked in dynamic phase. In case of inconsistency, it use Indet instead of an explicit error like I did for Polymorphic Equality. Maybe we should change either one?

let a : ? = 2. in
1 == a

[cyrus-]

@GuoDCZ the recent merge of #1121 modified elaboration to include the type in the elaborated constructor, so can you update this branch to make use of that to address the issues you identified above? marking as draft until then.

[GuoDCZ]

Remaining type inconsistency checker issue. Can be solved by fixing #1370