@@ -1218,21 +1218,19 @@ The following Idris code will compile:
12181218
12191219 main : IO ()
12201220 main = do
1221− let x = head [1, 2, 3]
1221+ let x : Integer = head [1,2,3]
12221222 print x
12231223
12241224And will print ``1``. However, the same code with ``head []`` won't compile:
12251225
12261226::
12271227
1228− test.idr:5:6:When checking right hand side of main with expected type
1228+ test.idr:5:26:When checking right hand side of main with expected type
12291229 IO ()
12301230
1231− Can't infer argument letty to head,
1232− Can't infer argument letty to [],
1233− Can't infer argument ok to head,
1234− Can't infer argument letty to print,
1235− Can't infer argument constraint to print
1231+ When checking argument ok to function Prelude.List.head:
1232+ Can't find a value of type
1233+ NonEmpty []
12361234
12371235We can't bind and print ``x`` because ``head []`` doesn't type check.
12381236
@@ -1247,15 +1245,14 @@ Haskell's ``head`` function.) ``unsafeHead`` might look like this:
12471245 unsafeHead (x::xs) = x
12481246
12491247And although it typechecks and compiles, it will not reduce (that is, evaluation
1250−of the function will cause its type to change):
1248+of the function will cause it to change):
12511249
12521250::
12531251
1254− unsafe> unsafeHead [1, 2, 3]
1252+ unsafe> the Integer $ unsafeHead [1, 2, 3]
12551253 1 : Integer
1256− unsafe> unsafeHead []
1257− (input):Can't infer argument iType to unsafeHead,
1258− Can't infer argument iType to []
1254+ unsafe> the Integer $ unsafeHead []
1255+ unsafeHead [] : Integer
12591256
12601257Functions that are not total are known as *partial functions*. As
12611258mentioned in the note about ``mutual`` blocks, non-total definitions