Support user-defined polymorphic type constructors

[shonfeder]

While we support user-defined type aliases, such as

type IntPair = (int, int)

and we allow type variables to appear on the right hand side

type Pair = (a, b)

we don't support any way for users to define type constructors that are parametric over a type. E.g.,

type Pair[a] = (a, a)

While we can define

type SameTypedPair = (a, a)

we have no way to express the shared type constraint that would let us define a well typed projection out of that pair:

def f(p: Pair[a]): a = p._1

This would already be useful to allow us to define interfaces over data structures, e.g.:

type OrdMap[k, v] = (m: k -> v, o: List[k])

This will be even more desirable once we have support for sum types. With the addition of user defined polymorphic type constructors, we can define the standard Option[a] and Either[a, b] type constructors (with associated operators). Otherwise, these will have to be implemented as builtins.

Discussed with @bugarela who noted

this could actually simplify the type system a bit, since currently we have separate typescript interfaces for List, Set and Fun(maps). Those could all be written as a generic parametric type (edited)

Related to #1062.

---

As per #1073 (comment), the implementation plan is

• Add IR nodes for type abstraction and type function application #1296
• Add parser support for polymorphic type declaration #1297
• Add support for polymorphic type declaration in the type checking constraints #1298

[shonfeder]

The "generality" checking we do on annotations makes it impossible even to use the existing support for type variables in aliases.

Given

// option.qnt
module option {

  type Option =
    | Some(a)
    | None

}

We get

$  quint typecheck examples/spells/option.qnt 
/quint/examples/spells/option.qnt:4:7 - error: [QNT000] Type annotation is too general: a should be t___SomeParam_5
Checking variable a
Checking type annotation (a) => Option

4:     | Some(a)
         ^^^^^^^

error: typechecking failed

So polymorphic sum types are out of reach unless we address this issue or change the checking on this rule.

[shonfeder]

After a bit of discovery work, here's the high level plan:

IR Representation

We'll follow the standard approach for representing polymorphic types.

Type abstraction represents the type-level variable binding formalized in
System-F via Λ. It will repeat the same pattern of our operators, but at the
type level.

Type function application will just look operator application, but at the type
level.

Syntax

Our current builtin support for polymorphic types looks like this: Set[a],
List[a]. The syntax for declaring polymorphic types follows naturally. We just
have to extend our current rule for type declarations to allow specifying
variables in the head:

type-declaration := 
   ...
   | 'type' ID ('[' typeVar? (, typeVar)* ']') = type

E.g., to define the type constructor for the option type, we would write

type Option[a] =
  | Some(a)
  | None

The existing syntax for type application gives us a form like Option[T] to
specify the concrete type for a type T.

Statics

To make the minimal change in our existing type system, we can reuse the
existing TypeSchema type, and just convert type application constraints
equating the parameter type variables to the type arguments.

Integration with Apalache

I do not currently foresee needing to make any changes for Apalache
compatibility. We expect all types to be inlined before exporting the IR to
Apalache, and totally ignore type declarations, and all inlined types should be
concrete after type inference is done.

[shonfeder]

🎉