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 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007
|
.. _error-index:
Compiler Error Index
====================
Elaboration on type errors produced by the compiler. Many error
messages contain links to the sections below.
Uniqueness errors
-----------------
.. _use-after-consume:
"Using *x*, but this was consumed at *y*."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A core principle of uniqueness typing (see :ref:`in-place-updates`) is
that after a variable is "consumed", it must not be used again. For
example, this is invalid, and will result in the error above:
.. code-block:: futhark
let y = x with [0] = 0
in x
Several operations can *consume* a variable: array update expressions,
calling a function with unique-typed parameters, or passing it as the
initial value of a unique-typed loop parameter. When a variable is
consumed, its *aliases* are also considered consumed. Aliasing is the
possibility of two variables occupying the same memory at run-time.
For example, this will fail as above, because ``y`` and ``x`` are
aliased:
.. code-block:: futhark
let y = x
let z = y with [0] = 0
in x
We can always break aliasing by using a ``copy`` expression:
.. code-block:: futhark
let y = copy x
let z = y with [0] = 0
in x
.. _not-consumable:
"Would consume *x*, which is not consumable"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This error message occurs for programs that try to perform a
consumption (such as an in-place update) on variables that are not
consumable. For example, it would occur for the following program:
.. code-block:: futhark
def f (a: []i32) =
let a[0] = a[0]+1
in a
Only arrays with a a *unique array type* can be consumed. Such a type
is written by prefixing the array type with an asterisk. The program
could be fixed by writing it like this:
.. code-block:: futhark
def f (a: *[]i32) =
let a[0] = a[0]+1
in a
Note that this places extra obligations on the caller of the ``f``
function, since it now *consumes* its argument. See
:ref:`in-place-updates` for the full details.
You can always obtain a unique copy of an array by using
``copy``:
.. code-block:: futhark
def f (a: []i32) =
let a = copy a
let a[0] = a[0]+1
in a
But note that in most cases (although not all), this subverts the
purpose of using in-place updates in the first place.
.. _return-aliased:
"Unique-typed return value of *x* is aliased to *y*, which is not consumable"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This can be caused by a function like this:
.. code-block:: futhark
def f (xs: []i32) : *[]i32 = xs
We are saying that ``f`` returns a *unique* array - meaning it has no
aliases - but at the same time, it aliases the parameter *xs*, which
is not marked as being unique (see :ref:`in-place-updates`). This
violates one of the core guarantees provided by uniqueness types,
namely that a unique return value does not alias any value that might
be used in the future. Imagine if this was permitted, and we had a
program that used ``f``:
.. code-block:: futhark
let b = f a
let b[0] = x
...
The update of ``b`` is fine, but if ``b`` was allowed to alias ``a``
(hence occupying the same memory), then we would be modifying ``a`` as
well, which is a violation of referential transparency.
As with most uniqueness errors, it can be fixed by using ``copy xs``
to break the aliasing. We can also change the type of ``f`` to take a
unique array as input:
.. code-block:: futhark
def f (xs: *[]i32) : *[]i32 = xs
This makes ``xs`` "consumable", in the sense used by the error message.
.. _unique-return-aliased:
"A unique-typed component of the return value of *x* is aliased to some other component"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Caused by programs like the following:
.. code-block:: futhark
def main (xs: *[]i32) : (*[]i32, *[]i32) = (xs, xs)
While we are allowed to "consume" ``xs``, as it is a unique parameter,
this function is trying to return two unique values that alias each
other. This violates one of the core guarantees provided by
uniqueness types, namely that a unique return value does not alias any
value that might be used in the future (see :ref:`in-place-updates`) -
and in this case, the two values alias each other. We can fix this by
inserting copies to break the aliasing:
.. code-block:: futhark
def main (xs: *[]i32) : (*[]i32, *[]i32) = (xs, copy xs)
.. _self-aliasing-arg:
"Argument passed for consuming parameter is self-aliased."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Caused by programs like the following:
.. code-block:: futhark
def g (t: *([]i64, []i64)) = 0
def f n =
let x = iota n
in g (x,x)
The function ``g`` expects to consume two separate ``[]i64`` arrays,
but ``f`` passes it a tuple containing two references to the same
physical array. This is not allowed, as ``g`` must be allowed to
assume that components of consuming record- or tuple parameters have
no internal aliases. We can fix this by inserting copies to break the
aliasing:
.. code-block:: futhark
def f n =
let x = iota n
in g (copy (x,x))
Alternative, we could duplicate the expression producing the array:
.. code-block:: futhark
def f n =
g (iota n, iota n))
.. _consuming-parameter:
"Consuming parameter passed non-unique argument"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Caused by programs like the following:
.. code-block:: futhark
def update (xs: *[]i32) = xs with [0] = 0
def f (ys: []i32) = update ys
The update ``function`` *consumes* its ``xs`` argument to perform an
:ref:`in-place update <in-place-updates>`, as denoted by the asterisk
before the type. However, the ``f`` function tries to pass an array
that it is not allowed to consume (no asterisk before the type).
One solution is to change the type of ``f`` so that it also consumes
its input, which allows it to pass it on to ``update``:
.. code-block:: futhark
def f (ys: *[]i32) = update ys
Another solution to ``copy`` the array that we pass to ``update``:
.. code-block:: futhark
def f (ys: []i32) = update (copy ys)
.. _consuming-argument:
"Non-consuming higher-order parameter passed consuming argument."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This error occurs when we have a higher-order function that expects a
function that does *not* consume its arguments, and we pass it one
that does:
.. code-block:: futhark
def apply 'a 'b (f: a -> b) (x: a) = f x
def consume (xs: *[]i32) = xs with [0] = 0
def f (arr: *[]i32) = apply consume arr
We can fix this by changing ``consume`` so that it does not have to
consume its argument, by adding a ``copy``:
.. code-block:: futhark
def consume (xs: []i32) = copy xs with [0] = 0
Or we can create a variant of ``apply`` that accepts a consuming
function:
.. code-block:: futhark
def apply 'a 'b (f: *a -> b) (x: *a) = f x
.. _alias-free-variable:
"Function result aliases the free variable *x*"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Caused by definitions such as the following:
.. code-block:: futhark
def x = [1,2,3]
def f () = x
To simplify the tracking of aliases, the Futhark type system requires
that the result of a function may only alias the function parameters,
not any free variables. Use ``copy`` to fix this:
.. code-block:: futhark
def f () = copy x
.. _size-expression-bind:
"Size expression with binding is replaced by unknown size."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To illustrate this error, consider the following program
.. code-block:: futhark
def main (xs: *[]i64) =
let a = iota (let n = 10 in n+n)
in ...
Intuitively, the type of ``a`` should be ``[let n = 10 in n+n]i32``,
but this puts a binding into a size expression, which is invalid.
Therefore, the type checker invents an :term:`unknown size`
variable, say ``l``, and assigns ``a`` the type ``[l]i32``.
.. _size-expression-consume:
"Size expression with consumption is replaced by unknown size."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To illustrate this error, consider the following program
.. code-block:: futhark
def consume (xs: *[]i64): i64 = xs[0]
def main (xs: *[]i64) =
let a = iota (consume xs)
in ...
Intuitively, the type of ``a`` should be ``[consume ys]i32``, but this
puts a consumption of the array ``ys`` into a size expression, which
is invalid. Therefore, the type checker invents an :term:`unknown
size` variable, say ``l``, and assigns ``a`` the type ``[l]i32``.
.. _inaccessible-size:
"Parameter *x* refers to size *y* which will not be accessible to the caller
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This happens when the size of an array parameter depends on a name
that cannot be expressed in the function type:
.. code-block:: futhark
def f (x: i64, y: i64) (A: [x]bool) = true
Intuitively, this function might have the following type:
.. code-block:: futhark
val f : (x: i64, y: i64) -> [x]bool -> bool
But this is not currently a valid Futhark type. In a function type,
each parameter can be named *as a whole*, but it cannot be taken apart
in a pattern. In this case, we could fix it by splitting the tuple
parameter into two separate parameters:
.. code-block:: futhark
def f (x: i64) (y: i64) (A: [x]bool) = true
This gives the following type:
.. code-block:: futhark
val f : (x: i64) -> (y: i64) -> [x]bool -> bool
Another workaround is to loosen the static safety, and use a size
coercion to give A its expected size:
.. code-block:: futhark
def f (x: i64, y: i64) (A_unsized: []bool) =
let A = A_unsized :> [x]bool
in true
This will produce a function with the following type:
.. code-block:: futhark
val f [d] : (i64, i64) -> [d]bool -> bool
This does however lose the constraint that the size of the array must
match one of the elements of the tuple, which means the program may
fail at run-time.
The error is not always due to an explicit type annotation. It might
also be due to size inference:
.. code-block:: futhark
def f (x: i64, y: i64) (A: []bool) = zip A (iota x)
Here the type rules force ``A`` to have size ``x``, leading to a
problematic type. It can be fixed using the techniques above.
.. _aliases-previously-returned:
"Return value for consuming loop parameter *x* aliases previously returned value"
---------------------------------------------------------------------------------
This error occurs when you have a loop with multiple loop parameters,
at least one of which is consuming, and the values returned by the
loop body alias each other. This would result in the consuming loop
parameter aliasing another loop parameter, which is not allowed. It is
essentially :ref:`unique-return-aliased` from a loop perspective.
A (contrived) example of this error is the following:
.. code-block:: futhark
loop (acc: []f64, arr: *[][]f64) for i < length arr-1 do
let arr[i] = acc
-- Error, because 'arr[i]' and 'arr' are aliased, yet the latter
-- is consumed.
in (arr[i+1], arr)
Size errors
-----------
.. _unused-size:
"Size *x* unused in pattern."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Caused by expressions like this:
.. code-block:: futhark
def [n] (y: i32) = x
And functions like this:
.. code-block:: futhark
def f [n] (x: i32) = x
Since ``n`` is not the size of anything, it cannot be assigned a value
at runtime. Hence this program is rejected.
.. _causality-check:
"Causality check"
~~~~~~~~~~~~~~~~~
Causality check errors occur when the program is written in such a way
that a size is needed before it is actually computed. See
:ref:`causality` for the full rules. Contrived example:
.. code-block:: futhark
def f (b: bool) (xs: []i32) =
let a = [] : [][]i32
let b = [filter (>0) xs]
in a[0] == b[0]
Here the inner size of the array ``a`` must be the same as the inner
size of ``b``, but the inner size of ``b`` depends on a ``filter``
operation that is executed after ``a`` is constructed.
There are various ways to fix causality errors. In the above case, we
could merely change the order of statements, such that ``b`` is bound
first, meaning that the size is available by the time ``a`` is bound.
In many other cases, we can lift out the "size-producing" expressions
into a separate ``let``-binding preceding the problematic expressions.
.. _unknown-param-def:
"Unknown size *x* in parameter of *y*"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This error occurs when you define a function that can never be
applied, as it requires an input of a specific size, and that size is
an :term:`unknown size`. Somewhat contrived example:
.. code-block:: futhark
def f (x: bool) =
let n = if x then 10 else 20
in \(y: [n]bool) -> ...
The above constructs a function that accepts an array of size 10 or
20, based on the value of ``x`` argument. But the type of ``f true``
by itself would be ``?[n].[n]bool -> bool``, where the ``n`` is
unknown. There is no way to construct an array of the right size, so
the type checker rejects this program. (In a fully dependently typed
language, the type would have been ``[10]bool -> bool``, but Futhark
does not do any type-level computation.)
In most cases, this error means you have done something you didn't
actually mean to. However, in the case that that the above really is
what you intend, the workaround is to make the function fully
polymorphic, and then perform a size coercion to the desired size
inside the function body itself:
.. code-block:: futhark
def f (x: bool) =
let n = if x then 10 else 20
in \(y_any: []bool) ->
let y = y_any :> [n]bool
in true
This requires a check at run-time, but it is the only way to
accomplish this in Futhark.
.. _existential-param-ret:
"Existential size would appear in function parameter of return type"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This occurs most commonly when we use function composition with one or
more functions that return an *existential size*. Example:
.. code-block:: futhark
filter (>0) >-> length
The ``filter`` function has this type:
.. code-block:: futhark
val filter [n] 't : (t -> bool) -> [n]t -> ?[m].[m]t
That is, ``filter`` returns an array whose size is not known until the
function actually returns. The ``length`` function has this type:
.. code-block:: futhark
val length [n] 't : [n]t -> i64
Whenever ``length`` occurs (as in the composition above), the type
checker must *instantiate* the ``[n]`` with the concrete symbolic size
of its input array. But in the composition, that size does not
actually exist until ``filter`` has been fully applied. For that
matter, the type checker does not know what ``>->`` does, and for all
it knows it may actually apply ``filter`` many times to different
arrays, yielding different sizes. This makes it impossible to
uniquely instantiate the type of ``length``, and therefore the program
is rejected.
The common workaround is to use *pipelining* instead of composition
whenever we use functions with existential return types:
.. code-block:: futhark
xs |> filter (>0) |> length
This works because ``|>`` is left-associative, and hence the ``xs |>
filter (>0)`` part will be fully evaluated to a concrete array before
``length`` is reached.
We can of course also write it as ``length (filter (>0) xs)``, with no
use of either pipelining or composition.
.. _unused-existential:
"Existential size *n* not used as array size"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This error occurs for type expressions that bind an existential size
for which there is no :term:`constructive use`, such as in the
following examples:
.. code-block:: futhark
?[n].bool
?[n].bool -> [n]bool
When we use existential quantification, we are required to use the
size constructively within its scope, *in particular* it must not be
exclusively as the parameter or return type of a function.
To understand the motivation behind this rule, consider that when we
use an existential quantifier we are saying that there is *some size*.
The size is not known statically, but must be read from some value
(i.e. array) at runtime. In the first example above, the existential
size ``n`` is not used at all, so the actual value cannot be
determined at runtime. In the second example, while an array
``[n]bool`` does exist, it is part of a function type, and at runtime
functions are black boxes and don't "carry" the size of their
parameter or result types.
The workaround is to actually use the existential size. This can be
as simple as adding a *witness array* of type ``[n]()``:
.. code-block:: futhark
?[n].([n](),bool)
?[n].([n](), bool -> [n]bool)
Such an array will take up no space at runtime.
.. _anonymous-nonconstructive:
"Type abbreviation contains an anonymous size not used constructively as an array size."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This error occurs for type abbreviations that use anonymous sizes,
such as the following:
.. code-block:: futhark
type^ t = []bool -> bool
Such an abbreviation is actually shorthand for
.. code-block:: futhark
type^ t = ?[n].[n]bool -> bool
which is erroneous, but with workarounds, as explained in
:ref:`unused-existential`.
.. _unify-consuming-param:
"Parameter types *x* and *y* are incompatible regarding consuming their arguments
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This error occurs when you provide a function that *does* consume its
argument in a context that expects a function that *does not* allow a
function that consumes its argument.
As a simple example, consider the following contrived function that
does consume its argument:
.. code-block:: futhark
def f (xs: *[]f32) : f32 = 0f32
Now we define another function that is merely ``f``, but with a type
annotation that tries to hide the consumption:
.. code-block:: futhark
def g : []f32 -> f32 = f
Allowing this would permit us to hide the fact that ``f`` consumes its
argument, which would not be sound, so the type checker complains.
.. _ambiguous-size:
"Ambiguous size *x*"
~~~~~~~~~~~~~~~~~~~~
There are various sources for this error, but they all have the same
ultimate cause: the type checker cannot figure out how some symbolic
size name should be resolved to a concrete size. The simplest
example, although contrived, is probably this:
.. code-block:: futhark
let [n][m] (xss: [n][m]i64) = []
The type checker can infer that ``n`` should be zero, but how can it
possibly figure out the shape of the (non-existent) rows of the
two-dimensional array? This can be fixed in many ways, but adding a
type ascription to the array is one of them: ``[] : [0][2]i64``.
Another common case arises when using holes. For an expression
``length ???``, how would the type checker figure out the intended
size of the array that the hole represents? Again, this can be solved
with a type ascription: ``length (??? : [10]bool)``.
Finally, ambiguous sizes can also occur for functions that use size
parameters only in "non-witnessing" position, meaning sizes that are
not actually uses as sizes of real arrays. An example:
.. code-block:: futhark
def f [n] (g: [n]i64 -> i64) : i64 = n
def main = f (\xs -> xs[0])
Note that ``f`` is a higher order function, and that the size
parameter ``n`` is only used in the type of the ``g`` function.
Futhark's value model is such that given a value of type ``[n]i64 ->
i64``, we cannot extract an ``n`` from it. Using a function such as
``f`` is only valid when ``n`` can be inferred from the usage, which
is not the case here. Again, we can fix it by adding a type
ascription to disambiguate:
.. code-block:: futhark
def main = f (\(xs:[1]i64) -> xs[0])
Module errors
-------------
.. _module-is-parametric:
"Module *x* is a parametric module
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A parametric module is a module-level function:
.. code-block:: futhark
module PM (P: {val x : i64}) = {
def y = x + 2
}
If we directly try to access the component of ``PM``, as ``PM.y``, we
will get an error. To use ``PM`` we must first apply it to a module
of the expected type:
.. code-block:: futhark
module M = PM { val x = 2 : i64 }
Now we can say ``M.y``. See :ref:`module-system` for more.
Other errors
------------
.. _literal-out-of-bounds:
"Literal out of bounds"
~~~~~~~~~~~~~~~~~~~~~~~
This occurs for overloaded constants such as ``1234`` that are
inferred by context to have a type that is too narrow for their value.
Example:
.. code-block::
257 : u8
It is not an error to have a *non-overloaded* numeric constant whose
value is too large for its type. The following is perfectly
cromulent:
.. code-block::
257u8
In such cases, the behaviour is overflow (so this is equivalent to
``1u8``).
.. _ambiguous-type:
"Type is ambiguous"
~~~~~~~~~~~~~~~~~~~
There are various cases where the type checker is unable to infer the
full type of something. For example:
.. code-block:: futhark
def f r = r.x
We know that ``r`` must be a record with a field called ``x``, but
maybe the record could also have other fields as well. Instead of
assuming a perhaps too narrow type, the type checker signals an error.
The solution is always to add a type annotation in one or more places
to disambiguate the type:
.. code-block:: futhark
def f (r: {x:bool, y:i32}) = r.x
Usually the best spot to add such an annotation is on a function
parameter, as above. But for ambiguous sum types, we often have to
put it on the return type. Consider:
.. code-block:: futhark
def f (x: bool) = #some x
The type of this function is ambiguous, because the type checker must
know what other possible contructors (apart from ``#some``) are
possible. We fix it with a type annotation on the return type:
.. code-block:: futhark
def f (x: bool) : (#some bool | #none) = #just x
See :ref:`typeabbrevs` for how to avoid typing long types in several
places.
.. _may-not-be-redefined:
"The *x* operator may not be redefined"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The ``&&`` and ``||`` operators have magical short-circuiting
behaviour, and therefore may not be redefined. There is no way to
define your own short-circuiting operators.
.. _unmatched-cases:
"Unmatched cases in match expression"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Futhark requires ``match`` expressions to be *exhaustive* - that is,
cover all possible forms of the value being matched. Example:
.. code-block:: futhark
def f (x: i32) =
match x case 0 -> false
case 1 -> true
Usually this is an actual bug, and you fix it by adding the missing
cases. But sometimes you *know* that the missing cases will never
actually occur at run-time. To satisfy the type checker, you can turn
the final case into a wildcard that matches anything:
.. code-block:: futhark
def f (x: i32) =
match x case 0 -> false
case _ -> true
Alternatively, you can add a wildcard case that explicitly asserts
that it should never happen:
.. code-block:: futhark
def f (x: i32) =
match x case 0 -> false
case 1 -> true
case _ -> assert false false
:ref:`See here <assert>` for details on how to use ``assert``.
.. _refutable-pattern:
"Refutable pattern not allowed here"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This occurs when you try to use a :term:`refutable pattern` in a
``let`` binding or function parameter. A refutable pattern is a
pattern that is not guaranteed to match a well-typed value. For
example, this expression tries to bind an arbitrary tuple value ``x``
a pattern that requires the first element is ``2``:
.. code-block:: futhark
let (2, y) = x in 0
What should happen at run-time if ``x`` is not 2? Refutable patterns
are only allowed in ``match`` expressions, where the failure to match
can be handled. For example:
.. code-block:: futhark
match x
case (2, y) -> 0
case _ -> ... -- do something else
.. _record-type-not-known:
"Full type of *x* is not known at this point"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When performing a :ref:`record update <record_update>`, the type of the
field we are updating must be known. This restriction is based on a
limitation in the type type checker, so the notion of "known" is a bit
subtle:
.. code-block:: futhark
def f r : {x:i32} = r with x = 0
Even though the return type annotation disambiguates the type, this
program still fails to type check. This is because the return type is
not consulted until *after* the body of the function has been checked.
The solution is to put a type annotation on the parameter instead:
.. code-block:: futhark
def f (r : {x:i32}) = r with x = 0
Entry points
------------
.. _nested-entry:
"Entry points may not be declared inside modules."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This occurs when the program uses the ``entry`` keyword inside a
module:
.. code-block:: futhark
module m = {
entry f x = x + 1
}
Entry points can only be declared at the top level of a file. When we
wish to make a function from inside a module available as an entry
point, we must define a wrapper function:
.. code-block:: futhark
module m = {
def f x = x + 1
}
entry f = m.f
.. _polymorphic-entry:
"Entry point functions may not be polymorphic."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Entry points are Futhark functions that can be called from other
languages, and are therefore limited how advanced their types can be.
In this case, the problem is that an entry point may not have a
polymorphic type, for example:
.. code-block:: futhark
entry dup 't (x: t) : (t,t) = x
This is an invalid entry point because it uses a type parameter
``'t``. This error occurs frequently when we want to test a
polymorphic function. In such cases, the solution is to define one or
more *monomorphic* entry points, each for a distinct type. For
example, to we can define a variety of monomorphic entry points that
call the built-in function ``scan``:
.. code-block:: futhark
entry scan_i32 (xs: []i32) = scan (+) 0 xs
entry scan_f32 (xs: []i32) = scan (*) 1 xs
.. _higher-order-entry:
"Entry point functions may not be higher-order."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Entry points are Futhark functions that can be called from other
languages, and are therefore limited how advanced their types can be.
In this case, the problem is that an entry point may use functions as
input or output. For example:
.. code-block:: futhark
entry apply (f: i32 -> i32) (x: i32) = f x
There is no simple workaround for such cases. One option is to
manually `defunctionalise
<https://en.wikipedia.org/wiki/Defunctionalization>`_ to use a
non-functional encoding of the functional values, but this can quickly
get very elaborate. Following up on the example above, if we know
that the only functions that would ever be passed are ``(+y)`` or
``(*y)`` for some ``y``, we could do something like the following:
.. code-block:: futhark
type function = #add i32 | #mul i32
entry apply (f: function) (x: i32) =
match f
case #add y -> x + y
case #mul y -> x + y
Although in many cases, the best solution is simply to define a
handful of simpler entry points instead of a single complicated one.
.. _size-polymorphic-entry:
"Entry point functions must not be size-polymorphic in their return type."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This somewhat rare error occurs when an entry point returns an array
that can have an arbitrary size chosen by its caller. Contrived example:
.. code-block:: futhark
-- Entry point taking no parameters.
entry f [n] : [0][n]i32 = []
The size ``n`` is chosen by the caller. Note that the ``n`` might be
inferred and invisible, as in this example:
.. code-block:: futhark
entry g : [0][]i32 = []
When calling functions within a Futhark program, size parameters are
handled by type inference, but entry points are called from the
outside world, which is not subject to type inference. If you really
must have entry points like this, turn the size parameter into an
ordinary parameter:
.. code-block:: futhark
entry f (n: i64) : [0][n]i32 = []
.. _nonconstructive-entry:
"Entry point size parameter [n] only used non-constructively."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This error occurs for programs such as the following::
.. code-block:: futhark
entry main [x] (A: [x+1]i32) = ...
The size parameter ``[x]`` is only used in an size expression ``x+1``,
rather than directly as an array size. This is allowed for ordinary
functions, but not for entry points. The reason is that entry points
are not subject to ordinary type inference, as they are called from
the external world, meaning that the value of the size parameter
``[x]`` will have to be determined from the size of the array ``A``.
This is in principle not a problem for simple sizes like ``x+1``, as
it is obvious that ``x == length A - 1``, but in the general case it
would require computing function inverses that might not exist. For
this reason, entry points require that all size parameters are used
:term:`constructively<constructive use>`.
As a workaround, you can rewrite the entry point as follows:
.. code-block:: futhark
entry main [n] (A: [n]i32) =
let x = n-1
let A = A :> [x+1]i32
...
Or by passing the ``x`` explicitly:
.. code-block:: futhark
entry main (x: i64) (A: [x+1]i32) = ...
|