module T595 where

import Data.Vector

data Test = Test
    { vec  :: Thing
    , x0   :: Bool
    }

type Thing = [()] -- Vector ()

{-@ data Test = Test
      { vec  :: Thing
      , x0   :: { v : Bool | ((len vec) < 1) ==> v }
      }
  @-}

-- The above data declaration should give us the following refined types
-- for the record selectors

{- assume vec :: x:Test -> {v:Thing | v = vec x} @-}
{- assume x0  :: x:Test -> {v:Bool  | v = x0 x  && ((len (vec x) < 1) => v) } @-}

example :: Test -> ()
example t =
    if x0 t
    then ()
    else vec t !! 0