summaryrefslogtreecommitdiff
path: root/dhall/src/errors/NotAFunction.txt
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