Unable to check across inductive cases

[michaelbjames]

This function will not check

list_last :: (xs:List Int -> Maybe Int) ^
  (xs:{List Int| len _v == 0} -> {Maybe Int | _v == Nothing}) ^
  (xs:{List Int | _v == ((Cons 2 (Cons 1 Nil)))} -> {Maybe Int | _v == Nothing}) ^

  -- This last refinement causes it to fail
  (xs:{List {Int | _v == 1} | len _v > 0} -> {Maybe Int | _v == Nothing})
  -- It does not fail with a concrete example
  -- (xs:{List Int | _v == Cons 1 Nil} -> {Maybe Int | _v == Just 1})
list_last = \xs .
  match xs with
    Nil -> Nothing
    Cons x3 x4 ->
      match x4 with
        Nil -> Nothing
        Cons x8 x9 -> list_last x4

It seems that while checking the recursive case, the system will not consider the other types in the intersection--It cannot figure out that the IH (_v == Cons 1 Nil) fits the recursive where {List {Int | _v == 1} | len _v > 0}

This bug prevents us from writing "hybrid" specs, ones that include a concrete example, along with an intersection.

[michaelbjames]

It is checking under the case where: list_last :: (xs:{List Int | _v == ((Cons 2 (Cons 1 Nil)))} -> {Maybe Int | _v == Nothing})

It stops checking on the expression list_last x4. So when it reaches this point, it nondeterministically selects one of the other refinements to try to prove this. Let's look at the case that should be used to prove this express, the last refinement. It uses a strengthening judgement and produces the subtyping relation for list_last: {List {Int | _v == 1} | len _v > 0} -> {Maybe Int | _v == Nothing} <: {List Int | _v == 1:[]} -> {Maybe Int | _v == Nothing} This decomposes to: {List Int | _v == 1:[]} <: {List {Int | _v == 1} | len _v > 0}

Tristan believes we cannot prove this currently and it's hard(tm) to show.