The type T is not searchable

When writing a property using a forall, we are only allowed to use types which are searchable, that is, types for which we can effectively generate sample values. Note this is not the same thing as being finite. For example, the type of natural numbers is searchable even though it is infinite; we can list natural numbers (either in order or randomly) in order to see which ones make the property true or false.

Disco> :test forall x:N. x < 10    -- this works as expected
  - Test is false: ∀x. x < 10
    Counterexample:
      x = 10

On the other hand, the function type N -> N is not searchable: there is no way to list all functions of type N -> N. The below property is in fact false, but Disco can’t handle it:

Disco> :test forall f : N -> N. f(4) > 6
Error: the type
  ℕ → ℕ
is not searchable (i.e. it cannot be used in a forall).