diff --git a/inline-r/inline-r.cabal b/inline-r/inline-r.cabal
index cbcaca90..17b180ac 100644
--- a/inline-r/inline-r.cabal
+++ b/inline-r/inline-r.cabal
@@ -59,18 +59,19 @@ library
     Foreign.R.Internal
     Foreign.R.Parse
     Foreign.R.Type
+    Foreign.R.Type.Singletons
 --    H.Prelude
 --    H.Prelude.Interactive
---    Language.R
+    Language.R
 --    Language.R.Debug
     Language.R.GC
     Language.R.Globals
     Language.R.HExp
     Language.R.Instance
---    Language.R.Internal
+    Language.R.Internal
     Language.R.Internal.FunWrappers
     Language.R.Internal.FunWrappers.TH
---    Language.R.Literal
+    Language.R.Literal
 --    Language.R.Matcher
 --    Language.R.QQ
   if !os(windows)
diff --git a/inline-r/src/Language/R.hs b/inline-r/src/Language/R.hs
index 79c2555b..dce32e60 100644
--- a/inline-r/src/Language/R.hs
+++ b/inline-r/src/Language/R.hs
@@ -36,12 +36,8 @@ import qualified Data.Vector.SEXP as Vector
 import Control.Monad.R.Class
 import Foreign.R
   ( SEXP
-  , SomeSEXP(..)
   , typeOf
-  , asTypeOf
   , cast
-  , unSomeSEXP
-  , unsafeCoerce
   )
 import qualified Foreign.R as R
 import qualified Foreign.R.Parse as R
@@ -73,7 +69,7 @@ import Prelude
 -- the dependency hierarchy.
 
 -- | Parse and then evaluate expression.
-parseEval :: ByteString -> IO (SomeSEXP V)
+parseEval :: ByteString -> IO (SEXP V)
 parseEval txt = useAsCString txt $ \ctxt ->
   R.withProtected (R.mkString ctxt) $ \rtxt ->
     alloca $ \status -> do
@@ -90,18 +86,20 @@ parseEval txt = useAsCString txt $ \ctxt ->
 --
 -- This function uses continuation because this is an easy way to make
 -- operations GC-safe.
