diff --git a/inline-r/inline-r.cabal b/inline-r/inline-r.cabal
index 43b05135..f530fec1 100644
--- a/inline-r/inline-r.cabal
+++ b/inline-r/inline-r.cabal
@@ -47,7 +47,7 @@ source-repository head
 library
   exposed-modules:
     Control.Memory.Region
---    Data.Vector.SEXP
+    Data.Vector.SEXP
     Data.Vector.SEXP.Base
     Data.Vector.SEXP.Mutable
     Foreign.R
diff --git a/inline-r/src/Data/Vector/SEXP.hs b/inline-r/src/Data/Vector/SEXP.hs
index 7060ef0e..20b100c9 100644
--- a/inline-r/src/Data/Vector/SEXP.hs
+++ b/inline-r/src/Data/Vector/SEXP.hs
@@ -18,6 +18,7 @@
 -- Note that since 'unstream' relies on slicing operations, it will still be an
 -- O(N) operation but it will copy vector data twice (instead of once).
 
+{-# OPTIONS_GHC -fplugin-opt=LiquidHaskell:--skip-module=False #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
@@ -32,7 +33,10 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 
+{-@ LIQUID "--exact-data-cons" @-}
+{-@ LIQUID "--prune-unsorted" @-}
 module Data.Vector.SEXP
+{-
   ( Vector(..)
   , Mutable.MVector(..)
   , ElemRep
@@ -254,7 +258,7 @@ module Data.Vector.SEXP
   , toString
   , toByteString
   , unsafeWithByteString
-  ) where
+  ) -} where
 
 import Control.Exception (evaluate)
 import Control.Monad.R.Class
@@ -296,12 +300,14 @@ import Control.Monad.Primitive ( PrimMonad, unsafeInlineIO, unsafePrimToPrim )
 import qualified Control.DeepSeq as DeepSeq
 import Data.Word ( Word8 )
 import Foreign ( Storable, Ptr, castPtr, peekElemOff )
+import Foreign.C.String -- XXX: Needed for LH name resolution
 import Foreign.ForeignPtr (ForeignPtr, withForeignPtr)
 import Foreign.Marshal.Array ( copyArray )
 import qualified GHC.Foreign as GHC
 import qualified GHC.ForeignPtr as GHC
 import GHC.IO.Encoding.UTF8
 import qualified GHC.Exts as Exts
+import Internal.Error (violation)
 import System.IO.Unsafe
 
 import Prelude
@@ -324,56 +330,58 @@ import Prelude
   )
 import qualified Prelude
 
-newtype ForeignSEXP (ty::SEXPTYPE) = ForeignSEXP (ForeignPtr R.SEXPREC)
+newtype ForeignSEXP = ForeignSEXP (ForeignPtr R.SEXPREC)
+
+{-@ measure Data.Vector.SEXP.ftypeOf :: ForeignSEXP -> R.SEXPTYPE @-}
 
 -- | Create a 'ForeignSEXP' from 'SEXP'.
-foreignSEXP :: PrimMonad m => SEXP s ty -> m (ForeignSEXP ty)
+{-@ assume foreignSEXP :: s:SEXP s -> m {v:ForeignSEXP | Data.Vector.SEXP.ftypeOf v == typeOf s} @-}
+foreignSEXP :: PrimMonad m => SEXP s -> m ForeignSEXP
 foreignSEXP sx@(SEXP (SEXP0 ptr)) =
     unsafePrimToPrim $ mask_ $ do
       R.preserveObject sx
       ForeignSEXP <$> GHC.newConcForeignPtr ptr (R.releaseObject sx)
 
-withForeignSEXP
-  :: ForeignSEXP ty
-  -> (SEXP V ty -> IO r)
-  -> IO r
+{-@ assume withForeignSEXP :: f:ForeignSEXP -> (TSEXP V (Data.Vector.SEXP.ftypeOf f) -> IO r) -> IO r @-}
+withForeignSEXP :: ForeignSEXP -> (SEXP V -> IO r) -> IO r
 withForeignSEXP (ForeignSEXP fptr) f =
     withForeignPtr fptr $ \ptr -> f (SEXP (SEXP0 ptr))
 
