@@ -103,6 +103,59 @@ the difference between:
103103 Idris> \n, m => n + (S m)
104104 \n => \m => plus n (S m) : Nat -> Nat -> Nat
105105
106+
107+Why can't I use a function with no arguments in a type?
108+=======================================================
109+
110+If you use a name in a type which begins with a lower case letter, and which is
111+not applied to any arguments, then Idris will treat it as an implicitly
112+bound argument. For example:
113+
114+.. code-block:: idris
115+
116+ append : Vect n ty -> Vect m ty -> Vect (n + m) ty
117+
118+Here, ``n``, ``m``, and ``ty`` are implicitly bound. This rule applies even
119+if there are functions defined elsewhere with any of these names. For example,
120+you may also have:
121+
122+.. code-block:: idris
123+
124+ ty : Type
125+ ty = String
126+
127+Even in this case, ``ty`` is still considered implicitly bound in the definition
128+of ``append``, rather than making the type of ``append`` equivalent to...
129+
130+.. code-block:: idris
131+
132+ append : Vect n String -> Vect m String -> Vect (n + m) String
133+
134+...which is probably not what was intended! The reason for this rule is so
135+that it is clear just from looking at the type of ``append``, and no other
136+context, what the implicitly bound names are.
137+
138+If you want to use an unapplied name in a type, you have two options. You
139+can either explicitly qualify it, for example, if ``ty`` is defined in the
140+namespace ``Main`` you can do the following:
141+
142+.. code-block:: idris
143+
144+ append : Vect n Main.ty -> Vect m Main.ty -> Vect (n + m) Main.ty
145+
146+Alternatively, you can use a name which does not begin with a lower case
147+letter, which will never be implicitly bound:
148+
149+.. code-block:: idris
150+
151+ Ty : Type
152+ Ty = String
153+
154+ append : Vect n Ty -> Vect m Ty -> Vect (n + m) Ty
155+
156+As a convention, if a name is intended to be used as a type synonym, it is
157+best for it to begin with a capital letter to avoid this restriction.
158+
106159I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?
107160=============================================================================================
108161