Daml-LF: define generic equality

[remyhaemmerle-da]

In order to add a generic Map type to Daml-LF (#2256), we need to come with a proper definition of equality for any of those values that can be used as key.

[remyhaemmerle-da]

Here are 5 different ways to get equality in LF.

1 - making equality builtin fails at runtime if it encounters value that cannot compare (typically functions)

• (+) adding a builtin function of type ∀ α. α→ α→ Boolean
• (-) We have to fully specify the failing cases, and test those and maintain them forever
• (-) Not typesafe
  consider the type variant V = I Int64 | F (Int64 -> Int64) and the expressions
  (a). (\x: V -> (equal @V x x)) @Int64 (I 42)
  (b). (\x: V -> (equal @V x x)) @(Int64 -> Int64) (F (\x: Int64 -> Int64))
  The values a and b typecheck. The evaluation of (a) returns True while the evaluation of (b) throws an error.

2 - do not specify the behaviors of equality on not equatable types (i.e. types that is inhabit only by equatable values)

• (+) adding a builtin function of type ∀ α. α→ α→ Boolean
• (-) not really typesafe
• (-) we have to abandon determinism (at least for all the program that use unspecified use of equalities)

3 - check at runtime the type is equatable

• (+) adding only a builtin functions of type ∀ α. α→ α→ Boolean to that checks at runtime that the type parameter is equatable type
• (-) still not typesafe
  The values (a) and (b) above typecheck.
• (+) a bit safer that porposition 1, in the sens that the evaluation of both (a) and (b) throws an error.
• (-) we have to abandon type erasure.

4 - add a builtin type class for "equatable" type (See spec in 8fad988)

• (+) typesafe ( The value (a) and (b) above do not tyepcheck)
• (+) adding only a builtin functions of type ∀ α. α→ α→ Boolean to the runtime
• (-) complex change in the typechecker/typeinference

5 - make a subkind of star to represent equatable type variables

• (+) typesafe.
• (+) adding only a builtin functions of type ∀ α. α→ α→ Boolean to the runtime
• (-) complex change in the typechecker/typeinference

6 - create a runtime proof that a type is equatable following the approach sketch in the draft PR #3073

• (+) simple addition in the checker and the runtime.
• (-) adding a new type for proof
• (-) we actually have to run the proof construction at runtime to ensure the proof is not built using ERROR builtin or infinite recursion.

[ghost]

#3260 includes a spec for this. Should we close this ticket?