unison/unison-src/transcripts/kind-inference.md

.> builtins.merge

A type param cannot have conflicting kind constraints within a single decl

conflicting constraints on the kind of a in a product

unique type T a = T a (a Nat)

conflicting constraints on the kind of a in a sum

unique type T a 
  = Star a 
  | StarStar (a Nat)

Kinds are inferred by decl component

Successfully infer a in Ping a to be of kind * -> * by inspecting its component-mate Pong.

unique type Ping a = Ping Pong
unique type Pong = Pong (Ping Optional)

Catch the conflict on the kind of a in Ping a. Ping restricts a to *, whereas Pong restricts a to * -> *.

unique type Ping a = Ping a Pong
unique type Pong = Pong (Ping Optional)

Successful example between mutually recursive type and ability

unique type Ping a = Ping (a Nat -> {Pong Nat} ())
unique ability Pong a where
  pong : Ping Optional -> ()

Catch conflict between mutually recursive type and ability

unique type Ping a = Ping (a -> {Pong Nat} ())
unique ability Pong a where
  pong : Ping Optional -> ()

Consistent instantiation of T's a parameter in S

unique type T a = T a

unique type S = S (T Nat)

Delay kind defaulting until all components are processed. Here S constrains the kind of T's a parameter, although S is not in the same component as T.

unique type T a = T

unique type S = S (T Optional)

Catch invalid instantiation of T's a parameter in S

unique type T a = T a

unique type S = S (T Optional)

Checking annotations

Catch kind error in type annotation

test : Nat Nat
test = 0

Catch kind error in annotation example 2

test : Optional -> ()
test _ = ()

Catch kind error in annotation example 3

unique type T a = T (a Nat)

test : T Nat -> ()
test _ = ()

Catch kind error in scoped type variable annotation

unique type StarStar a = StarStar (a Nat)
unique type Star a = Star a

test : StarStar a -> ()
test _ = 
  buggo : Star a
  buggo = bug ""
  ()

Effect/type mismatch

Effects appearing where types are expected

unique ability Foo where
  foo : ()

test : Foo -> ()
test _ = ()

Types appearing where effects are expected

test : {Nat} ()
test _ = ()

Cyclic kinds

unique type T a = T (a a)

unique type T a b = T (a b) (b a)

unique type Ping a = Ping (a Pong)
unique type Pong a = Pong (a Ping)