Nim: How to prove not nil?

Question

To me, one of the most interesting features of Nim is the not nil annotation, because it basically allows to completely rule out all sorts of NPE / access violations bugs statically, by the help of the compiler. However, I have trouble to use it in practice. Let's consider one of the most basic use cases:

type
  SafeSeq[T] = seq[T] not nil

An immediate pitfall here is that even instantiating such a SafeSeq is not that easy. The attempt

let s: SafeSeq[int] = newSeq[int](100)

fails with error cannot prove 'newSeq(100)' is not nil, which is surprising because one might expect that a newSeq simply is not nil. A workaround seems to use a helper like this:

proc newSafeSeq*[T](size: int): SafeSeq[T] =
  # I guess only @[] expressions are provably not nil
  result = @[]
  result.setlen(size)

The next problem arises when trying to do something with a SafeSeq. For instance, one might expect that when you map over a SafeSeq the result should be not nil again. However, something like this fails as well:

let a: SafeSeq[int] = @[1,2,3]
let b: SafeSeq[string] = a.mapIt(string, $it)

The general problem seems to be that as soon as a return type becomes an ordinary seq the compiler seems to forget about the not nil property and can no longer prove it.

My idea now was to introduce a small (arguably ugly) helper method that allows me to actually prove not nil:

proc proveNotNil*[T](a: seq[T]): SafeSeq[T] =
  if a != nil:
    result = a # surprise, still error "cannot prove 'a' is not nil"
  else:
    raise newException(ValueError, "can't convert")

# which should allow this:
let a: SafeSeq[int] = @[1,2,3]
let b: SafeSeq[string] = a.mapIt(string, $it).proveNotNil

However, the compiler also fails to prove not nil here. My questions are:

• How should I help the compiler inferring not nil in such cases?

• What is the long term goal with this feature, i.e, are there plans to make inferring not nil more powerful? The problem with a manual proveNotNil is that it is potentially unsafe and against the idea that the compiler takes care of proving it. However, if the proveNotNil would only be required in very rare cases, it wouldn't hurt much.

Note: I know that seq attempts to be nil agnostic, i.e., everything works fine even in the nil case. However, this only applies for within Nim. When interfacing C code, the nil-hiding-principle becomes a dangerous source for bugs, because a nil sequence is only harmless on the Nim side...

Stannwood

I would guess the standard library needs some work there, for example annotating that newSeq returns a not nil seq – Heliolatry

Answer 1

Use isNil magic to check for nil:

type SafeSeq[T] = seq[T] not nil
proc proveNotNil[T](s: seq[T]): SafeSeq[T] =
  if s.isNil: # Here is the magic!
    assert(false)
  else:
    result = s
let s = proveNotNil newSeq[int]()

Package

Nice, thanks, that's exactly what I was looking for. I've never heard of isNil before e.g. it is not mentioned in the manual. But it makes sense that inferring "not nil" from a conditional requires compiler magic. – Stannwood

In 2020, .isNil is no longer necessary to activate the nil-tracking “compiler magic”, according to a Nim developer. if s == nil is enough to satisfy the compiler. – Crypt