summaryrefslogtreecommitdiff
path: root/dhall/src/error/text/UnboundVariable.txt
blob: bd7d483b18d7fed414aeda5005a160799e28165a (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
Explanation: Expressions can only reference previously introduced (i.e. "bound")
variables that are still "in scope"

For example, the following valid expressions introduce a "bound" variable named
❰x❱:


    ┌─────────────────┐
    │ λ(x : Bool) → x │  Anonymous functions introduce "bound" variables
    └─────────────────┘
        ⇧
        This is the bound variable


    ┌─────────────────┐
    │ let x = 1 in x  │  ❰let❱ expressions introduce "bound" variables
    └─────────────────┘
          ⇧
          This is the bound variable


However, the following expressions are not valid because they all reference a
variable that has not been introduced yet (i.e. an "unbound" variable):


    ┌─────────────────┐
    │ λ(x : Bool) → y │  The variable ❰y❱ hasn't been introduced yet
    └─────────────────┘
                    ⇧
                    This is the unbound variable


    ┌──────────────────────────┐
    │ (let x = True in x) && x │  ❰x❱ is undefined outside the parentheses
    └──────────────────────────┘
                             ⇧
                             This is the unbound variable


    ┌────────────────┐
    │ let x = x in x │  The definition for ❰x❱ cannot reference itself
    └────────────────┘
              ⇧
              This is the unbound variable


Some common reasons why you might get this error:

● You misspell a variable name, like this:


    ┌────────────────────────────────────────────────────┐
    │ λ(empty : Bool) → if emty then "Empty" else "Full" │
    └────────────────────────────────────────────────────┘
                           ⇧
                           Typo


● You misspell a reserved identifier, like this:


    ┌──────────────────────────┐
    │ foral (a : Type) → a → a │
    └──────────────────────────┘
      ⇧
      Typo


● You tried to define a recursive value, like this:


    ┌─────────────────────┐
    │ let x = x + +1 in x │
    └─────────────────────┘
              ⇧
              Recursive definitions are not allowed


● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱


        Unbound variable
        ⇩
    ┌─────────────────┐
    │  (x : Bool) → x │
    └─────────────────┘
      ⇧
      A ❰λ❱ here would transform this into a valid anonymous function 


        Unbound variable
        ⇩
    ┌────────────────────┐
    │  (x : Bool) → Bool │
    └────────────────────┘
      ⇧
      A ❰∀❱ or ❰forall❱ here would transform this into a valid function type