type_path = [ package_name_segment , ":" ] , type_name ; type_application = type_path , { type_expression } ; type_expression = type_path | type_parameter_name | type_application ;
───── Γ ⊢ ◇ Empty Γ ⊢ ◇ x ∉ dom(Γ) ────────── Γ, x ⊢ ◇ Extension
Γ ⊢ p = { t₀ : *, t₁ : *, ... tₙ : * } Γ ⊢ f = { ... } T ∉ dom(Γ) ────────────────────────────────────────── Γ, T ⊢ [record T p f] : *₀ → *₁ → ... → *ₙ TypeDeclareRecord
Γ ⊢ p = { t₀ : *, t₁ : *, ... tₙ : * } Γ ⊢ c = { ... } T ∉ dom(Γ) ─────────────────────────────────────────── Γ, T ⊢ [variant T p f] : *₀ → *₁ → ... → *ₙ TypeDeclareVariant
Γ ⊢ S = { t₀ : *, t₁ : *, ... tₙ : * } Γ ⊢ f : * → *₀ → *₁ → ... → *ₙ |S| ≠ 0 ────────────────────────────────── Γ ⊢ [f t₀ t₁ ... tₙ] : * TypeApplication
(record T [parameter A] [parameter B] [field f0 A] [field f1 B]) (record U) T ; Has kind * → * → * (T) ; Error: T has kind * → * → * but no parameters were supplied (T U) ; Error: T has kind * → * → * but only one parameter was supplied (T U U) ; Has kind *