Lifting redundant constructor restrictions

type:changed

problems

• tv_opt was almost ignored in the typing of E_constructor (if not to substitute the free variables in the type of constructor parameter)
• evaluate_type was weird ? it seems to me that we should look-up the context in the E_app and E_var cases, and add to the context in the T_for_all T_abstraction cases ?

the redundant constructor problem (we could not write that)

type union_a =
| Add of int
| Remove of int

type union_b =
| Add of nat
| Config of nat


let x = (Add 1 : union_a) , (Add 1n : union_b)

Although we could write this ! but it was wrong:

type t1 =
  | B of nat
  | C of int
  | D of string
  | A of unit

type t2 =
  [@layout:comb]
  | B of nat
  | C of int
  | D of string
  | A of unit

let x = (B 42n : t1) , (B 42n : t2)

> ../ligo.37.0 compile expression cameligo "x" --ini result/oueach.mligo
(Pair (Left (Right 42)) (Left (Right 42)))

> ligo compile expression cameligo "x" --ini result/oueach.mligo
(Pair (Left (Right 42)) (Left 42))

Semantic: The most recently declared constructor is chosen by default (this is more or less OCaml behavior). A warning will pop if two constructor with the same label and same parameter type are in scope:

type union_a =
| A of int
| B of int

type union_b =
| A of int
| B of nat
(* here we expect a warning because both A constructor have the same parameter type *)
let main = fun (() , (_: union_b)) -> ([]: operation list) , A 1

File "test.mligo", line 10, characters 61-66:
  9 | 
 10 | let main = fun (() , (_: union_b)) -> ([]: operation list) , Add 1

The type of this value is ambiguous: Inferred type is union_b but could be of type union_a.
Hint: You might want to add a type annotation. 

Changelog details:

Lifting restrictions on redundant constructors

It is now possible to declare variant types sharing the same constructors as in:

type t1 =
| Foo of int
| Bar of string

type t2 =
| Foo of int
| Baz of nat