2023-09-20 22:20:53 +03:00
|
|
|
|
|
|
|
```ucm:hide
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> builtins.merge
|
2023-09-20 22:20:53 +03:00
|
|
|
```
|
|
|
|
|
|
|
|
## A type param cannot have conflicting kind constraints within a single decl
|
|
|
|
|
|
|
|
conflicting constraints on the kind of `a` in a product
|
|
|
|
```unison:error
|
|
|
|
unique type T a = T a (a Nat)
|
|
|
|
```
|
|
|
|
|
|
|
|
conflicting constraints on the kind of `a` in a sum
|
|
|
|
```unison:error
|
|
|
|
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`.
|
|
|
|
```unison
|
|
|
|
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 `* -> *`.
|
|
|
|
```unison:error
|
|
|
|
unique type Ping a = Ping a Pong
|
|
|
|
unique type Pong = Pong (Ping Optional)
|
|
|
|
```
|
|
|
|
|
|
|
|
Successful example between mutually recursive type and ability
|
|
|
|
```unison
|
|
|
|
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
|
|
|
|
```unison:error
|
|
|
|
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`
|
|
|
|
```unison
|
|
|
|
unique type T a = T a
|
|
|
|
|
|
|
|
unique type S = S (T Nat)
|
|
|
|
```
|
|
|
|
|
2023-10-30 16:56:05 +03:00
|
|
|
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`.
|
2023-10-30 16:51:55 +03:00
|
|
|
```unison
|
2023-10-27 17:37:08 +03:00
|
|
|
unique type T a = T
|
|
|
|
|
|
|
|
unique type S = S (T Optional)
|
|
|
|
```
|
|
|
|
|
2023-09-20 22:20:53 +03:00
|
|
|
Catch invalid instantiation of `T`'s `a` parameter in `S`
|
|
|
|
```unison:error
|
|
|
|
unique type T a = T a
|
|
|
|
|
|
|
|
unique type S = S (T Optional)
|
|
|
|
```
|
|
|
|
|
|
|
|
## Checking annotations
|
|
|
|
|
|
|
|
Catch kind error in type annotation
|
|
|
|
```unison:error
|
|
|
|
test : Nat Nat
|
|
|
|
test = 0
|
|
|
|
```
|
|
|
|
|
|
|
|
Catch kind error in annotation example 2
|
|
|
|
```unison:error
|
|
|
|
test : Optional -> ()
|
|
|
|
test _ = ()
|
|
|
|
```
|
|
|
|
|
|
|
|
Catch kind error in annotation example 3
|
|
|
|
```unison:error
|
|
|
|
unique type T a = T (a Nat)
|
|
|
|
|
|
|
|
test : T Nat -> ()
|
|
|
|
test _ = ()
|
|
|
|
```
|
|
|
|
|
|
|
|
Catch kind error in scoped type variable annotation
|
|
|
|
```unison:error
|
|
|
|
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
|
|
|
|
```unison:error
|
|
|
|
unique ability Foo where
|
|
|
|
foo : ()
|
|
|
|
|
|
|
|
test : Foo -> ()
|
|
|
|
test _ = ()
|
|
|
|
```
|
|
|
|
|
|
|
|
Types appearing where effects are expected
|
|
|
|
```unison:error
|
|
|
|
test : {Nat} ()
|
|
|
|
test _ = ()
|
|
|
|
```
|
|
|
|
|
|
|
|
## Cyclic kinds
|
|
|
|
|
|
|
|
```unison:error
|
|
|
|
unique type T a = T (a a)
|
|
|
|
```
|
2023-09-21 20:49:30 +03:00
|
|
|
|
|
|
|
```unison:error
|
|
|
|
unique type T a b = T (a b) (b a)
|
|
|
|
```
|
|
|
|
|
|
|
|
```unison:error
|
|
|
|
unique type Ping a = Ping (a Pong)
|
|
|
|
unique type Pong a = Pong (a Ping)
|
|
|
|
```
|