diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2013-2014, Ranjit Jhala
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Ranjit Jhala nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-ghc-prim.cabal b/liquid-ghc-prim.cabal
new file mode 100644
--- /dev/null
+++ b/liquid-ghc-prim.cabal
@@ -0,0 +1,46 @@
+cabal-version:      1.24
+name:               liquid-ghc-prim
+version:            0.6.1
+synopsis:           Drop-in ghc-prim replacement for LiquidHaskell
+description:        Drop-in ghc-prim replacement for LiquidHaskell.
+license:            BSD3
+license-file:       LICENSE
+copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.
+author:             Ranjit Jhala, Niki Vazou, Eric Seidel
+maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
+category:           Language
+homepage:           https://github.com/ucsd-progsys/liquidhaskell
+build-type:         Custom
+
+data-files:         src/GHC/*.spec
+
+
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
+library
+  exposed-modules:
+                    -- We can't really export 'GHC.Prim' or this won't build on Windows,
+                    -- unfortunately. The issue is that 'GHC.Prim' is a special snowflake,
+                    -- treated specially by the GHC pipeline. In particular, GHC doesn't
+                    -- generate a '.hi' file for it, and this causes Windows' builds to choke.
+                    -- GHC.Prim
+                    GHC.CString
+                    GHC.Classes
+                    GHC.Debug
+                    GHC.IntWord64
+                    GHC.Magic
+                    GHC.Prim.Ext
+                    GHC.PrimopWrappers
+                    GHC.Tuple
+                    GHC.Types
+
+  hs-source-dirs:     src
+  build-depends:      ghc-prim             == 0.6.1
+                    , liquidhaskell        >= 0.8.10.1
+  default-language:   Haskell2010
+  default-extensions: PackageImports
+                      NoImplicitPrelude
+                      MagicHash
+  if impl(ghc >= 8.10)
+    ghc-options: -fplugin=LiquidHaskell
diff --git a/src/GHC/CString.hs b/src/GHC/CString.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/CString.hs
@@ -0,0 +1,5 @@
+module GHC.CString (module Exports) where
+
+import "this" GHC.Types
+
+import "ghc-prim" GHC.CString as Exports
diff --git a/src/GHC/CString.spec b/src/GHC/CString.spec
new file mode 100644
--- /dev/null
+++ b/src/GHC/CString.spec
@@ -0,0 +1,9 @@
+module spec GHC.CString where
+
+import GHC.Types
+
+measure strLen :: Addr# -> GHC.Types.Int
+
+GHC.CString.unpackCString#
+  :: x:GHC.Prim.Addr#
+  -> {v:[Char] | v ~~ x && len v == strLen x}
diff --git a/src/GHC/Classes.hs b/src/GHC/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Classes.hs
@@ -0,0 +1,4 @@
+module GHC.Classes (module Exports) where
+
+import GHC.Types
+import "ghc-prim" GHC.Classes as Exports
diff --git a/src/GHC/Classes.spec b/src/GHC/Classes.spec
new file mode 100644
--- /dev/null
+++ b/src/GHC/Classes.spec
@@ -0,0 +1,29 @@
+module spec GHC.Classes where
+
+import GHC.Types
+
+not     :: x:GHC.Types.Bool -> {v:GHC.Types.Bool | ((v) <=> ~(x))}
+(&&)    :: x:GHC.Types.Bool -> y:GHC.Types.Bool
+        -> {v:GHC.Types.Bool | ((v) <=> ((x) && (y)))}
+(||)    :: x:GHC.Types.Bool -> y:GHC.Types.Bool
+        -> {v:GHC.Types.Bool | ((v) <=> ((x) || (y)))}
+(==)    :: (GHC.Classes.Eq  a) => x:a -> y:a
+        -> {v:GHC.Types.Bool | ((v) <=> x = y)}
+(/=)    :: (GHC.Classes.Eq  a) => x:a -> y:a
+        -> {v:GHC.Types.Bool | ((v) <=> x != y)}
+(>)     :: (GHC.Classes.Ord a) => x:a -> y:a
+        -> {v:GHC.Types.Bool | ((v) <=> x > y)}
+(>=)    :: (GHC.Classes.Ord a) => x:a -> y:a
+        -> {v:GHC.Types.Bool | ((v) <=> x >= y)}
+(<)     :: (GHC.Classes.Ord a) => x:a -> y:a
+        -> {v:GHC.Types.Bool | ((v) <=> x < y)}
+(<=)    :: (GHC.Classes.Ord a) => x:a -> y:a
+        -> {v:GHC.Types.Bool | ((v) <=> x <= y)}
+
+compare :: (GHC.Classes.Ord a) => x:a -> y:a
+        -> {v:GHC.Types.Ordering | (((v = GHC.Types.EQ) <=> (x = y)) &&
+                                    ((v = GHC.Types.LT) <=> (x < y)) &&
+                                    ((v = GHC.Types.GT) <=> (x > y))) }
+
+max :: (GHC.Classes.Ord a) => x:a -> y:a -> {v:a | v = (if x > y then x else y) }
+min :: (GHC.Classes.Ord a) => x:a -> y:a -> {v:a | v = (if x < y then x else y) }
diff --git a/src/GHC/Debug.hs b/src/GHC/Debug.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Debug.hs
@@ -0,0 +1,3 @@
+module GHC.Debug (module Exports) where
+
+import "ghc-prim" GHC.Debug as Exports
diff --git a/src/GHC/IntWord64.hs b/src/GHC/IntWord64.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/IntWord64.hs
@@ -0,0 +1,3 @@
+module GHC.IntWord64 (module Exports) where
+
+import "ghc-prim" GHC.IntWord64 as Exports
diff --git a/src/GHC/Magic.hs b/src/GHC/Magic.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Magic.hs
@@ -0,0 +1,3 @@
+module GHC.Magic (module Exports) where
+
+import "ghc-prim" GHC.Magic as Exports
diff --git a/src/GHC/Prim/Ext.hs b/src/GHC/Prim/Ext.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Prim/Ext.hs
@@ -0,0 +1,3 @@
+module GHC.Prim.Ext (module Exports) where
+
+import "ghc-prim" GHC.Prim.Ext as Exports
diff --git a/src/GHC/PrimopWrappers.hs b/src/GHC/PrimopWrappers.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/PrimopWrappers.hs
@@ -0,0 +1,3 @@
+module GHC.PrimopWrappers (module Exports) where
+
+import "ghc-prim" GHC.PrimopWrappers as Exports
diff --git a/src/GHC/Tuple.hs b/src/GHC/Tuple.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Tuple.hs
@@ -0,0 +1,3 @@
+module GHC.Tuple (module Exports) where
+
+import "ghc-prim" GHC.Tuple as Exports
diff --git a/src/GHC/Types.hs b/src/GHC/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Types.hs
@@ -0,0 +1,10 @@
+module GHC.Types (module Exports) where
+
+{-@ embed GHC.Prim.Int#     as int @-}
+{-@ embed GHC.Prim.Addr#    as Str @-}
+{-@ embed GHC.Prim.Char#    as Char @-}
+{-@ embed GHC.Prim.Double#  as real @-}
+{-@ embed GHC.Prim.Float#   as real @-}
+{-@ embed GHC.Prim.Word#    as int  @-}
+
+import "ghc-prim" GHC.Types as Exports
diff --git a/src/GHC/Types.spec b/src/GHC/Types.spec
new file mode 100644
--- /dev/null
+++ b/src/GHC/Types.spec
@@ -0,0 +1,35 @@
+module spec GHC.Types where
+
+// Boxed types
+embed GHC.Types.Double  as real
+embed GHC.Types.Float   as real
+embed GHC.Types.Word    as int
+embed GHC.Types.Int     as int
+embed GHC.Types.Bool    as bool
+embed GHC.Types.Char    as Char
+
+embed GHC.Integer.Type.Integer as int
+
+GHC.Types.True  :: {v:GHC.Types.Bool | v     }
+GHC.Types.False :: {v:GHC.Types.Bool | (~ v) }
+GHC.Types.isTrue#  :: n:_ -> {v:GHC.Types.Bool | (n = 1 <=> v)}
+
+GHC.Types.D# :: x:GHC.Prim.Double# -> {v: GHC.Types.Double | v = (x :: real) }
+GHC.Types.F# :: x:GHC.Prim.Float# -> {v: GHC.Types.Float | v = (x :: real) }
+GHC.Types.I# :: x:GHC.Prim.Int# -> {v: GHC.Types.Int | v = (x :: int) }
+GHC.Types.C# :: x:GHC.Prim.Char# -> {v: GHC.Types.Char | v = (x :: Char) }
+GHC.Types.W# :: w:_ -> {v:GHC.Types.Word | v == w }
+
+measure addrLen :: GHC.Prim.Addr# -> GHC.Types.Int
+
+type GeInt N = {v: GHC.Types.Int | v >= N }
+type LeInt N = {v: GHC.Types.Int | v <= N }
+type Nat     = {v: GHC.Types.Int | v >= 0 }
+type Even    = {v: GHC.Types.Int | (v mod 2) = 0 }
+type Odd     = {v: GHC.Types.Int | (v mod 2) = 1 }
+type BNat N  = {v: Nat           | v <= N }
+type TT      = {v: GHC.Types.Bool | v}
+type FF      = {v: GHC.Types.Bool | not v}
+type String  = [GHC.Types.Char]
+
+class measure len :: forall f a. f a -> GHC.Types.Int