--- | Immutable vectors. The second type paramater is a phantom parameter
--- reflecting at the type level the tag of the vector when viewed as a 'SEXP'.
--- The tag of the vector and the representation type are related via 'ElemRep'.
-data Vector (ty :: SEXPTYPE) a = Vector
-  { vectorBase   :: {-# UNPACK #-} !(ForeignSEXP ty)
+{-@ measure Data.Vector.SEXP.vtypeOf :: Vector a -> R.SEXPTYPE @-}
+{-@ type TVector a T = {v:Vector a | Data.Vector.SEXP.vtypeOf v == T} @-}
+
+-- | Immutable vectors.
+data Vector a = Vector
+  { vectorBase   :: {-# UNPACK #-} !ForeignSEXP
   , vectorOffset :: {-# UNPACK #-} !Int32
   , vectorLength :: {-# UNPACK #-} !Int32
   }
 
-instance (Eq a, SVECTOR ty a) => Eq (Vector ty a) where
+instance (Eq a, Storable a) => Eq (Vector a) where
   a == b = toList a == toList b
 
-instance (Show a, SVECTOR ty a)  => Show (Vector ty a) where
+instance (Show a, Storable a)  => Show (Vector a) where
   show v = "fromList " Prelude.++ showList (toList v) ""
 
 -- | Internal wrapper type for reflection. First type parameter is the reified
 -- type to reflect.
-newtype W t ty a = W { unW :: Vector ty a }
+newtype W t a = W { unW :: Vector a }
 
-withW :: proxy t -> Vector ty a -> W t ty a
+withW :: proxy t -> Vector a -> W t a
 withW _ v = W v
 
-proxyFW :: (W t ty a -> r) -> Vector ty a -> p t -> r
+proxyFW :: (W t a -> r) -> Vector a -> p t -> r
 proxyFW f v p = f (withW p v)
 
-proxyFW2 :: (W t tya a -> W t tyb b -> r) -> Vector tya a -> Vector tyb b -> p t -> r
+proxyFW2 :: (W t a -> W t b -> r) -> Vector a -> Vector b -> p t -> r
 proxyFW2 f v1 v2 p = f (withW p v1) (withW p v2)
 
-proxyW :: W t ty a -> p t -> Vector ty a
+proxyW :: W t a -> p t -> Vector a
 proxyW v _ = unW v
 
-type instance G.Mutable (W t ty) = Mutable.W t ty
+type instance G.Mutable (W t) = Mutable.W t
 
-instance (Reifies t (AcquireIO s), SVECTOR ty a) => G.Vector (W t ty) a where
+instance (Reifies t (AcquireIO s, IO R.SEXPTYPE), Storable a) => G.Vector (W t) a where
   {-# INLINE basicUnsafeFreeze #-}
   basicUnsafeFreeze (Mutable.unW -> Mutable.MVector sx off len) = do
       fp <- foreignSEXP sx
@@ -384,7 +392,7 @@ instance (Reifies t (AcquireIO s), SVECTOR ty a) => G.Vector (W t ty) a where
          sx' <- acquireIO (R.release ptr)
          return $ Mutable.withW p $ Mutable.MVector (R.unsafeRelease sx') off len
     where
-      AcquireIO acquireIO = reflect (Proxy :: Proxy t)
+      (acquireIO, _) = reflect (Proxy :: Proxy t)
       p = Proxy :: Proxy t
   basicLength (unW -> Vector _ _ len) = fromIntegral len
   {-# INLINE basicUnsafeSlice #-}
@@ -401,21 +409,27 @@ instance (Reifies t (AcquireIO s), SVECTOR ty a) => G.Vector (W t ty) a where
   {-# INLINE elemseq #-}
   elemseq _ = seq
 
-instance SVECTOR ty a => Exts.IsList (Vector ty a) where
-  type Item (Vector ty a) = a
-  fromList = fromList
-  fromListN = fromListN
-  toList = toList
+-- TODO: how to disable LH on a class instance?
+-- instance Storable a => Exts.IsList (Vector a) where
+--   type Item (Vector a) = a
+  -- TODO: How to disable LH so it doesn't complain of these methods calling error
+  -- fromList = Prelude.error "cannot convert list to vector without an explicit runtime type"
+  -- fromListN = Prelude.error "cannot convert list to vector without an explicit runtime type"
+  -- fromList = fromList
+  -- fromListN = fromListN
+--  toList = toList
 
 -- | Return Pointer of the first element of the vector storage.
-unsafeToPtr :: Storable a => Vector ty a -> Ptr a
+unsafeToPtr :: Storable a => Vector a -> Ptr a
 {-# INLINE unsafeToPtr #-}
 unsafeToPtr (Vector fp off len) = unsafeInlineIO $ withForeignSEXP fp $ \sx ->
     return $ Mutable.unsafeToPtr $ Mutable.MVector sx off len
 
 -- | /O(n)/ Create an immutable vector from a 'SEXP'. Because 'SEXP's are
 -- mutable, this function yields an immutable /copy/ of the 'SEXP'.
-fromSEXP :: (SVECTOR ty a) => SEXP s ty -> Vector ty a
+{-@ assume fromSEXP :: {s:SEXP s | isVectorType (typeOf s)} -> {v:Vector a | Data.Vector.SEXP.vtypeOf v == typeOf s} @-}
+{-@ ignore fromSEXP @-}
+fromSEXP :: Storable a => SEXP s -> Vector a
 fromSEXP s = phony $ \p -> runST $ do
   w <- run (proxyFW G.clone (unsafeFromSEXP s) p)
   v <- G.unsafeFreeze w
@@ -424,16 +438,19 @@ fromSEXP s = phony $ \p -> runST $ do
 -- | /O(1)/ Unsafe convert a mutable 'SEXP' to an immutable vector without
 -- copying. The mutable vector must not be used after this operation, lest one
 -- runs the risk of breaking referential transparency.
-unsafeFromSEXP :: SVECTOR ty a
-               => SEXP s ty
-               -> Vector ty a
+{-@ assume unsafeFromSEXP :: {s:SEXP s | isVectorType (typeOf s)} -> {v:Vector a | Data.Vector.SEXP.vtypeOf v == typeOf s} @-}
+unsafeFromSEXP :: Storable a
+               => SEXP s
+               -> Vector a
 unsafeFromSEXP s = unsafeInlineIO $ do
   sxp <- foreignSEXP s
   l <- R.length s
   return $ Vector sxp 0 (fromIntegral l)
 
 -- | /O(n)/ Yield a (mutable) copy of the vector as a 'SEXP'.
-toSEXP :: SVECTOR ty a => Vector ty a -> SEXP s ty
+
+{-@ assume toSEXP :: v:Vector a -> {s:SEXP s | typeOf s == Data.Vector.SEXP.vtypeOf v} @-}
+toSEXP :: Storable a => Vector a -> SEXP s
 toSEXP s = phony $ \p -> runST $ do
   w <- run (proxyFW G.clone s p)
   v <- G.unsafeFreeze w
@@ -441,18 +458,23 @@ toSEXP s = phony $ \p -> runST $ do
 
 -- | /O(1)/ Unsafely convert an immutable vector to a (mutable) 'SEXP' without
 -- copying. The immutable vector must not be used after this operation.
-unsafeToSEXP :: SVECTOR ty a => Vector ty a -> SEXP s ty
+{-@ assume unsafeToSEXP :: v:Vector a -> {s:SEXP s | typeOf s == Data.Vector.SEXP.vtypeOf v} @-}
+unsafeToSEXP :: Storable a => Vector a -> SEXP s
 unsafeToSEXP (Vector (ForeignSEXP fsx) _ _) = unsafePerformIO $ -- XXX
   withForeignPtr fsx $ return . R.sexp . SEXP0
 
 -- | /O(n)/ Convert a character vector into a 'String'.
-toString :: Vector 'Char Word8 -> String
+{-@ assume toString :: TVector Word8 Char -> String @-}
+{-@ ignore toString @-}
+toString :: Vector Word8 -> String
 toString v = unsafeInlineIO $
   GHC.peekCStringLen utf8 ( castPtr $ unsafeToPtr v
                           , fromIntegral $ vectorLength v)
 
 -- | /O(n)/ Convert a character vector into a strict 'ByteString'.
-toByteString :: Vector 'Char Word8 -> ByteString
+{-@ assume toByteString :: TVector Word8 Char -> ByteString @-}
+{-@ ignore toByteString @-}
+toByteString :: Vector Word8 -> ByteString
 toByteString v = unsafeInlineIO $
    B.packCStringLen ( castPtr $ unsafeToPtr v
                     , fromIntegral $ vectorLength v)
@@ -461,12 +483,14 @@ toByteString v = unsafeInlineIO $
 -- outside of the function. Any change to bytestring will be
 -- reflected in the source vector, thus breaking referencial
 -- transparancy.
-unsafeWithByteString :: DeepSeq.NFData a => Vector 'Char Word8 -> (ByteString -> IO a) -> a
+{-@ assume unsafeWithByteString :: TVector Word8 Char -> (ByteString -> IO a) -> a @-}
+{-@ ignore unsafeWithByteString @-}
+unsafeWithByteString :: DeepSeq.NFData a => Vector Word8 -> (ByteString -> IO a) -> a
 unsafeWithByteString v f = unsafeInlineIO $ do
    x <- B.unsafePackCStringLen (castPtr $ unsafeToPtr v
                                ,fromIntegral $ vectorLength v)
    w <- DeepSeq.force <$> f x
-   evaluate w 
+   evaluate w
 
 ------------------------------------------------------------------------
 -- Vector API
@@ -477,12 +501,12 @@ unsafeWithByteString v f = unsafeInlineIO $ do
 ------------------------------------------------------------------------
 
 -- | /O(1)/ Yield the length of the vector.
-length :: SVECTOR ty a => Vector ty a -> Int
+length :: Storable a => Vector a -> Int
 {-# INLINE length #-}
 length v = phony $ proxyFW G.length v
 
 -- | /O(1)/ Test whether a vector if empty
-null :: SVECTOR ty a => Vector ty a -> Bool
+null :: Storable a => Vector a -> Bool
 {-# INLINE null #-}
 null v = phony $ proxyFW G.null v
 
@@ -491,37 +515,37 @@ null v = phony $ proxyFW G.null v
 ------------------------------------------------------------------------
 
 -- | O(1) Indexing
-(!) :: SVECTOR ty a => Vector ty a -> Int -> a
+(!) :: Storable a => Vector a -> Int -> a
 {-# INLINE (!) #-}
 (!) v i = phony $ proxyFW (G.! i) v
 
 -- | O(1) Safe indexing
-(!?) :: SVECTOR ty a => Vector ty a -> Int -> Maybe a
+(!?) :: Storable a => Vector a -> Int -> Maybe a
 {-# INLINE (!?) #-}
 (!?) v i = phony $ proxyFW (G.!? i) v
 
 -- | /O(1)/ First element
-head :: SVECTOR ty a => Vector ty a -> a
+head :: Storable a => Vector a -> a
 {-# INLINE head #-}
 head v = phony $ proxyFW G.head v
 
 -- | /O(1)/ Last element
-last :: SVECTOR ty a => Vector ty a -> a
+last :: Storable a => Vector a -> a
 {-# INLINE last #-}
 last v = phony $ proxyFW G.last v
 
 -- | /O(1)/ Unsafe indexing without bounds checking
-unsafeIndex :: SVECTOR ty a => Vector ty a -> Int -> a
+unsafeIndex :: Storable a => Vector a -> Int -> a
 {-# INLINE unsafeIndex #-}
 unsafeIndex v i = phony $ proxyFW (`G.unsafeIndex` i) v
 
 -- | /O(1)/ First element without checking if the vector is empty
-unsafeHead :: SVECTOR ty a => Vector ty a -> a
+unsafeHead :: Storable a => Vector a -> a
 {-# INLINE unsafeHead #-}
 unsafeHead v = phony $ proxyFW G.unsafeHead v
 
 -- | /O(1)/ Last element without checking if the vector is empty
-unsafeLast :: SVECTOR ty a => Vector ty a -> a
+unsafeLast :: Storable a => Vector a -> a
 {-# INLINE unsafeLast #-}
 unsafeLast v = phony $ proxyFW G.unsafeLast v
 
@@ -548,37 +572,37 @@ unsafeLast v = phony $ proxyFW G.unsafeLast v
 -- Here, no references to @v@ are retained because indexing (but /not/ the
 -- elements) is evaluated eagerly.
 --
-indexM :: (SVECTOR ty a, Monad m) => Vector ty a -> Int -> m a
+indexM :: (Storable a, Monad m) => Vector a -> Int -> m a
 {-# INLINE indexM #-}
 indexM v i = phony $ proxyFW (`G.indexM` i) v
 
 -- | /O(1)/ First element of a vector in a monad. See 'indexM' for an
 -- explanation of why this is useful.
-headM :: (SVECTOR ty a, Monad m) => Vector ty a -> m a
+headM :: (Storable a, Monad m) => Vector a -> m a
 {-# INLINE headM #-}
 headM v = phony $ proxyFW G.headM v
 
 -- | /O(1)/ Last element of a vector in a monad. See 'indexM' for an
 -- explanation of why this is useful.
-lastM :: (SVECTOR ty a, Monad m) => Vector ty a -> m a
+lastM :: (Storable a, Monad m) => Vector a -> m a
 {-# INLINE lastM #-}
 lastM v = phony $ proxyFW G.lastM v
 
 -- | /O(1)/ Indexing in a monad without bounds checks. See 'indexM' for an
 -- explanation of why this is useful.
-unsafeIndexM :: (SVECTOR ty a, Monad m) => Vector ty a -> Int -> m a
+unsafeIndexM :: (Storable a, Monad m) => Vector a -> Int -> m a
 {-# INLINE unsafeIndexM #-}
 unsafeIndexM v = phony $ proxyFW G.unsafeIndexM v
 
 -- | /O(1)/ First element in a monad without checking for empty vectors.
 -- See 'indexM' for an explanation of why this is useful.
-unsafeHeadM :: (SVECTOR ty a, Monad m) => Vector ty a -> m a
+unsafeHeadM :: (Storable a, Monad m) => Vector a -> m a
 {-# INLINE unsafeHeadM #-}
 unsafeHeadM v = phony $ proxyFW G.unsafeHeadM v
 
 -- | /O(1)/ Last element in a monad without checking for empty vectors.
 -- See 'indexM' for an explanation of why this is useful.
-unsafeLastM :: (SVECTOR ty a, Monad m) => Vector ty a -> m a
+unsafeLastM :: (Storable a, Monad m) => Vector a -> m a
 {-# INLINE unsafeLastM #-}
 unsafeLastM v = phony $ proxyFW G.unsafeLastM v
 
@@ -588,34 +612,39 @@ unsafeLastM v = phony $ proxyFW G.unsafeLastM v
 
 -- | /O(N)/ Yield a slice of the vector with copying it. The vector must
 -- contain at least @i+n@ elements.
-slice :: SVECTOR ty a
+{-@ assume slice :: Int -> Int -> v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+slice :: Storable a
       => Int   -- ^ @i@ starting index
       -> Int   -- ^ @n@ length
-      -> Vector ty a
-      -> Vector ty a
+      -> Vector a
+      -> Vector a
 {-# INLINE slice #-}
 slice i n v = phony $ unW . proxyFW (G.slice i n) v
 
 -- | /O(N)/ Yield all but the last element, this operation will copy an array.
 -- The vector may not be empty.
-init :: SVECTOR ty a => Vector ty a -> Vector ty a
+{-@ assume init :: v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+init :: Storable a => Vector a -> Vector a
 {-# INLINE init #-}
 init v = phony $ unW . proxyFW G.init v
 
 -- | /O(N)/ Copy all but the first element. The vector may not be empty.
-tail :: SVECTOR ty a => Vector ty a -> Vector ty a
+{-@ assume tail :: v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+tail :: Storable a => Vector a -> Vector a
 {-# INLINE tail #-}
 tail v = phony $ unW . proxyFW G.tail v
 
 -- | /O(N)/ Yield at the first @n@ elements with copying. The vector may
 -- contain less than @n@ elements in which case it is returned unchanged.
-take :: SVECTOR ty a => Int -> Vector ty a -> Vector ty a
+{-@ assume take :: Int -> v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+take :: Storable a => Int -> Vector a -> Vector a
 {-# INLINE take #-}
 take i v = phony $ unW . proxyFW (G.take i) v
 
 -- | /O(N)/ Yield all but the first @n@ elements with copying. The vector may
 -- contain less than @n@ elements in which case an empty vector is returned.
-drop :: SVECTOR ty a => Int -> Vector ty a -> Vector ty a
+{-@ assume drop :: Int -> v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+drop :: Storable a => Int -> Vector a -> Vector a
 {-# INLINE drop #-}
 drop i v = phony $ unW . proxyFW (G.drop i) v
 
@@ -623,40 +652,46 @@ drop i v = phony $ unW . proxyFW (G.drop i) v
 --
 -- Note that @'splitAt' n v@ is equivalent to @('take' n v, 'drop' n v)@
 -- but slightly more efficient.
+{-@ assume splitAt :: Int -> v:Vector a -> (TVector a (Data.Vector.SEXP.vtypeOf v), TVector a (Data.Vector.SEXP.vtypeOf v)) @-}
 {-# INLINE splitAt #-}
-splitAt :: SVECTOR ty a => Int -> Vector ty a -> (Vector ty a, Vector ty a)
+splitAt :: Storable a => Int -> Vector a -> (Vector a, Vector a)
 splitAt i v = phony $ (\(a,b) -> (unW a, unW b)) . proxyFW (G.splitAt i) v
 
 -- | /O(N)/ Yield a slice of the vector with copying. The vector must
 -- contain at least @i+n@ elements but this is not checked.
-unsafeSlice :: SVECTOR ty a => Int   -- ^ @i@ starting index
+{-@ assume unsafeSlice :: Int -> Int -> v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+unsafeSlice :: Storable a => Int   -- ^ @i@ starting index
                        -> Int   -- ^ @n@ length
-                       -> Vector ty a
-                       -> Vector ty a
+                       -> Vector a
+                       -> Vector a
 {-# INLINE unsafeSlice #-}
 unsafeSlice i j v = phony $ unW . proxyFW (G.unsafeSlice i j) v
 
 -- | /O(N)/ Yield all but the last element with copying. The vector may not
 -- be empty but this is not checked.
-unsafeInit :: SVECTOR ty a => Vector ty a -> Vector ty a
+{-@ assume unsafeInit :: v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+unsafeInit :: Storable a => Vector a -> Vector a
 {-# INLINE unsafeInit #-}
 unsafeInit v = phony $ unW . proxyFW G.unsafeInit v
 
 -- | /O(N)/ Yield all but the first element with copying. The vector may not
 -- be empty but this is not checked.
-unsafeTail :: SVECTOR ty a => Vector ty a -> Vector ty a
+{-@ assume unsafeTail :: v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+unsafeTail :: Storable a => Vector a -> Vector a
 {-# INLINE unsafeTail #-}
 unsafeTail v = phony $ unW . proxyFW G.unsafeTail v
 
 -- | /O(N)/ Yield the first @n@ elements with copying. The vector must
 -- contain at least @n@ elements but this is not checked.
-unsafeTake :: SVECTOR ty a => Int -> Vector ty a -> Vector ty a
+{-@ assume unsafeTake :: Int -> v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+unsafeTake :: Storable a => Int -> Vector a -> Vector a
 {-# INLINE unsafeTake #-}
 unsafeTake i v = phony $ unW . proxyFW (G.unsafeTake i) v
 
 -- | /O(N)/ Yield all but the first @n@ elements with copying. The vector
 -- must contain at least @n@ elements but this is not checked.
-unsafeDrop :: SVECTOR ty a => Int -> Vector ty a -> Vector ty a
+{-@ assume unsafeDrop :: Int -> v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf v) @-}
+unsafeDrop :: Storable a => Int -> Vector a -> Vector a
 {-# INLINE unsafeDrop #-}
 unsafeDrop i v = phony $ unW . proxyFW (G.unsafeDrop i) v
 
@@ -664,30 +699,35 @@ unsafeDrop i v = phony $ unW . proxyFW (G.unsafeDrop i) v
 -- --------------
 
 -- | /O(1)/ Empty vector
-empty :: SVECTOR ty a => Vector ty a
+{-@ empty :: x:VSEXPTYPE s a -> TVector a (vstypeOf x) @-}
+empty :: Storable a => VSEXPTYPE s a -> Vector a
 {-# INLINE empty #-}
-empty = phony $ proxyW G.empty
+empty _t = phony $ proxyW G.empty
 
 -- | /O(1)/ Vector with exactly one element
-singleton :: SVECTOR ty a => a -> Vector ty a
+{-@ assume singleton :: x:VSEXPTYPE s a -> a -> TVector a (vstypeOf x) @-}
+singleton :: Storable a => VSEXPTYPE s a -> a -> Vector a
 {-# INLINE singleton #-}
-singleton a = phony $ proxyW (G.singleton a)
+singleton _t a = phony $ proxyW (G.singleton a)
 
 -- | /O(n)/ Vector of the given length with the same value in each position
-replicate :: SVECTOR ty a => Int -> a -> Vector ty a
+{-@ assume replicate :: x:VSEXPTYPE s a -> Int -> a -> TVector a (vstypeOf x) @-}
+replicate :: Storable a => VSEXPTYPE s a -> Int -> a -> Vector a
 {-# INLINE replicate #-}
-replicate i v = phony $ proxyW (G.replicate i v)
+replicate _t i v = phony $ proxyW (G.replicate i v)
 
 -- | /O(n)/ Construct a vector of the given length by applying the function to
 -- each index
-generate :: SVECTOR ty a => Int -> (Int -> a) -> Vector ty a
+{-@ generate :: x:VSEXPTYPE s a -> Int -> (Int -> a) -> TVector a (vstypeOf x) @-}
+generate :: Storable a => VSEXPTYPE s a -> Int -> (Int -> a) -> Vector a
 {-# INLINE generate #-}
-generate i f = phony $ proxyW (G.generate i f)
+generate _t i f = phony $ proxyW (G.generate i f)
 
 -- | /O(n)/ Apply function n times to value. Zeroth element is original value.
-iterateN :: SVECTOR ty a => Int -> (a -> a) -> a -> Vector ty a
+{-@ assume iterateN :: x:VSEXPTYPE s a -> Int -> (a -> a) -> a -> TVector a (vstypeOf x) @-}
+iterateN :: Storable a => VSEXPTYPE s a -> Int -> (a -> a) -> a -> Vector a
 {-# INLINE iterateN #-}
-iterateN i f a = phony $ proxyW (G.iterateN i f a)
+iterateN _t i f a = phony $ proxyW (G.iterateN i f a)
 
 -- Unfolding
 -- ---------
@@ -697,27 +737,30 @@ iterateN i f a = phony $ proxyW (G.iterateN i f a)
 --
 -- > unfoldr (\n -> if n == 0 then Nothing else Just (n,n-1)) 10
 -- >  = <10,9,8,7,6,5,4,3,2,1>
-unfoldr :: SVECTOR ty a => (b -> Maybe (a, b)) -> b -> Vector ty a
+{-@ assume unfoldr :: x:VSEXPTYPE s a -> (b -> Maybe (a, b)) -> b -> TVector a (vstypeOf x) @-}
+unfoldr :: Storable a => VSEXPTYPE s a -> (b -> Maybe (a, b)) -> b -> Vector a
 {-# INLINE unfoldr #-}
-unfoldr g a = phony $ proxyW (G.unfoldr g a)
+unfoldr _t g a = phony $ proxyW (G.unfoldr g a)
 
 -- | /O(n)/ Construct a vector with at most @n@ by repeatedly applying the
 -- generator function to the a seed. The generator function yields 'Just' the
 -- next element and the new seed or 'Nothing' if there are no more elements.
 --
 -- > unfoldrN 3 (\n -> Just (n,n-1)) 10 = <10,9,8>
-unfoldrN :: SVECTOR ty a => Int -> (b -> Maybe (a, b)) -> b -> Vector ty a
+{-@ assume unfoldrN :: x:VSEXPTYPE s a -> Int -> (b -> Maybe (a, b)) -> b -> TVector a (vstypeOf x) @-}
+unfoldrN :: Storable a => VSEXPTYPE s a -> Int -> (b -> Maybe (a, b)) -> b -> Vector a
 {-# INLINE unfoldrN #-}
-unfoldrN n g a = phony $ proxyW (G.unfoldrN n g a)
+unfoldrN _t n g a = phony $ proxyW (G.unfoldrN n g a)
 
 -- | /O(n)/ Construct a vector with @n@ elements by repeatedly applying the
 -- generator function to the already constructed part of the vector.
 --
 -- > constructN 3 f = let a = f <> ; b = f <a> ; c = f <a,b> in f <a,b,c>
 --
-constructN :: SVECTOR ty a => Int -> (Vector ty a -> a) -> Vector ty a
+{-@ assume constructN :: x:VSEXPTYPE s a -> Int -> (TVector a (vstypeOf x) -> a) -> Vector a (vstypeOf x) @-}
+constructN :: Storable a => VSEXPTYPE s a -> Int -> (Vector a -> a) -> Vector a
 {-# INLINE constructN #-}
-constructN n g = phony $ proxyW (G.constructN n (g.unW))
+constructN _t n g = phony $ proxyW (G.constructN n (g.unW))
 
 -- | /O(n)/ Construct a vector with @n@ elements from right to left by
 -- repeatedly applying the generator function to the already constructed part
@@ -725,9 +768,10 @@ constructN n g = phony $ proxyW (G.constructN n (g.unW))
 --
 -- > constructrN 3 f = let a = f <> ; b = f<a> ; c = f <b,a> in f <c,b,a>
 --
-constructrN :: SVECTOR ty a => Int -> (Vector ty a -> a) -> Vector ty a
+{-@ assume constructrN :: x:VSEXPTYPE s a -> Int -> (TVector a (vstypeOf x) -> a) -> Vector a (vstypeOf x) @-}
+constructrN :: Storable a => VSEXPTYPE s a -> Int -> (Vector a -> a) -> Vector a
 {-# INLINE constructrN #-}
-constructrN n g = phony $ proxyW (G.constructrN n (g.unW))
+constructrN _t n g = phony $ proxyW (G.constructrN n (g.unW))
 
 -- Enumeration
 -- -----------
@@ -736,83 +780,95 @@ constructrN n g = phony $ proxyW (G.constructrN n (g.unW))
 -- etc. This operation is usually more efficient than 'enumFromTo'.
 --
 -- > enumFromN 5 3 = <5,6,7>
-enumFromN :: (SVECTOR ty a, Num a) => a -> Int -> Vector ty a
+{-@ enumFromN :: x:VSEXPTYPE s a -> a -> Int -> TVector a (vstypeOf x) @-}
+enumFromN :: (Storable a, Num a) => VSEXPTYPE s a -> a -> Int -> Vector a
 {-# INLINE enumFromN #-}
-enumFromN a i = phony $ proxyW (G.enumFromN a i)
+enumFromN _t a i = phony $ proxyW (G.enumFromN a i)
 
 -- | /O(n)/ Yield a vector of the given length containing the values @x@, @x+y@,
 -- @x+y+y@ etc. This operations is usually more efficient than 'enumFromThenTo'.
 --
 -- > enumFromStepN 1 0.1 5 = <1,1.1,1.2,1.3,1.4>
-enumFromStepN :: (SVECTOR ty a, Num a) => a -> a -> Int -> Vector ty a
+{-@ enumFromStepN :: x:VSEXPTYPE a -> a -> Int -> TVector a (vstypeOf x) @-}
+enumFromStepN :: (Storable a, Num a) => VSEXPTYPE s a -> a -> a -> Int -> Vector a
 {-# INLINE enumFromStepN #-}
-enumFromStepN f t s = phony $ proxyW (G.enumFromStepN f t s)
+enumFromStepN _t f t s = phony $ proxyW (G.enumFromStepN f t s)
 
 -- | /O(n)/ Enumerate values from @x@ to @y@.
 --
 -- /WARNING:/ This operation can be very inefficient. If at all possible, use
 -- 'enumFromN' instead.
-enumFromTo :: (SVECTOR ty a, Enum a) => a -> a -> Vector ty a
+{-@ enumFromTo :: x:VSEXPTYPE s a -> a -> a -> Vector a (vstypeOf x) @-}
+enumFromTo :: (Storable a, Enum a) => VSEXPTYPE s a -> a -> a -> Vector a
 {-# INLINE enumFromTo #-}
-enumFromTo f t = phony $ proxyW (G.enumFromTo f t)
+enumFromTo _t f t = phony $ proxyW (G.enumFromTo f t)
 
 -- | /O(n)/ Enumerate values from @x@ to @y@ with a specific step @z@.
 --
 -- /WARNING:/ This operation can be very inefficient. If at all possible, use
 -- 'enumFromStepN' instead.
-enumFromThenTo :: (SVECTOR ty a, Enum a) => a -> a -> a -> Vector ty a
+{-@ enumFromThenTo :: x:VSEXPTYPE s a -> a -> a -> a -> TVector a (vstypeOf x) @-}
+enumFromThenTo :: (Storable a, Enum a) => VSEXPTYPE s a -> a -> a -> a -> Vector a
 {-# INLINE enumFromThenTo #-}
-enumFromThenTo f t s = phony $ proxyW (G.enumFromThenTo f t s)
+enumFromThenTo _t f t s = phony $ proxyW (G.enumFromThenTo f t s)
 
 -- Concatenation
 -- -------------
 
 -- | /O(n)/ Prepend an element
-cons :: SVECTOR ty a => a -> Vector ty a -> Vector ty a
+{-@ cons :: a -> v:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf x) @-}
+cons :: Storable a => a -> Vector a -> Vector a
 {-# INLINE cons #-}
 cons a v = phony $ unW . proxyFW (G.cons a) v
 
 -- | /O(n)/ Append an element
-snoc :: SVECTOR ty a => Vector ty a -> a -> Vector ty a
+{-@ snoc :: v:Vector a -> a -> TVector a (Data.Vector.SEXP.vtypeOf x) @-}
+snoc :: Storable a => Vector a -> a -> Vector a
 {-# INLINE snoc #-}
 snoc v a = phony $ unW . proxyFW (`G.snoc` a) v
 
 infixr 5 ++
 -- | /O(m+n)/ Concatenate two vectors
-(++) :: SVECTOR ty a => Vector ty a -> Vector ty a -> Vector ty a
+{-@ assume (++) :: x:Vector a -> TVector a (Data.Vector.SEXP.vtypeOf x) -> TVector a (Data.Vector.SEXP.vtypeOf x) @-}
+(++) :: Storable a => Vector a -> Vector a -> Vector a
 {-# INLINE (++) #-}
 v1 ++ v2 = phony $ unW . proxyFW2 (G.++) v1 v2
 
 -- | /O(n)/ Concatenate all vectors in the list
-concat :: SVECTOR ty a => [Vector ty a] -> Vector ty a
+{-@ concat :: x:VSEXPTYPE s a -> [TVector a (vstypeOf x)] -> TVector a (vstypeOf x) @-}
+concat :: Storable a => VSEXPTYPE s a -> [Vector a] -> Vector a
 {-# INLINE concat #-}
-concat vs = phony $ \p -> unW $ G.concat $ Prelude.map (withW p) vs
+concat _t vs = phony $ \p -> unW $ G.concat $ Prelude.map (withW p) vs
 
 -- Monadic initialisation
 -- ----------------------
 
 -- | /O(n)/ Execute the monadic action the given number of times and store the
 -- results in a vector.
-replicateM :: (Monad m, SVECTOR ty a) => Int -> m a -> m (Vector ty a)
+{-@ replicateM :: x:VSEXPTYPE s a -> Int -> m a -> m (TVector a (vstypeOf x)) @-}
+replicateM :: (Monad m, Storable a) => VSEXPTYPE s a -> Int -> m a -> m (Vector a)
 {-# INLINE replicateM #-}
-replicateM n f = phony $ \p -> (\v -> proxyW v p) <$> G.replicateM n f
+replicateM _t n f = phony $ \p -> (\v -> proxyW v p) <$> G.replicateM n f
 
 -- | /O(n)/ Construct a vector of the given length by applying the monadic
 -- action to each index
-generateM :: (Monad m, SVECTOR ty a) => Int -> (Int -> m a) -> m (Vector ty a)
+{-@ generateM :: x:VSEXPTYPE s a -> Int -> (Int -> m a) -> m (TVector a (vstypeOf x)) @-}
+generateM :: (Monad m, Storable a) => VSEXPTYPE s a -> Int -> (Int -> m a) -> m (Vector a)
 {-# INLINE generateM #-}
-generateM n f = phony $ \p -> (\v -> proxyW v p) <$> G.generateM n f
+generateM _t n f = phony $ \p -> (\v -> proxyW v p) <$> G.generateM n f
 
 -- | Execute the monadic action and freeze the resulting vector.
 --
 -- @
 -- create (do { v \<- new 2; write v 0 \'a\'; write v 1 \'b\'; return v }) = \<'a','b'\>
 -- @
-create :: SVECTOR ty a => (forall r. ST r (MVector r ty a)) -> Vector ty a
+{-@ create :: x:VSEXPTYPE s a -> (forall r. ST r (TMVector r a (vstypeOf x))) -> TVector a (vstypeOf x) @-}
+create :: Storable a => VSEXPTYPE s a -> (forall r. ST r (MVector r a)) -> Vector a
 {-# INLINE create #-}
 -- NOTE: eta-expanded due to http://hackage.haskell.org/trac/ghc/ticket/4120
-create f = phony $ \p -> unW $ G.create (Mutable.withW p <$> f)
+create _t f = phony $ \p -> unW $ G.create (Mutable.withW p <$> f)
 
+{-
 -- Restricting memory usage
 -- ------------------------
 
@@ -1679,26 +1735,27 @@ scanr1' f v = phony $ unW . proxyFW (G.scanr1' f) v
 
 -- Conversions - Lists
 -- ------------------------
-
+-}
 -- | /O(n)/ Convert a vector to a list
-toList :: SVECTOR ty a => Vector ty a -> [a]
+toList :: Storable a => Vector a -> [a]
 {-# INLINE toList #-}
 toList v = phony $ proxyFW G.toList v
 
 -- | /O(n)/ Convert a list to a vector
-fromList :: forall ty a . SVECTOR ty a => [a] -> Vector ty a
+{-@ assume fromList :: forall a . Storable a => t:VSEXPTYPE s a -> [a] -> TVector a (vstypeOf t) @-}
+fromList :: Storable a => VSEXPTYPE s a -> [a] -> Vector a
 {-# INLINE fromList #-}
-fromList xs = phony $ proxyW (G.fromListN (Prelude.length xs) xs)
+fromList _t xs = phony $ proxyW (G.fromListN (Prelude.length xs) xs)
 
 -- | /O(n)/ Convert the first @n@ elements of a list to a vector
 --
 -- @
 -- fromListN n xs = 'fromList' ('take' n xs)
 -- @
-fromListN :: forall ty a . SVECTOR ty a => Int -> [a] -> Vector ty a
+fromListN :: Storable a => VSEXPTYPE s a -> Int -> [a] -> Vector a
 {-# INLINE fromListN #-}
-fromListN i l = phony $ proxyW (G.fromListN i l)
-
+fromListN _t i l = phony $ proxyW (G.fromListN i l)
+{-
 -- Conversions - Unsafe casts
 -- --------------------------
 
@@ -1745,11 +1802,12 @@ copy :: (MonadR m, VECTOR (Region m) ty a, ElemRep V ty ~ a)
      => MVector (Region m) ty a -> Vector ty a -> m ()
 {-# INLINE copy #-}
 copy m1 v2 = withAcquire $ \p -> G.copy (Mutable.withW p m1) (withW p v2)
+      -}
 
-phony :: (forall t . Reifies t (AcquireIO s) => Proxy t -> r) -> r
-phony f = reify (AcquireIO acquireIO) $ \p ->  f p
+phony
+  :: forall s r.
+     (forall t. Reifies t (AcquireIO s, IO R.SEXPTYPE) => Proxy t -> r) -> r
+phony f =
+    reify acquireIO $ \p -> f p
   where
-    acquireIO :: SEXP V ty -> IO (SEXP g ty)
-    acquireIO x = mask_ $ do
-      R.preserveObject x
-      return $ R.unsafeRelease x
+    acquireIO = violation "phony" "phony acquire or SEXPTYPE called."
diff --git a/inline-r/src/Data/Vector/SEXP/Base.hs b/inline-r/src/Data/Vector/SEXP/Base.hs
index b0502f80..28a608c0 100644
--- a/inline-r/src/Data/Vector/SEXP/Base.hs
+++ b/inline-r/src/Data/Vector/SEXP/Base.hs
@@ -5,7 +5,9 @@
 {-# OPTIONS_GHC -fplugin-opt=LiquidHaskell:--skip-module=False #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
+{-@ LIQUID "--exact-data-cons" @-}
 
 module Data.Vector.SEXP.Base where
 
@@ -36,6 +38,30 @@ type family ElemRep s (a :: SEXPTYPE) where
   ElemRep s 'Expr    = SEXP s
   ElemRep s 'Raw     = Word8
 
+data VSEXPTYPE s a where
+  VChar :: VSEXPTYPE s Word8
+  VLogical :: VSEXPTYPE s Logical
+  VInt :: VSEXPTYPE s Int32
+  VReal :: VSEXPTYPE s Double
+  VComplex :: VSEXPTYPE s (Complex Double)
+  VString :: VSEXPTYPE s (SEXP s)
+  VVector :: VSEXPTYPE s (SEXP s)
+  VExpr :: VSEXPTYPE s (SEXP s)
+  VRaw :: VSEXPTYPE s Word8
+
+
+{-@ reflect vstypeOf @-}
+vstypeOf :: VSEXPTYPE s a -> SEXPTYPE
+vstypeOf VChar = Char
+vstypeOf VLogical = Logical
+vstypeOf VInt = Int
+vstypeOf VReal = Real
+vstypeOf VComplex = Complex
+vstypeOf VString = String
+vstypeOf VVector = Vector
+vstypeOf VExpr = Expr
+vstypeOf VRaw = Raw
+
 -- | 'ElemRep' in the form of a relation, for convenience.
 type E s a b = ElemRep s a ~ b
 
@@ -43,4 +69,4 @@ type E s a b = ElemRep s a ~ b
 -- type VECTOR s ty a = (Storable a, IsVector ty, SingI ty)
 
 -- | Constraint synonym for all operations on vectors.
-type SVECTOR ty a = (Storable a, IsVector ty, SingI ty, ElemRep V ty ~ a)
+-- type SVECTOR ty a = (Storable a, IsVector ty, SingI ty, ElemRep V ty ~ a)