@@ -1218,21 +1218,19 @@ The following Idris code will compile:
1219 main : IO ()
1219 main : IO ()
1220 main = do
1220 main = do
1221− let x = head [1, 2, 3]
1221+ let x : Integer = head [1,2,3]
1224And will print ``1``. However, the same code with ``head []`` won't compile:
1224And will print ``1``. However, the same code with ``head []`` won't compile:
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
1231− Can't infer argument letty to head,
1231+ When checking argument ok to function Prelude.List.head:
1232− Can't infer argument letty to [],
1232+ Can't find a value of type
1233− Can't infer argument ok to head,
1233+ NonEmpty []
1234− Can't infer argument letty to print,
1235− Can't infer argument constraint to print
1237We can't bind and print ``x`` because ``head []`` doesn't type check.
1235We can't bind and print ``x`` because ``head []`` doesn't type check.
@@ -1247,15 +1245,14 @@ Haskell's ``head`` function.) ``unsafeHead`` might look like this:
1247 unsafeHead (x::xs) = x
1245 unsafeHead (x::xs) = x
1249And although it typechecks and compiles, it will not reduce (that is, evaluation
1247And 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):
1254− unsafe> unsafeHead [1, 2, 3]
1252+ unsafe> the Integer $ unsafeHead [1, 2, 3]
1255 1 : Integer
1253 1 : Integer
1256− unsafe> unsafeHead []
1254+ unsafe> the Integer $ unsafeHead []
1257− (input):Can't infer argument iType to unsafeHead,
1255+ unsafeHead [] : Integer
1258− Can't infer argument iType to []
1260Functions that are not total are known as *partial functions*. As
1257Functions that are not total are known as *partial functions*. As
1261mentioned in the note about ``mutual`` blocks, non-total definitions
1258mentioned in the note about ``mutual`` blocks, non-total definitions