Gradient cannot does not understand `[t, ...]` correctly

[Fl4m3Ph03n1x]

Background

I am trying some code with comprehensions that can either return a list of one element [t, ...] or an empty list [].

parsing_with_option.ex

defmodule ParsingWithOption do
  alias Event

  @type option(t) :: some(t) | nothing
  @type some(t) :: [t, ...]
  @type nothing :: []

  @spec validate_name(String.t()) :: option(String.t())
  def validate_name(name) do
    if String.length(name) > 0 do
      [name]
    else
      []
    end
  end

  @spec validate_end(integer) :: option(integer())
  def validate_end(the_end) do
    if the_end < 3000 do
      [the_end]
    else
      []
    end
  end

  @spec validate_start(integer(), integer()) :: option(integer())
  def validate_start(start, the_end) do
    if start <= the_end do
      [start]
    else
      []
    end
  end

  @spec validate_length(integer(), integer(), integer()) :: option(integer())
  def validate_length(a_start, an_end, min_length) do
    actual_length = an_end - a_start

    if actual_length >= min_length do
      [actual_length]
    else
      []
    end
  end

  @spec parse(String.t(), integer(), integer()) :: option(Event.t())
  def parse(name, a_start, an_end) do
    for valid_name <- validate_name(name),
        valid_end <- validate_end(an_end),
        valid_start <- validate_start(a_start, an_end) do
      %Event{name: valid_name, start: valid_start, end: valid_end}
    end
  end

end

event.ex

defmodule Event do
  @enforce_keys [:name, :start, :end]
  defstruct [:name, :start, :end]

  @type t :: %__MODULE__{
          name: String.t(),
          start: integer(),
          end: integer()
        }
end

While running this code I get the following error:

error

$ mix gradient
Compiling 1 file (.ex)
Typechecking files...
lib/coffee_break_5.34/parsing_with_option.ex: The function call on line 48 is expected to have type option(Event.t()) but it has type list(T)
46   @spec parse(String.t(), integer(), integer()) :: option(Event.t())
47   def parse(name, a_start, an_end) do
48     for valid_name <- validate_name(name),
49         valid_end <- validate_end(an_end),
50         valid_start <- validate_start(a_start, an_end) do

To me it looks quite baffling. It complains that [t] is different from [t, ...]. The first one is a list of type t that can have elements of type t or (inclusive or) be empty. The second case is more specific. I say it can have elements of type t but that it will at least have 1 element and it won't be empty.

Indeed, if I change the spec to @type some(t) :: [t] gradient is happy, but I disagree i need to do this. My case is very straightforward:

• I either have a list of 1 element
• OR (exclusive OR) I have an empty list

Gradient doesn't seem to like this.

[erszcz]

@Fl4m3Ph03n1x thanks for the report :+1:

This needs research on our side, but one thing I have in mind is that we're aware of some regressions which happened when exhaustiveness checking in Gradualizer was extended to cover non-trivial types. There's a WIP fix for them which still needs some polishing. Note to self: check if the bug reported here is still a bug with the fixes from https://github.com/josefs/Gradualizer/pull/359 applied (erszcz/master has that merged in).