blob: dd2695dc9a402e189b7f47284e9b05493e05ca5f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
Explanation: A function can return an output "term" that has a given "type",
like this:
┌────────────────────┐
│ ∀(x : Text) → Bool │ This is the type of a function that returns an
└────────────────────┘ output term that has type ❰Bool❱
⇧
This is the type of the output term
┌────────────────┐
│ Bool → Integer │ This is the type of a function that returns an output
└────────────────┘ term that has type ❰Int❱
⇧
This is the type of the output term
... or a function can return an output "type" that has a given "kind", like
this:
┌────────────────────┐
│ ∀(a : Type) → Type │ This is the type of a function that returns an
└────────────────────┘ output type that has kind ❰Type❱
⇧
This is the kind of the output type
┌──────────────────────┐
│ (Type → Type) → Type │ This is the type of a function that returns an
└──────────────────────┘ output type that has kind ❰Type❱
⇧
This is the kind of the output type
Other outputs are $_NOT valid, like this:
┌─────────────────┐
│ ∀(x : Bool) → x │ ❰x❱ is a "term" and not a "type" nor a "kind" so the
└─────────────────┘ output cannot have "type" ❰x❱ or "kind" ❰x❱
⇧
This is not a type or kind
┌─────────────┐
│ Text → True │ ❰True❱ is a "term" and not a "type" nor a "kind" so the
└─────────────┘ output cannot have "type" ❰True❱ or "kind" ❰True❱
⇧
This is not a type or kind
You specified that your function outputs a:
↳ $txt
... which is neither a type nor a kind:
Some common reasons why you might get this error:
● You use ❰∀❱ instead of ❰λ❱ by mistake, like this:
┌────────────────┐
│ ∀(x: Bool) → x │
└────────────────┘
⇧
Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function
|
