diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr
index dacf24e9e..7cc362e25 100644
--- a/libs/prelude/Builtins.idr
+++ b/libs/prelude/Builtins.idr
@@ -5,18 +5,19 @@
 
 ||| The canonical single-element type, also known as the trivially
 ||| true proposition.
-data Unit = 
+%elim 
+ data Unit = 
    ||| The trivial constructor for `()`.
    MkUnit         
   
 ||| The non-dependent pair type, also known as conjunction.
 ||| @A the type of the left elements in the pair
 ||| @B the type of the left elements in the pair
-data Pair : (A : Type) -> (B : Type) -> Type =
+data Pair : (A : Type) -> (B : Type) -> Type where
    ||| A pair of elements
    ||| @a the left element of the pair
    ||| @b the right element of the pair
-   MkPair : (a : A) -> (b : B) -> Pair A B
+   MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
          
 ||| Dependent pairs, in their internal representation
 ||| @ a the type of the witness
diff --git a/libs/prelude/Prelude/Basics.idr b/libs/prelude/Prelude/Basics.idr
index 945b2e45f..03949a556 100644
--- a/libs/prelude/Prelude/Basics.idr
+++ b/libs/prelude/Prelude/Basics.idr
@@ -1,5 +1,7 @@
 module Prelude.Basics
 
+import Builtins
+       
 Not : Type -> Type
 Not a = a -> _|_
 
diff --git a/libs/prelude/Prelude/Classes.idr b/libs/prelude/Prelude/Classes.idr
index 572fd40c8..52455a896 100644
--- a/libs/prelude/Prelude/Classes.idr
+++ b/libs/prelude/Prelude/Classes.idr
@@ -28,10 +28,8 @@ class Eq a where
     x /= y = not (x == y)
     x == y = not (x /= y)
 
-%logging 5
 instance Eq () where
   () == () = True
-%logging 0
 
 instance Eq Int where
     (==) = boolOp prim__eqInt
diff --git a/samples/reflection.idr b/samples/reflection.idr
index bb7d4ac61..462c64ab3 100644
--- a/samples/reflection.idr
+++ b/samples/reflection.idr
@@ -32,13 +32,13 @@ envList = ?envListPrf
 
 ||| Reflected raw rep. for the type (TTName, TT)
 tupleType : Raw
-tupleType = RApp (RApp (Var (MN 0 "__Pair"))
+tupleType = RApp (RApp (Var (UN "Pair"))
                        (Var (NS (UN "TTName") ["Reflection", "Language"])))
                  (Var (NS (UN "TT") ["Reflection", "Language"]))
 
 ||| Reflected raw rep for the type List (TTName, TT)
 mkTuple : Raw
-mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))
+mkTuple = RApp (RApp (Var (UN "MkPair"))
                      (Var (NS (UN "TTName") ["Reflection", "Language"])))
                (Var (NS (UN "TT") ["Reflection", "Language"]))
 
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
index d0ff060e8..5651523d0 100644
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -1065,16 +1065,10 @@ getInferType (App (App _ ty) _) = ty
 
 -- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
 
-primNames = [unitTy, unitCon,
-             falseTy, pairTy, pairCon,
-             eqTy, eqCon, inferTy, inferCon]
+primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]
 
-unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
 unitTy   = sUN "Unit"
 unitCon  = sUN "MkUnit"
-unitDecl = PDatadecl unitTy PType
-                     [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
-unitOpts = [DefaultEliminator]
 
 falseDoc = parseDocstring . T.pack $
              "The empty type, also known as the trivially false proposition." ++
@@ -1085,25 +1079,8 @@ falseTy   = sMN 0 "__False"
 falseDecl = PDatadecl falseTy PType []
 falseOpts = []
 
-pairDoc   = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
 pairTy    = sUN "Pair"
 pairCon   = sUN "MkPair"
-pairDecl  = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
-            [(pairConDoc, pairConParamDoc,
-             pairCon, PPi impl (n "A") PType (
-                               PPi impl (n "B") PType (
-                               PPi expl (n "a") (PRef bi (n "A")) (
-                               PPi expl (n "b") (PRef bi (n "B"))
-                                (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
-                                                           pexp (PRef bi (n "B"))])))), bi, [])]
-    where n a = sMN 0 a
-          pairConDoc      = parseDocstring . T.pack $ "A pair of elements"
-          pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),
-                             (n "b", parseDocstring . T.pack $ "the right element of the pair")]
-pairOpts = []
-pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),
-                (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]
-    where n a = sMN 0 a
 
 eqTy = sUN "="
 eqCon = sUN "Refl"
diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
index d711a2019..a8535a888 100644
--- a/src/Idris/ElabDecls.hs
+++ b/src/Idris/ElabDecls.hs
@@ -76,10 +76,10 @@ elabPrims :: Idris ()
 elabPrims = do mapM_ (elabDecl' EAll recinfo)
                      (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
                         (zip4
-                         [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
-                         [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]
-                         [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]
-                         [[], [], [], pairParamDoc, eqParamDoc]))
+                         [inferOpts,      falseOpts, eqOpts]
+                         [inferDecl,      falseDecl, eqDecl]
+                         [emptyDocstring, falseDoc,  eqDoc]
+                         [[],             [],   eqParamDoc]))
                addNameHint eqTy (sUN "prf")
                mapM_ elabPrim primitives
                -- Special case prim__believe_me because it doesn't work on just constants
diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs
index fe66dc6e0..485a682b6 100644
--- a/src/Idris/ElabTerm.hs
+++ b/src/Idris/ElabTerm.hs
@@ -245,8 +245,12 @@ elab ist info emode opts fn tm
 --       = lift $ tfail (Msg "Typecase is not allowed") 
     elab' ina (PConstant c)  = do apply (RConstant c) []; solve
     elab' ina (PQuote r)     = do fill r; solve
-    elab' ina (PTrue fc _)   = try (elab' ina (PRef fc unitCon))
-                                   (elab' ina (PRef fc unitTy))
+    elab' ina (PTrue fc _)   =
+       do hnf_compute
+          g <- goal
+          case g of
+            TType _ -> elab' ina (PRef fc unitTy)
+            _ -> elab' ina (PRef fc unitCon)
     elab' ina (PFalse fc)    = elab' ina (PRef fc falseTy)
     elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
        = do g <- goal; resolveTC False 5 g fn ist
@@ -283,11 +287,11 @@ elab ist info emode opts fn tm
         = do hnf_compute
              g <- goal
              case g of
-                TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)
+                TType _ -> elab' ina (PApp fc (PRef fc pairTy)
                                                       [pexp l,pexp r])
-                _ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)
-                                                [pimp (sMN 0 "A") Placeholder True,
-                                                 pimp (sMN 0 "B") Placeholder True,
+                _ -> elab' ina (PApp fc (PRef fc pairCon)
+                                                [pimp (sUN "A") Placeholder False,
+                                                 pimp (sUN "B") Placeholder False,
                                                  pexp l, pexp r])
     elab' ina (PDPair fc p l@(PRef _ n) t r)
             = case t of
diff --git a/test/quasiquote001/expected b/test/quasiquote001/expected
index 6b9c1f39e..579771d78 100644
--- a/test/quasiquote001/expected
+++ b/test/quasiquote001/expected
@@ -1,5 +1,5 @@
-(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10))))))
+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 9 0) (UN Unit) (TType (UVar -1))))))
 --------------
-(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 190))) (TType (UVar 192))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 194))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 196)))))
+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 50))) (TType (UVar 52))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 54))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 56)))))
 --------------
-(App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190)))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190))))
+(App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50)))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50))))