-parseFile :: FilePath -> (SEXP s 'R.Expr -> IO a) -> IO a
+{-@ parseFile :: FilePath -> (SEXP s 'R.Expr -> IO a) -> IO a @-}
+parseFile :: FilePath -> (SEXP s -> IO a) -> IO a
 {-# DEPRECATED parseFile "Use [r| parse(file=\"path/to/file\") |] instead." #-}
 parseFile fl f = do
     withCString fl $ \cfl ->
       R.withProtected (R.mkString cfl) $ \rfl ->
         r1 (C8.pack "parse") rfl >>= \(R.SomeSEXP s) ->
-          return (R.unsafeCoerce s) `R.withProtected` f
+          return s `R.withProtected` f
 
+{-@ parseText :: String -> Bool -> IO (R.SEXP V 'R.Expr) @-}
 parseText
   :: String -- ^ Text to parse
   -> Bool   -- ^ Whether to annotate the AST with source locations.
-  -> IO (R.SEXP V 'R.Expr)
+  -> IO (R.SEXP V)
 {-# DEPRECATED parseText "Use [r| parse(text=...) |] instead." #-}
 parseText txt b = do
     s <- parseEval $ C8.pack $
@@ -112,22 +110,26 @@ parseText txt b = do
          | otherwise = "FALSE"
 
 -- | Internalize a symbol name.
-install :: MonadR m => String -> m (SEXP V 'R.Symbol)
+{-@ install :: String -> m (SEXP V 'R.Symbol) @-}
+install :: MonadR m => String -> m (SEXP V)
 install = io . installIO
 
 {-# DEPRECATED string, strings "Use mkSEXP instead" #-}
 
 -- | Create an R character string from a Haskell string.
-string :: String -> IO (SEXP V 'R.Char)
+{-@ string :: String -> IO (SEXP V 'R.Char) @-}
+string :: String -> IO (SEXP V)
 string str = withCString str R.mkChar
 
 -- | Create an R string vector from a Haskell string.
-strings :: String -> IO (SEXP V 'R.String)
+{-@ strings :: String -> IO (SEXP V 'R.String) @-}
+strings :: String -> IO (SEXP V)
 strings str = withCString str R.mkString
 
 -- | Evaluate a (sequence of) expression(s) in the given environment, returning the
 -- value of the last.
-evalEnv :: MonadR m => SEXP s a -> SEXP s 'R.Env -> m (SomeSEXP (Region m))
+{-@ evalEnv :: SEXP s a -> SEXP s 'R.Env -> m (SEXP (Region m)) @-}
+evalEnv :: MonadR m => SEXP s -> SEXP s -> m (SEXP (Region m))
 evalEnv (hexp -> Language.R.HExp.Expr _ v) rho = acquireSome =<< do
     io $ alloca $ \p -> do
       mapM_ (\(SomeSEXP s) -> void $ R.protect s) (Vector.toList v)
@@ -146,14 +148,15 @@ evalEnv x rho = acquireSome =<< do
       return v
 
 -- | Evaluate a (sequence of) expression(s) in the global environment.
-eval :: MonadR m => SEXP s a -> m (SomeSEXP (Region m))
+eval :: MonadR m => SEXP s -> m (SEXP (Region m))
 eval x = evalEnv x (R.release globalEnv)
 
 -- | Silent version of 'eval' function that discards it's result.
-eval_ :: MonadR m => SEXP s a -> m ()
+eval_ :: MonadR m => SEXP s -> m ()
 eval_ = void . eval
 
 -- | Throw an R error as an exception.
+{-@ throwR :: R.SEXP s 'R.Env -> m a @-}
 throwR :: MonadR m => R.SEXP s 'R.Env   -- ^ Environment in which to find error.
        -> m a
 throwR env = getErrorMessage env >>= io . throwIO . R.RError
@@ -173,7 +176,8 @@ throwRMessage :: MonadR m => String -> m a
 throwRMessage = io . throwIO . R.RError
 
 -- | Read last error message.
-getErrorMessage :: MonadR m => R.SEXP s 'R.Env -> m String
+{-@ getErrorMessage :: MonadR m => R.SEXP s 'R.Env -> m String @-}
+getErrorMessage :: MonadR m => R.SEXP s -> m String
 getErrorMessage e = io $ do
   R.withProtected (withCString "geterrmessage" ((R.install >=> R.lang1))) $ \f -> do
     R.withProtected (return (R.release e)) $ \env -> do
diff --git a/inline-r/src/Language/R/Internal.hs b/inline-r/src/Language/R/Internal.hs
index 3aecf408..45bdf114 100644
--- a/inline-r/src/Language/R/Internal.hs
+++ b/inline-r/src/Language/R/Internal.hs
@@ -19,17 +19,18 @@ inVoid = id
 {-# INLINE inVoid #-}
 
 -- | Call a pure unary R function of the given name in the global environment.
-r1 :: ByteString -> SEXP s a -> IO (SomeSEXP V)
+r1 :: ByteString -> SEXP s -> IO (SEXP V)
 r1 fn a =
     useAsCString fn $ \cfn -> R.install cfn >>= \f ->
       R.withProtected (R.lang2 f (R.release a)) (unsafeRunRegion . inVoid . eval)
 
 -- | Call a pure binary R function. See 'r1' for additional comments.
-r2 :: ByteString -> SEXP s a -> SEXP s b -> IO (SomeSEXP V)
+r2 :: ByteString -> SEXP s -> SEXP s -> IO (SEXP V)
 r2 fn a b =
     useAsCString fn $ \cfn -> R.install cfn >>= \f ->
       R.withProtected (R.lang3 f (R.release a) (R.release b)) (unsafeRunRegion . inVoid . eval)
 
 -- | Internalize a symbol name.
-installIO :: String -> IO (SEXP V 'R.Symbol)
+{-@ installIO :: String -> IO (TSEXP V Foreign.R.Type.Symbol) @-}
+installIO :: String -> IO (SEXP V)
 installIO str = withCString str R.install
diff --git a/inline-r/src/Language/R/Internal.hs-boot b/inline-r/src/Language/R/Internal.hs-boot
index 3457a22e..25489f8a 100644
--- a/inline-r/src/Language/R/Internal.hs-boot
+++ b/inline-r/src/Language/R/Internal.hs-boot
@@ -4,9 +4,8 @@ module Language.R.Internal where
 
 import Control.Memory.Region
 import Data.ByteString (ByteString)
-import Foreign.R (SEXP, SomeSEXP(..))
-import qualified Foreign.R.Type as R
+import Foreign.R (SEXP)
 
-r1 :: ByteString -> SEXP s a -> IO (SomeSEXP V)
-r2 :: ByteString -> SEXP s a -> SEXP s b -> IO (SomeSEXP V)
-installIO :: String -> IO (SEXP V 'R.Symbol)
+r1 :: ByteString -> SEXP s -> IO (SEXP V)
+r2 :: ByteString -> SEXP s -> SEXP s -> IO (SEXP V)
+installIO :: String -> IO (SEXP V)
diff --git a/inline-r/src/Language/R/Literal.hs b/inline-r/src/Language/R/Literal.hs
index 7a7ccca6..75e8878d 100644
--- a/inline-r/src/Language/R/Literal.hs
+++ b/inline-r/src/Language/R/Literal.hs
@@ -9,6 +9,7 @@
 {-# Language FlexibleInstances #-}
 {-# Language FunctionalDependencies #-}
 {-# Language GADTs #-}
+{-# Language KindSignatures #-}
 {-# Language LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -17,8 +18,11 @@
 {-# Language ViewPatterns #-}
 
 -- required to not warn about IsVector usage.
-{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints -fplugin-opt=LiquidHaskell:--skip-module=False #-}
+{-@ LIQUID "--exact-data-cons" @-} -- needed to have LH accept specs in module HExp
+{-@ LIQUID "--prune-unsorted" @-}
 module Language.R.Literal
+  {-
   ( -- * Literals conversion
     Literal(..)
   , toPairList
@@ -33,16 +37,20 @@ module Language.R.Literal
   , mkProtectedSEXPVectorIO
     -- * Internal
   , funToSEXP
-  ) where
+  ) -} where
 
 import           Control.Memory.Region
 import           Control.Monad.R.Class
 import qualified Data.Vector.SEXP as SVector
 import qualified Data.Vector.SEXP.Mutable as SMVector
+import qualified Data.Vector.SEXP.Mutable as Mutable -- Needed to help LH name resolution
+import           Foreign.C  -- Needed to help LH name resolution
 import qualified Foreign.R as R
-import qualified Foreign.R.Internal as R (somesexp)
-import           Foreign.R.Type ( IsVector, SSEXPTYPE )
-import           Foreign.R ( SEXP, SomeSEXP(..) )
+import           Foreign.R.Type ( IsVector )
+import           Foreign.R.Type.Singletons (SSEXPTYPE)
+import           Foreign.R ( SEXP )
+import           GHC.ForeignPtr -- Needed to help LH name resolution
+import           GHC.ST -- Needed to help LH name resolution
 import           Internal.Error
 import           {-# SOURCE #-} Language.R.Internal (r1)
 import           Language.R.Globals (nilValue)
@@ -67,74 +75,87 @@ import qualified GHC.Foreign as GHC
 import GHC.IO.Encoding.UTF8
 import System.IO.Unsafe ( unsafePerformIO )
 
+{-@ measure Language.R.Literal.literalRType :: a -> R.SEXPTYPE @-}
+
 -- | Values that can be converted to 'SEXP'.
-class SingI ty => Literal a ty | a -> ty where
+class SingI ty => Literal a (ty :: R.SEXPTYPE) | a -> ty where
     -- | Internal function for converting a literal to a 'SEXP' value. You
     -- probably want to be using 'mkSEXP' instead.
-    mkSEXPIO :: a -> IO (SEXP V ty)
-    fromSEXP :: SEXP s ty -> a
+    {-@ mkSEXPIO :: x:a -> IO (TSEXP V (literalRType x)) @-}
+    mkSEXPIO :: a -> IO (SEXP V)
+    {-@ fromSEXP :: s:SEXP s -> {v:a | literalRType v == typeOf s} @-}
+    fromSEXP :: SEXP s -> a
+
+    {-@ literalRType :: x:a -> {v:R.SEXPTYPE | v == literalRType x } @-}
+    literalRType :: a -> R.SEXPTYPE
 
-    default mkSEXPIO :: (IsVector ty, Literal [a] ty) => a -> IO (SEXP V ty)
+{-
+    default mkSEXPIO :: (IsVector ty, Literal [a] ty) => a -> IO (SEXP V)
     mkSEXPIO x = mkSEXPIO [x]
 
-    default fromSEXP :: (IsVector ty, Literal [a] ty) => SEXP s ty -> a
+    default fromSEXP :: (IsVector ty, Literal [a] ty) => SEXP s -> a
     fromSEXP (fromSEXP -> [x]) = x
     fromSEXP _ = failure "fromSEXP" "Not a singleton vector."
+-}
 
 -- |  Create a SEXP value and protect it in current region
-mkSEXP :: (Literal a b, MonadR m) => a -> m (SEXP (Region m) b)
-mkSEXP x = acquire =<< io (mkSEXPIO x)
-
--- | Like 'fromSEXP', but with no static type satefy. Performs a dynamic
--- (i.e. at runtime) check instead.
-fromSomeSEXP :: forall s a form. (Literal a form) => R.SomeSEXP s -> a
-fromSomeSEXP = fromSEXP . R.cast (sing :: Sing form)
+{-@ assume mkSEXP :: x:a -> m (TSEXP (Region m) (literalRType x)) @-}
+mkSEXP :: (Literal a b, MonadR m) => a -> m (SEXP (Region m))
+mkSEXP x = io (mkSEXPIO x) >>= \a -> acquire a
 
 -- | Like 'fromSomeSEXP', but behaves like the @as.*@ family of functions
 -- in R, by performing a best effort conversion to the target form (e.g. rounds
 -- reals to integers, etc) for atomic types.
-dynSEXP :: forall a s ty. (Literal a ty) => SomeSEXP s -> a
-dynSEXP (SomeSEXP sx) =
-    fromSomeSEXP $ unsafePerformIO $ case fromSing (sing :: SSEXPTYPE ty) of
+dynSEXP :: forall a s ty. (Literal a ty) => SEXP s -> a
+dynSEXP sx =
+    fromSEXP $ unsafePerformIO $ case fromSing (sing :: SSEXPTYPE ty) of
       R.Char -> r1 "as.character" sx
       R.Int -> r1 "as.integer" sx
       R.Real -> r1 "as.double" sx
       R.Complex -> r1 "as.complex" sx
       R.Logical -> r1 "as.logical" sx
       R.Raw -> r1 "as.raw" sx
-      _ -> return $ SomeSEXP $ R.release sx
+      _ -> return $ R.release sx
 
 {-# NOINLINE mkSEXPVector #-}
-mkSEXPVector :: (Storable (SVector.ElemRep s a), IsVector a)
-             => SSEXPTYPE a
-             -> [IO (SVector.ElemRep s a)]
-             -> SEXP s a
+{-@ mkSEXPVector :: vt:VSEXPTYPE s a -> [IO a] -> TSEXP s (vstypeOf vt) @-}
+mkSEXPVector :: Storable a
+             => SVector.VSEXPTYPE s a
+             -> [IO a]
+             -> SEXP s
 mkSEXPVector ty allocators = unsafePerformIO $ mkSEXPVectorIO ty allocators
 
-mkSEXPVectorIO :: (Storable (SVector.ElemRep s a), IsVector a)
-               => SSEXPTYPE a
-               -> [IO (SVector.ElemRep s a)]
-               -> IO (SEXP s a)
+{-@ assume mkSEXPVectorIO :: vt:VSEXPTYPE s a -> [IO a] -> IO (TSEXP s (vstypeOf vt)) @-}
+{-@ ignore mkSEXPVectorIO @-}
+mkSEXPVectorIO :: Storable a
+               => SVector.VSEXPTYPE s a
+               -> [IO a]
+               -> IO (SEXP s)
 mkSEXPVectorIO ty allocators =
-    R.withProtected (R.allocVector ty $ length allocators) $ \vec -> do
+    R.withProtected (R.allocVector (SVector.vstypeOf ty) $ length allocators) $ \vec -> do
       let ptr = castPtr $ R.unsafeSEXPToVectorPtr vec
       zipWithM_ (\i -> (>>= pokeElemOff ptr i)) [0..] allocators
       return vec
 
 {-# NOINLINE mkProtectedSEXPVector #-}
-mkProtectedSEXPVector :: IsVector b
-                      => SSEXPTYPE b
-                      -> [SEXP s a]
-                      -> SEXP s b
+{-@
+mkProtectedSEXPVector :: vt:VSEXPTYPE s a -> [SEXP s] -> TSEXP s (vstypeOf vt)
+@-}
+mkProtectedSEXPVector :: SVector.VSEXPTYPE s a
+                      -> [SEXP s]
+                      -> SEXP s
 mkProtectedSEXPVector ty xs = unsafePerformIO $ mkProtectedSEXPVectorIO ty xs
 
-mkProtectedSEXPVectorIO :: IsVector b
-                        => SSEXPTYPE b
-                        -> [SEXP s a]
-                        -> IO (SEXP s b)
+{-@
+assume mkProtectedSEXPVectorIO :: vt:VSEXPTYPE s a -> [SEXP s] -> IO (TSEXP s (vstypeOf vt))
+ignore mkProtectedSEXPVectorIO
+@-}
+mkProtectedSEXPVectorIO :: SVector.VSEXPTYPE s a
+                        -> [SEXP s]
+                        -> IO (SEXP s)
 mkProtectedSEXPVectorIO ty xs = do
     mapM_ (void . R.protect) xs
-    z <- R.withProtected (R.allocVector ty $ length xs) $ \vec -> do
+    z <- R.withProtected (R.allocVector (SVector.vstypeOf ty) $ length xs) $ \vec -> do
            let ptr = castPtr $ R.unsafeSEXPToVectorPtr vec
            zipWithM_ (pokeElemOff ptr) [0..] xs
            return vec
@@ -142,9 +163,10 @@ mkProtectedSEXPVectorIO ty xs = do
     return z
 
 instance Literal [R.Logical] 'R.Logical where
-    mkSEXPIO = mkSEXPVectorIO sing . map return
+    mkSEXPIO = mkSEXPVectorIO (fromSing sing) . map return
     fromSEXP (hexp -> Logical v) = SVector.toList v
 
+{-
 instance Literal [Int32] 'R.Int where
     mkSEXPIO = mkSEXPVectorIO sing . map return
     fromSEXP (hexp -> Int v) = SVector.toList v
@@ -256,7 +278,7 @@ instance (NFData a, Literal a la) => HFunWrap (R s a) (IO R.SEXP0) where
 
 instance (Literal a la, HFunWrap b wb)
          => HFunWrap (a -> b) (R.SEXP0 -> wb) where
-    hFunWrap f a = hFunWrap $ f $! fromSEXP (R.cast sing (R.somesexp a) :: SEXP s la)
+    hFunWrap f a = hFunWrap $ f $! fromSEXP (R.SEXP a :: SEXP s la)
 
 foreign import ccall "missing_r.h funPtrToSEXP" funPtrToSEXP
     :: FunPtr a -> IO (SEXP s 'R.ExtPtr)
@@ -265,3 +287,4 @@ funToSEXP :: HFunWrap a b => (b -> IO (FunPtr b)) -> a -> IO (SEXP s 'R.ExtPtr)
 funToSEXP w x = funPtrToSEXP =<< w (hFunWrap x)
 
 $(thWrapperLiterals 3 12)
+-}