Confusion of `fromList` on Chapter 5

[VhRvo]

Hello everyone, I have confusion. And I search this question in this issues, don't help me. I write the following solution for the exercise.

{-@ fromList :: n:Int -> ps:[(Int, a)] -> Maybe (SparseN a n) @-}
fromList          :: Int   -> [(Int, a)] -> Maybe (Sparse a)
fromList dim elts = if dim >= 0 then SP dim <$> traverse f elts else Nothing
  where
    f (i, x)
      | i >= 0 && i < dim = Just (i, x)
      | otherwise = Nothing

But the test case:

{-@ test1 :: SparseN String 3 @-}
test1     = fromJust $ fromList 3 [(0, "cat"), (2, "mouse")]

complains:

Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Maybe.Maybe {v : (Tutorial_05_Datatypes.Sparse [GHC.Types.Char]) | spDim v == (3 : int)}) | v == ?c}
    .
    is not a subtype of the required type
      VV : {VV : (GHC.Maybe.Maybe (Tutorial_05_Datatypes.Sparse [GHC.Types.Char])) | isJust VV}

I notice that I should prove that the argument of fromJust is Just, so I want to encode the information in the refinement type signature, but I don't know how to express it exactly, and the following are failed attempts.

Attempt 1

{-@ predicate ListIn N Xs = filter (between N) Xs == Xs @-}
{-@ fromList :: n:Int -> ps:[(Int, a)] -> {vs:Maybe (SparseN a n)| ListIn n ps => isJust vs } @-}

complains: Unbound symbol Data.Vector.filter

Attempt 2

{-@ fromList :: n:Int -> ps:[(index:Int, a)] -> {vs:Maybe (SparseN a n)| 0 <= index && index < n => isJust vs }@-}

complains: Unbound symbol index

Wish for your help!

[VhRvo]

And I look at liquid haskell course.

{- test :: SparseIN String 3 @-}
test     :: Maybe (Sparse String)
test     = fromList 3 [(0, "cat"), (2, "mouse")]

The type were changed and the fromJust were removed.