summaryrefslogtreecommitdiff
path: root/dhall/src/errors/AnnotMismatch.txt
blob: 4904bf89f32acadd8eec6b31d59d2b1e6e4d9720 (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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
Explanation: Every function declares what type or kind of argument to accept

For example:


    ┌───────────────────────────────┐
    │ λ(x : Bool) → x : Bool → Bool │  This anonymous function only accepts
    └───────────────────────────────┘  arguments that have type ❰Bool❱
                        ⇧
                        The function's input type


    ┌───────────────────────────────┐
    │ Natural/even : Natural → Bool │  This built-in function only accepts
    └───────────────────────────────┘  arguments that have type ❰Natural❱
                     ⇧
                     The function's input type


    ┌───────────────────────────────┐
    │ λ(a : Type) → a : Type → Type │  This anonymous function only accepts
    └───────────────────────────────┘  arguments that have kind ❰Type❱
                        ⇧
                        The function's input kind


    ┌────────────────────┐
    │ List : Type → Type │  This built-in function only accepts arguments that
    └────────────────────┘  have kind ❰Type❱
             ⇧
             The function's input kind


For example, the following expressions are valid:


    ┌────────────────────────┐
    │ (λ(x : Bool) → x) True │  ❰True❱ has type ❰Bool❱, which matches the type
    └────────────────────────┘  of argument that the anonymous function accepts


    ┌─────────────────┐
    │ Natural/even +2 │  ❰+2❱ has type ❰Natural❱, which matches the type of
    └─────────────────┘  argument that the ❰Natural/even❱ function accepts,


    ┌────────────────────────┐
    │ (λ(a : Type) → a) Bool │  ❰Bool❱ has kind ❰Type❱, which matches the kind
    └────────────────────────┘  of argument that the anonymous function accepts


    ┌───────────┐
    │ List Text │  ❰Text❱ has kind ❰Type❱, which matches the kind of argument
    └───────────┘  that that the ❰List❱ function accepts


However, you can $_NOT apply a function to the wrong type or kind of argument

For example, the following expressions are not valid:


    ┌───────────────────────┐
    │ (λ(x : Bool) → x) "A" │  ❰"A"❱ has type ❰Text❱, but the anonymous function
    └───────────────────────┘  expects an argument that has type ❰Bool❱


    ┌──────────────────┐
    │ Natural/even "A" │  ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
    └──────────────────┘  expects an argument that has type ❰Natural❱


    ┌────────────────────────┐
    │ (λ(a : Type) → a) True │  ❰True❱ has type ❰Bool❱, but the anonymous
    └────────────────────────┘  function expects an argument of kind ❰Type❱


    ┌────────┐
    │ List 1 │  ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
    └────────┘  argument that has kind ❰Type❱


You tried to invoke the following function:

↳ $txt0

... which expects an argument of type or kind:

↳ $txt1

... on the following argument:

↳ $txt2

... which has a different type or kind:

↳ $txt3

Some common reasons why you might get this error:

● You omit a function argument by mistake:


    ┌────────────────────────────────────────┐
    │ List/head   ([1, 2, 3] : List Integer) │
    └────────────────────────────────────────┘
                ⇧
                ❰List/head❱ is missing the first argument,
                which should be: ❰Integer❱


● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱

    ┌────────────────┐
    │ Natural/even 2 │
    └────────────────┘
                   ⇧
                   This should be ❰+2❱