Support discriminated unions in the type system

[bugarela]

We need to implement variants and use them to type discriminated unions and their operators (match) in the type system.

• Implement type checking and inference for variant construction via the exotic variant operator introduced in Add syntax for match and variant operators #1206
• Implement type checking and inference for variant elimination via the exotic match operator introduced in Add syntax for match and variant operators #1206

[shonfeder]

Leaving a note here on (what looks to me like) a somewhat unfortunate variation from the representation of discriminated unions in the TlaType1 representation:

afaiu, TlaType1 follows the approach to extensible variants described in https://homepage.cs.uiowa.edu/~jgmorrs/pubs/morris-popl2019-rows.pdf, in (extensible) variants obtained through the sum of a single record. But in TNT we are representing unions as a set of tagged rows.

E.g.,

https://github.com/informalsystems/tnt/blob/a0ac34896f5205e3b8d9894ecec1a556df6cf303/tntc/test/types/parser.test.ts#L82-L109

If we were following the "Abstracting Extensible Data Types" and TlaType1, we would have instead something like

    \\ Maybe we'd have a different notation for the union tags
    const type = parseType('| a(int) | b(bool)')

    assert.isTrue(type.isRight())
    type.map(value => assert.deepEqual(value, {
      kind: 'union',
      row: {
        kind: 'row',
        fields: [
          { fieldName: 'a', fieldType: { kind: 'int', id: 1n } },
          { fieldName: 'b', fieldType: { kind: 'bool', id: 2n } }],
        other: { kind: 'empty' },
      },
      id: 3n,
    }
    ))
  })

This seems much nicer to me on every level:

• The input syntax is clear and more flexible
• The implementation is simpler
• It seems to be more elegant theoretically, in allowing rows to express both records and variants by application of product or sum operations.

[konnov]

I also like the approach implemented in TlaType1 currently, though it may have some quirks we have not had time to think about.