first attempt at type scheme compilation

[flupe]

Basic implementation for type scheme compilation.

[flupe]

The following:

record Σ (A : Set) (B : A → Prop) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

Σ-syntax : (A : Set) (B : A → Prop) → Set
Σ-syntax = Σ

syntax Σ-syntax A (λ x → B) = [ x ∈ A ∣ B ]

Arrow : (A B : Set) → Set
Arrow A B = A → B

ListAlias : Set → Set
ListAlias = List

ListAlias' : Set → Set
ListAlias' A = List A

Vec : (A : Set) → Nat → Set
Vec A n = [ xs ∈ List A ∣ Eq (length xs) n ]

Produces the following AST:

[...]
Scheme.Σ:
  mutual inductive(s):
    Σ
    type variables:  [A, B]
      constructors:
        _,_ (2 arg(s))
          fst : @0
          snd : □

Scheme.Σ-syntax:
  type alias:
    type variables: [A, B]
    type: Scheme.Σ{0} @0 □

Scheme.Vec:
  type alias:
    type variables: [A, _]
    type: Scheme.Σ-syntax (Agda.Builtin.List.List{0} □ @0) □

Scheme.ListAlias':
  type alias:
    type variables: [_]
    type: Agda.Builtin.List.List{0} □ @0

Scheme.ListAlias:
  type alias:
    type variables: [_]
    type: Agda.Builtin.List.List{0} □ @0

Scheme.Arrow:
  type alias:
    type variables: [A, B]
    type: @0 → @1
[...]

Which is what we expect, I think.