diff --git a/StdLib/List.gr b/StdLib/List.gr
index 65a652d79..c6c9fc425 100644
--- a/StdLib/List.gr
+++ b/StdLib/List.gr
@@ -14,7 +14,7 @@ import Result
 import Maybe
 import Bool
 
-data List a where Empty; Next a (List a)
+data List a where Empty | Next a (List a)
 
 --- Append two lists
 append_list : forall {a : Type} . List a -> List a -> List a
diff --git a/StdLib/Vec.gr b/StdLib/Vec.gr
index c6f339a35..68b4b977e 100644
--- a/StdLib/Vec.gr
+++ b/StdLib/Vec.gr
@@ -128,11 +128,11 @@ uncons
 uncons (Cons x xs) = (x,xs)
 
 --- Split a vector at position 'n'
-split
+splitVec
   : forall {a : Type, m n : Nat}
   . N n -> (Vec (n + m) a) -> (Vec n a, Vec m a)
-split Z xs = (Nil, xs);
-split (S n) (Cons x xs) = let (xs', ys') = split n xs in (Cons x xs', ys')
+splitVec Z xs = (Nil, xs);
+splitVec (S n) (Cons x xs) = let (xs', ys') = splitVec n xs in (Cons x xs', ys')
 
 --- Sum a vector of integers (using `foldr`)
 sum
diff --git a/compiler/src/Language/Granule/Compiler/HSCodegen.hs b/compiler/src/Language/Granule/Compiler/HSCodegen.hs
index 3f28fca93..3df0ca69b 100644
--- a/compiler/src/Language/Granule/Compiler/HSCodegen.hs
+++ b/compiler/src/Language/Granule/Compiler/HSCodegen.hs
@@ -134,8 +134,10 @@ cgType (GrType.TyApp t1 t2) =
     t2' <- cgType t2
     return $ Hs.TyApp () t1' t2'
 cgType (GrType.Star _t t2) = cgType t2
+cgType (GrType.Borrow _t t2) = cgType t2
 cgType (GrType.TyInt i) = return mkUnit
 cgType (GrType.TyRational ri) = return mkUnit
+cgType (GrType.TyFraction ri) = return mkUnit
 cgType (GrType.TyGrade mt i) = return mkUnit
 cgType (GrType.TyInfix t1 t2 t3) = return mkUnit
 cgType (GrType.TySet p l_t) = return mkUnit
@@ -143,6 +145,7 @@ cgType (GrType.TyCase t l_p_tt) = unsupported "cgType: tycase not implemented"
 cgType (GrType.TySig t t2) = unsupported "cgType: tysig not implemented"
 cgType (GrType.TyExists _ _ _) = unsupported "cgType: tyexists not implemented"
 cgType (GrType.TyForall _ _ _) = unsupported "cgType: tyforall not implemented"
+cgType (GrType.TyName _) = unsupported "cgType: tyname not implemented"
 
 isTupleType :: GrType.Type -> Bool
 isTupleType (GrType.TyApp (GrType.TyCon id) _) = id == Id "," ","
diff --git a/docs/style.css b/docs/style.css
index e185095b2..228e19537 100644
--- a/docs/style.css
+++ b/docs/style.css
@@ -12,11 +12,16 @@ body {
 }
 
 .code pre {
-  white-space: pre-wrap;       /* css-3 */
-  white-space: -moz-pre-wrap;  /* Mozilla, since 1999 */
-  white-space: -pre-wrap;      /* Opera 4-6 */
-  white-space: -o-pre-wrap;    /* Opera 7 */
-  word-wrap: break-word;       /* Internet Explorer 5.5+ */
+  white-space: pre-wrap;
+  /* css-3 */
+  white-space: -moz-pre-wrap;
+  /* Mozilla, since 1999 */
+  white-space: -pre-wrap;
+  /* Opera 4-6 */
+  white-space: -o-pre-wrap;
+  /* Opera 7 */
+  word-wrap: break-word;
+  /* Internet Explorer 5.5+ */
 }
 
 .inline {
@@ -65,6 +70,11 @@ body {
   color: rgb(194, 2, 50);
 }
 
+.perm,
+.perm span {
+  color: rgb(34, 102, 34);
+}
+
 #navigator {
   width: calc(25vw - 20px - 2 * 20px);
   margin: 0px;
diff --git a/examples/effects_nondet.gr b/examples/effects_nondet.gr
index 32d02f11c..79140a722 100644
--- a/examples/effects_nondet.gr
+++ b/examples/effects_nondet.gr
@@ -10,7 +10,7 @@ import List
 
 data Labels = Toss | Drop
 
--- Operations
+-- (Sigma functor) - Signature of operations
 data GameOps : Set Labels -> Type -> Type where
   FlipCoin : forall {r : Type} . () -> (Bool -> r) [2] -> GameOps {Toss} r;
   Fumble   : forall {r : Type} . () -> (Void -> r) [0] -> GameOps {Drop} r
@@ -33,7 +33,7 @@ foo = call FlipCoin ()
 
 -- Two coin flips, all good
 example1 : (Bool, Bool) <Eff (Set Labels) GameOps {Toss}>
-example1 = let
+example1 = let  -- do x <- ...
   x <- call FlipCoin ();
   y <- call FlipCoin ()
   in pure (x, y)
diff --git a/examples/parallelWithMutation.gr b/examples/parallelWithMutation.gr
new file mode 100644
index 000000000..e7519f943
--- /dev/null
+++ b/examples/parallelWithMutation.gr
@@ -0,0 +1,65 @@
+import Parallel
+import Prelude
+import Vec
+
+--- Convert an indexed natural number to an untyped int
+natToInt'
+  : forall {n : Nat}
+  . N n -> Int
+natToInt' Z = 0;
+natToInt' (S m) = 1 + natToInt' m
+
+toFloatArray : forall {n : Nat} . Vec n Float -> exists {id : Name} . *(FloatArray id)
+toFloatArray v =
+  let (n', v) = length' v
+  in unpack <id, arr> = newFloatArray (natToInt' n')
+  in pack <id, (toFloatArrayAux arr [0] v)> as exists {id : Name} . *(FloatArray id)
+
+toFloatArrayAux : forall {n : Nat, id : Name} . *(FloatArray id) -> Int [n] -> Vec n Float -> *(FloatArray id)
+toFloatArrayAux a [n] Nil = a;
+toFloatArrayAux a [n] (Cons x xs) =
+  toFloatArrayAux (writeFloatArray a n x) [n + 1] xs
+
+sumFromTo : forall {id : Name, f : Fraction} . & f (FloatArray id) ->  !Int -> !Int -> (Float, & f (FloatArray id))
+sumFromTo array [i] [n] =
+  if i == n
+    then (0.0, array)
+    else
+      let (x, a) = readFloatArray array i;
+          (y, arr) = sumFromTo a [i+1] [n]
+      in  (x + y, arr)
+
+-- A reference to a droppable value can be written to without violating linearity
+writeRef : forall {a : Type, id : Name} . {Dropable a} => a -> & 1 (Ref id a) -> & 1 (Ref id a)
+writeRef x r = let
+    (y, r') = swapRef r x;
+    () = drop@a y in r'
+
+parSum : forall {id id' : Name} . *(FloatArray id) -> *(Ref id' Float) -> *(Ref id' Float, FloatArray id)
+parSum array ref = let
+     ([n], array) : (!Int, *(FloatArray id))     = lengthFloatArray array;
+     compIn                                      = borrowPull (ref, array)
+  in flip withBorrow compIn (\compIn ->
+
+                let (ref, array)      = borrowPush compIn;
+                    (array1, array2)  = split array;
+
+                    -- Compute in parallel
+                    ((x, array1), (y, array2)) =
+                                par (\() -> sumFromTo array1 [0] [div n 2])
+                                    (\() -> sumFromTo array2 [div n 2] [n]);
+
+                    -- Update the reference
+                    ref'        = writeRef ((x : Float) + y) ref;
+                    compOut     = borrowPull (ref', join (array1, array2))
+
+                  in compOut)
+
+main : Float
+main =
+  unpack <id , arr> = toFloatArray (Cons 10.0 (Cons 20.0 (Cons 30.0 (Cons 40.0 Nil)))) in
+  unpack <id', ref> = newRef 0.0 in
+  let
+      (result, array) = borrowPush (parSum arr ref);
+      () = deleteFloatArray array
+  in freezeRef result
\ No newline at end of file
diff --git a/examples/simple-clone.gr b/examples/simple-clone.gr
new file mode 100644
index 000000000..6de7c7dbb
--- /dev/null
+++ b/examples/simple-clone.gr
@@ -0,0 +1,4 @@
+example : ()
+example = unpack <id , a> = newFloatArray 3 in
+  clone (share a) as x in
+    unpack <id' , a'> = x in (deleteFloatArray a')
\ No newline at end of file
diff --git a/frontend/granule-frontend.cabal b/frontend/granule-frontend.cabal
index 73aa3f584..acfccaf55 100644
--- a/frontend/granule-frontend.cabal
+++ b/frontend/granule-frontend.cabal
@@ -71,6 +71,7 @@ library
   other-modules:
       Language.Granule.Checker.CoeffectsTypeConverter
       Language.Granule.Checker.Constraints.Compile
+      Language.Granule.Checker.Constraints.SFrac
       Language.Granule.Checker.Constraints.SymbolicGrades
       Language.Granule.Checker.Effects
       Language.Granule.Checker.Exhaustivity
diff --git a/frontend/src/Language/Granule/Checker/Checker.hs b/frontend/src/Language/Granule/Checker/Checker.hs
index 8a076bb9f..9ac64cd50 100644
--- a/frontend/src/Language/Granule/Checker/Checker.hs
+++ b/frontend/src/Language/Granule/Checker/Checker.hs
@@ -663,6 +663,22 @@ checkExpr defs gam pol topLevel tau
       else
         throw $ TypeError { errLoc = s, tyExpected = TyCon $ mkId "DFloat", tyActual = tau }
 
+-- Clone
+-- Pattern match on an applicable of `uniqueBind fun e`
+checkExpr defs gam pol topLevel tau
+   expr@(App s a rf
+     (App _ _ _
+       (Val _ _ _ (Var _ (internalName -> "uniqueBind")))
+       (Val _ _ _ (Abs _ (PVar _ _ _ var) _ body)))
+     e) = do
+  debugM "checkExpr[Clone]" (pretty s <> " : " <> pretty tau)
+  (tau', gam, subst, elab) <- synthExpr defs gam pol expr
+  -- Check the return types match
+  (eqT, _, substTy) <- equalTypes s tau tau'
+  unless eqT $ throw TypeError{ errLoc = s, tyExpected = tau, tyActual = tau' }
+  substF <- combineSubstitutions s subst substTy
+  return (gam, subst, elab)
+
 -- Application checking
 checkExpr defs gam pol topLevel tau (App s a rf e1 e2) | (usingExtension GradedBase) = do
   debugM "checkExpr[App]-gradedBase" (pretty s <> " : " <> pretty tau)
@@ -745,6 +761,15 @@ checkExpr defs gam pol _ ty@(Star demand tau) (Val s _ rf (Nec _ e)) = do
     let elaborated = Val s ty rf (Nec tau elaboratedE)
     return (gam', subst, elaborated)
 
+checkExpr defs gam pol _ ty@(Borrow demand tau) (Val s _ rf (Ref _ e)) = do
+    debugM "checkExpr[Borrow]" (pretty s <> " : " <> pretty ty)
+
+    -- Checker the expression being borrowed
+    (gam', subst, elaboratedE) <- checkExpr defs gam pol False tau e
+
+    let elaborated = Val s ty rf (Ref tau elaboratedE)
+    return (gam', subst, elaborated)
+
 -- Check a case expression
 checkExpr defs gam pol True tau (Case s _ rf guardExpr cases) = do
   debugM "checkExpr[Case]" (pretty s <> " : " <> pretty tau)
@@ -888,8 +913,9 @@ synthExpr :: (?globals :: Globals)
 
 -- Hit an unfilled hole
 synthExpr _ ctxt _ (Hole s _ _ _ _) = do
+  st <- get
   debugM "synthExpr[Hole]" (pretty s)
-  throw $ InvalidHolePosition s
+  throw $ InvalidHolePosition s ctxt (tyVarContext st)
 
 -- Literals can have their type easily synthesised
 synthExpr _ _ _ (Val s _ rf (NumInt n))  = do
@@ -912,6 +938,51 @@ synthExpr _ _ _ (Val s _ rf (StringLiteral c)) = do
   let t = TyCon $ mkId "String"
   return (t, usedGhostVariableContext, [], Val s t rf (StringLiteral c))
 
+-- Clone
+-- Pattern match on an applicable of `uniqueBind fun e`
+synthExpr defs gam pol
+   expr@(App s a rf
+     (App _ _ _
+       (Val _ _ _ (Var _ (internalName -> "uniqueBind")))
+       (Val _ _ _ (Abs _ (PVar _ _ _ var) _ body)))
+     e) = do
+  debugM "synthExpr[uniqueBind]" (pretty s <> pretty expr)
+  -- Infer the type of e (the boxed argument)
+  (ty, ghostVarCtxt, subst0, elabE) <- synthExpr defs gam pol e
+  -- Check that ty is actually a boxed type
+  case ty of
+    Box r tyA -> do
+      -- existential type for the cloned var ((exists {id : Name} . *(Rename id a))
+      idVar <- mkId <$> freshIdentifierBase "id"
+      let clonedInputTy =
+            TyExists idVar (TyCon $ mkId "Name")
+              (Borrow (TyCon $ mkId "Star") (TyApp (TyApp (TyCon $ mkId "Rename") (TyVar idVar)) tyA))
+      let clonedAssumption = (var, Linear clonedInputTy)
+
+      debugM "synthExpr[uniqueBind]body" (pretty clonedAssumption)
+      -- synthesise the type of the body for the clone
+      (tyB, ghostVarCtxt', subst1, elabBody) <- synthExpr defs (clonedAssumption : gam) pol body
+
+      let contType = FunTy Nothing Nothing (Box r tyA) tyB
+      let funType  = FunTy Nothing Nothing clonedInputTy tyB
+      let cloneType = FunTy Nothing Nothing contType funType
+      let elab = App s tyB rf
+                  (App s contType rf (Val s cloneType rf (Var cloneType $ mkId "uniqueBind"))
+                     (Val s funType rf (Abs funType (PVar s clonedInputTy rf var) Nothing elabBody))) elabE
+
+      -- Add constraints of `clone`
+      -- Constraint that 1 : s <= r
+      (semiring, subst2, _) <- synthKind s r
+      let constraint = ApproximatedBy s (TyGrade (Just semiring) 1) r semiring
+      addConstraint constraint
+      -- Cloneable constraint
+      otherTypeConstraints <- enforceConstraints s [TyApp (TyCon $ mkId "Cloneable") tyA]
+      registerWantedTypeConstraints otherTypeConstraints
+
+      substFinal <- combineSubstitutions s subst0 subst1
+      return (tyB, ghostVarCtxt <> (deleteVar var ghostVarCtxt'), substFinal, elab)
+    _ -> throw TypeError{ errLoc = s, tyExpected = Box (TyVar $ mkId "a") (TyVar $ mkId "b"), tyActual = ty }
+
 -- Secret syntactic weakening
 synthExpr defs gam pol
     (App s _ _ (Val _ _ _ (Var _ (sourceName -> "weak__"))) v@(Val _ _ _ (Var _ x))) = do
@@ -1195,7 +1266,7 @@ synthExpr defs gam pol (TryCatch s _ rf e1 p mty e2 e3) = do
 
 -- Variables
 synthExpr defs gam _ (Val s _ rf (Var _ x)) = do
-   debugM "synthExpr[Var]" (pretty s)
+   debugM ("synthExpr[Var] - " <> pretty x) (pretty s)
 
    -- Try the local context
    case lookup x gam of
@@ -1387,6 +1458,25 @@ synthExpr defs gam pol (Val s _ rf (Nec _ e)) = do
   let elaborated = Val s finalTy rf (Nec t elaboratedE)
   return (finalTy, gam', subst, elaborated)
 
+-- Infer type for references
+synthExpr defs gam pol (Val s _ rf (Ref _ e)) = do
+  debugM "synthExpr[Ref]" (pretty s)
+
+   -- Create a fresh kind variable for this permission
+  vark <- freshIdentifierBase $ "kref_[" <> pretty (startPos s) <> "]"
+   -- remember this new kind variable in the kind environment
+  modify (\st -> st { tyVarContext = (mkId vark, (kguarantee, InstanceQ)) : tyVarContext st })
+
+   -- Create a fresh permission variable for the permission of the borrowed expression
+  var <- freshTyVarInContext (mkId $ "ref_[" <> pretty (startPos s) <> "]") (tyVar vark)
+
+  -- Synth type of necessitated expression
+  (t, gam', subst, elaboratedE) <- synthExpr defs gam pol e
+
+  let finalTy = Borrow (TyVar var) t
+  let elaborated = Val s finalTy rf (Ref t elaboratedE)
+  return (finalTy, gam', subst, elaborated)
+
 -- BinOp
 synthExpr defs gam pol (Binop s _ rf op e1 e2) = do
     debugM "synthExpr[BinOp]" (pretty s)
diff --git a/frontend/src/Language/Granule/Checker/CoeffectsTypeConverter.hs b/frontend/src/Language/Granule/Checker/CoeffectsTypeConverter.hs
index 8392598f9..1d6b4e9ac 100644
--- a/frontend/src/Language/Granule/Checker/CoeffectsTypeConverter.hs
+++ b/frontend/src/Language/Granule/Checker/CoeffectsTypeConverter.hs
@@ -1,13 +1,12 @@
 {-# LANGUAGE GADTs #-}
 module Language.Granule.Checker.CoeffectsTypeConverter(includeOnlyGradeVariables, tyVarContextExistential) where
 
-import Control.Monad.Except (catchError)
 import Control.Monad.State.Strict
 import Data.Maybe(catMaybes, mapMaybe)
 
 import Language.Granule.Checker.Monad
 import Language.Granule.Checker.Predicates
-import Language.Granule.Checker.Kinding (checkKind)
+import Language.Granule.Checker.Kinding (requiresSolver)
 
 import Language.Granule.Context
 
@@ -22,9 +21,11 @@ includeOnlyGradeVariables :: (?globals :: Globals)
   => Span -> Ctxt (Type, b) -> Checker (Ctxt (Type, b))
 includeOnlyGradeVariables s xs = mapM convert xs >>= (return . catMaybes)
   where
-    convert (var, (t, q)) = (do
-      k <- checkKind s t kcoeffect <|> checkKind s t keffect
-      return $ Just (var, (t, q))) `catchError` const (return Nothing)
+    convert (var, (t, q)) = do
+      reqSolver <- requiresSolver s t
+      return $ if reqSolver
+        then Just (var, (t, q))
+        else Nothing
 
 tyVarContextExistential :: Checker (Ctxt (Type, Quantifier))
 tyVarContextExistential = do
diff --git a/frontend/src/Language/Granule/Checker/Constraints.hs b/frontend/src/Language/Granule/Checker/Constraints.hs
index d92a4c8f8..5ef390328 100644
--- a/frontend/src/Language/Granule/Checker/Constraints.hs
+++ b/frontend/src/Language/Granule/Checker/Constraints.hs
@@ -22,6 +22,7 @@ import Language.Granule.Context (Ctxt)
 
 import Language.Granule.Checker.Constraints.SymbolicGrades
 import qualified Language.Granule.Checker.Constraints.SNatX as SNatX
+import qualified Language.Granule.Checker.Constraints.SFrac as SFrac
 
 import Language.Granule.Syntax.Helpers
 import Language.Granule.Syntax.Identifiers
@@ -226,22 +227,32 @@ freshSolverVarScoped quant name (TyCon (internalName -> "Q")) q k =
 freshSolverVarScoped quant name (TyCon (internalName -> "Sec")) q k =
     quant q name (\solverVar -> k (sTrue, SSec solverVar))
 
+freshSolverVarScoped quant name (TyCon (internalName -> "Fraction")) q k = do
+   quant q name (\solverVar ->
+    k (SFrac.fractionConstraint solverVar
+     , SFraction (SFrac.SFrac solverVar)))
+
+freshSolverVarScoped quant name (TyCon (internalName -> "Star")) q k = do
+   quant q name (\solverVar ->
+    k (SFrac.fractionConstraint solverVar
+     , SFraction (SFrac.SFrac solverVar)))
+
 freshSolverVarScoped quant name (TyCon conName) q k =
-    -- Integer based
-    quant q name (\solverVar ->
-      case internalName conName of
-        "Nat"    -> k (solverVar .>= 0, SNat solverVar)
-        "Level"  -> k (solverVar .== literal privateRepresentation
-                  .|| solverVar .== literal publicRepresentation
-                  .|| solverVar .== literal unusedRepresentation
-                    , SLevel solverVar)
-        "LNL"    -> k (solverVar .== literal zeroRep
-                  .|| solverVar .== literal oneRep
-                  .|| solverVar .== literal manyRep
-                    , SLNL solverVar)
-        "OOZ"    -> k (solverVar .== 0 .|| solverVar .== 1, SOOZ (ite (solverVar .== 0) sFalse sTrue))
-        "Cartesian" -> k (sTrue, SPoint)
-        k -> solverError $ "I don't know how to make a fresh solver variable of type " <> show conName)
+      -- Integer based
+      quant q name (\solverVar ->
+        case internalName conName of
+          "Nat"    -> k (solverVar .>= 0, SNat solverVar)
+          "Level"  -> k (solverVar .== literal privateRepresentation
+                    .|| solverVar .== literal publicRepresentation
+                    .|| solverVar .== literal unusedRepresentation
+                      , SLevel solverVar)
+          "LNL"    -> k (solverVar .== literal zeroRep
+                    .|| solverVar .== literal oneRep
+                    .|| solverVar .== literal manyRep
+                      , SLNL solverVar)
+          "OOZ"    -> k (solverVar .== 0 .|| solverVar .== 1, SOOZ (ite (solverVar .== 0) sFalse sTrue))
+          "Cartesian" -> k (sTrue, SPoint)
+          k -> solverError $ "I don't know how to make a fresh solver variable of type " <> show conName)
 
 freshSolverVarScoped quant name t q k | t == extendedNat = do
    quant q name (\solverVar ->
@@ -294,6 +305,10 @@ instance QuantifiableScoped Integer where
   universalScoped v = universal [v]
   existentialScoped v = existential [v]
 
+instance QuantifiableScoped Rational where
+  universalScoped v = universal [v]
+  existentialScoped v = existential [v]
+
 instance QuantifiableScoped Bool where
   universalScoped v = universal [v]
   existentialScoped v = existential [v]
@@ -458,6 +473,12 @@ compileCoeffect (TyGrade k' n) k _ | k == extendedNat && (k' == Nothing || k' ==
 compileCoeffect (TyRational r) (TyCon k) _ | internalName k == "Q" =
   return (SFloat  . fromRational $ r, sTrue)
 
+compileCoeffect (TyFraction f) (TyCon k) _ | internalName k == "Fraction" =
+  return (SFraction (SFrac.SFrac $ fromInteger (numerator f) / fromInteger (denominator f)), sTrue)
+
+compileCoeffect (TyCon (internalName -> "Star")) (TyCon (internalName -> "Fraction")) _ = do
+  return (SFraction (SFrac.star), sTrue)
+
 compileCoeffect (TySet _ xs) (isSet -> Just (elemTy, polarity)) _ =
     return (SSet polarity . S.fromList $ mapMaybe justTyConNames xs, sTrue)
   where
@@ -557,6 +578,7 @@ compileCoeffect (TyGrade k' 1) k vars = do
         "OOZ"       -> return (SOOZ sTrue, sTrue)
         "LNL"       -> return (SLNL (literal oneRep), sTrue)
         "Cartesian" -> return (SPoint, sTrue)
+        "Fraction"  -> return (SFraction (SFrac.SFrac 1), sTrue)
         _           -> solverError $ "I don't know how to compile a 1 for " <> pretty k
 
     otherK | otherK == extendedNat ->
@@ -615,6 +637,7 @@ eqConstraint (SLevel l) (SLevel k) = return $ l .== k
 eqConstraint u@(SUnknown{}) u'@(SUnknown{}) = symGradeEq u u'
 eqConstraint (SExtNat x) (SExtNat y) = return $ x .== y
 eqConstraint SPoint SPoint           = return sTrue
+eqConstraint (SFraction f) (SFraction f') = return $ f .== f'
 
 eqConstraint (SInterval lb1 ub1) (SInterval lb2 ub2) =
   liftM2 (.&&) (eqConstraint lb1 lb2) (eqConstraint ub1 ub2)
@@ -629,6 +652,7 @@ eqConstraint x y =
 approximatedByOrEqualConstraint :: SGrade -> SGrade -> Symbolic SBool
 approximatedByOrEqualConstraint (SNat n) (SNat m)      = return $ n .== m
 approximatedByOrEqualConstraint (SFloat n) (SFloat m)  = return $ n .<= m
+approximatedByOrEqualConstraint (SFraction f) (SFraction f') = return $ f .== f'
 approximatedByOrEqualConstraint SPoint SPoint          = return $ sTrue
 approximatedByOrEqualConstraint (SOOZ s) (SOOZ r) = pure $ s .== r
 approximatedByOrEqualConstraint (SSet Normal s) (SSet Normal t) =
@@ -772,6 +796,7 @@ trivialUnsatisfiableConstraints
     neqC :: Type -> Type -> Bool
     neqC (TyInt n) (TyInt m) = n /= m
     neqC (TyRational n) (TyRational m) = n /= m
+    neqC (TyFraction f) (TyFraction f') = f /= f'
     --neqC (CInterval lb1 ub1) (CInterval lb2 ub2) =
     --   neqC lb1 lb2 || neqC ub1 ub2
     neqC (TySig r t) (TySig r' t') | t == t' = neqC r r'
diff --git a/frontend/src/Language/Granule/Checker/Constraints/Compile.hs b/frontend/src/Language/Granule/Checker/Constraints/Compile.hs
index fdd163143..7c97363da 100644
--- a/frontend/src/Language/Granule/Checker/Constraints/Compile.hs
+++ b/frontend/src/Language/Granule/Checker/Constraints/Compile.hs
@@ -62,6 +62,7 @@ compileAtType s op c1 c2 coeffTy = do
     TyOpLesserEqNat -> return $ Con (LtEq s c1 c2)
     TyOpGreaterEqNat -> return $ Con (GtEq s c1 c2)
     TyOpHsup         -> return $ Con (Hsup s c1 c2 coeffTy)
+    TyOpMutable      -> return $ Disj [(Con (Eq s c1 (TyCon (mkId $ "Star")) coeffTy)), (Con (Eq s c1 (TyFraction 1) coeffTy))]
     TyOpImpl         -> do
       p1 <- compileTypeConstraintToConstraint s c1
       p2 <- compileTypeConstraintToConstraint s c2
@@ -121,6 +122,9 @@ isDefinedConstraint s (TyApp (TyCon (internalName -> "NonInterfering")) semiring
 isDefinedConstraint s (TyApp (TyCon (internalName -> "Dropable")) typ)
   = return (dropable typ)
 
+isDefinedConstraint s (TyApp (TyCon (internalName -> "Cloneable")) typ)
+  = return (cloneable typ)
+
 isDefinedConstraint _ _
   = return False
 
@@ -170,6 +174,17 @@ exactSemiring (TyApp
                  s2) = exactSemiring s1 && exactSemiring s2
 exactSemiring _ = False
 
+cloneable :: Type -> Bool
+cloneable (TyApp
+  (TyCon (internalName -> "FloatArray")) _ ) = True
+cloneable (TyApp
+  (TyApp
+    (TyCon (internalName -> "Ref")) _) t) = cloneable t
+cloneable (TyApp
+  (TyApp
+    (TyCon (internalName -> ",")) x) y) = cloneable x && cloneable y
+cloneable _ = False
+
 nonInterfering :: Type -> Bool
 nonInterfering (TyCon (internalName -> "Level")) = True
 nonInterfering (TyCon (internalName -> "Set")) = True
@@ -184,16 +199,19 @@ dropable =
       , tfFunTy = \_ c x y -> return y
       , tfTyCon = \id -> return $ notElem id nonDropable
       , tfBox = \x y -> return (x && y)
-      , tfDiamond = \x y -> return (x && y)
-      , tfStar = \x y -> return (x && y)
+      , tfDiamond = \x y -> return $ (x && y)
+      , tfStar = \x y -> return $ (x && y)
+      , tfBorrow = \x y -> return $ (x && y)
       , tfTyVar = \_ -> return False
       , tfTyApp = \x y -> return x
       , tfTyInt = \_ -> return True
       , tfTyRational = \_ -> return True
+      , tfTyFraction = \_ -> return True
       , tfTyGrade = \_ _ -> return True
       , tfTyInfix = \_ x y -> return (x && y)
       , tfSet = \_ _ -> return  True
       , tfTyCase = \_ _ -> return False
       , tfTySig = \t _ _ -> return t
       , tfTyExists = \_ _ x -> return x
-      , tfTyForall = \_ _ x -> return x })
+      , tfTyForall = \_ _ x -> return x
+      , tfTyName = \_ -> return False })
diff --git a/frontend/src/Language/Granule/Checker/Constraints/SFrac.hs b/frontend/src/Language/Granule/Checker/Constraints/SFrac.hs
new file mode 100644
index 000000000..46ffa68d4
--- /dev/null
+++ b/frontend/src/Language/Granule/Checker/Constraints/SFrac.hs
@@ -0,0 +1,65 @@
+{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+
+{-# LANGUAGE DeriveAnyClass  #-}
+{-# LANGUAGE DeriveGeneric   #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+-- | Represents fractions with star in the solver
+module Language.Granule.Checker.Constraints.SFrac where
+
+-- import Control.Monad ((<=<))
+import Data.SBV
+import GHC.Generics (Generic)
+
+newtype SFrac = SFrac { fVal  :: SFloat }
+  deriving (Generic, Mergeable)
+
+instance Show SFrac where
+  show (SFrac val) = case unliteral val of
+    Just (0) -> "*"
+    Just f    -> show f
+    _         -> "<symbolic>"
+
+star :: SFrac
+star = SFrac $ (literal (0))
+
+isUniq :: SFrac -> SBool
+isUniq (SFrac f) = f .== 0
+
+instance Num SFrac where
+  x + y = ite (isUniq x .|| isUniq y)
+              star
+              (SFrac (fVal x + fVal y))
+  x * y = ite (isUniq x .|| isUniq y)
+              star
+              (SFrac (fVal x * fVal y))
+  x - y = ite (isUniq x .|| isUniq y)
+              star
+              (SFrac (fVal x - fVal y))
+
+instance EqSymbolic SFrac where
+  (SFrac a) .== (SFrac b) = a .== b
+
+instance OrdSymbolic SFrac where
+  (SFrac a) .< (SFrac b) = a .== b
+
+fractionConstraint :: SFloat -> SBool
+fractionConstraint v = v .== v .&& v .<= 1 .&& v .>= 0
+
+freeSFrac :: String -> Symbolic SFrac
+freeSFrac nm = do
+  v <- sFloat $ nm <> "_fVal"
+  constrain $ fractionConstraint v
+  return $ SFrac v
+
+existsSFrac :: String -> Symbolic SFrac
+existsSFrac nm = do
+  v <- sbvExists $ nm <> "_fVal"
+  constrain $ fractionConstraint v
+  return $ SFrac v
+
+forallSFrac :: String -> Symbolic SFrac
+forallSFrac nm = do
+  v <- sbvForall $ nm <> "_fVal"
+  constrain $ fractionConstraint v
+  return $ SFrac v
\ No newline at end of file
diff --git a/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs b/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
index 9f1c3dbf4..a73267770 100644
--- a/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
+++ b/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
@@ -6,6 +6,7 @@
 module Language.Granule.Checker.Constraints.SymbolicGrades where
 
 import Language.Granule.Checker.Constraints.SNatX
+import Language.Granule.Checker.Constraints.SFrac
 import Language.Granule.Syntax.Type
 
 import Data.Functor.Identity
@@ -25,6 +26,7 @@ solverError msg = liftIO $ throwIO . ErrorCall $ msg
 -- Symbolic grades, for coeffects and indices
 data SGrade =
        SNat      SInteger
+     | SFraction { sFraction :: SFrac }
      | SFloat    SFloat
      | SLevel    SInteger
      | SSec      SBool -- Hi = True, Lo = False
@@ -135,6 +137,7 @@ sLtTree _ _ = return sFalse
 match :: SGrade -> SGrade -> Bool
 match (SNat _) (SNat _) = True
 match (SFloat _) (SFloat _) = True
+match (SFraction _) (SFraction _) = True
 match (SLevel _) (SLevel _) = True
 match (SSet p _) (SSet p' _) | p == p' = True
 match (SExtNat _) (SExtNat _) = True
@@ -184,6 +187,7 @@ natLike _ = False
 instance Mergeable SGrade where
   symbolicMerge s sb (SNat n) (SNat n') = SNat (symbolicMerge s sb n n')
   symbolicMerge s sb (SFloat n) (SFloat n') = SFloat (symbolicMerge s sb n n')
+  symbolicMerge s sb (SFraction f) (SFraction f') = SFraction (symbolicMerge s sb f f')
   symbolicMerge s sb (SLevel n) (SLevel n') = SLevel (symbolicMerge s sb n n')
   symbolicMerge s sb (SSet _ n) (SSet _ n') = error "Can't symbolic merge sets yet"
   symbolicMerge s sb (SExtNat n) (SExtNat n') = SExtNat (symbolicMerge s sb n n')
@@ -211,6 +215,8 @@ symGradeLess (SInterval lb1 ub1) (SInterval lb2 ub2) =
 
 symGradeLess (SNat n) (SNat n')     = return $ n .< n'
 symGradeLess (SFloat n) (SFloat n') = return $ n .< n'
+symGradeLess (SFraction f) (SFraction f') = return $ f .< f'
+
 symGradeLess (SLevel n) (SLevel n') =
   -- Using the ordering from the Agda code (by cases)
   return $ ltCase dunnoRepresentation   publicRepresentation  -- DunnoPub
@@ -267,6 +273,8 @@ symGradeEq (SInterval lb1 ub1) (SInterval lb2 ub2) =
 
 symGradeEq (SNat n) (SNat n')     = return $ n .== n'
 symGradeEq (SFloat n) (SFloat n') = return $ n .== n'
+symGradeEq (SFraction f) (SFraction f') = return $ f .== f'
+
 symGradeEq (SLevel n) (SLevel n') = return $ n .== n'
 symGradeEq (SSet p n) (SSet p' n') | p == p' = return $ n .== n'
 
@@ -312,6 +320,8 @@ symGradeMeet (SLevel s) (SLevel t) =
                         (literal dunnoRepresentation)
                   $ literal publicRepresentation -- join Public Public = Public
 symGradeMeet (SFloat n1) (SFloat n2) = return $ SFloat $ n1 `smin` n2
+symGradeMeet (SFraction f) (SFraction f') = return $ SFraction $
+  ite (isUniq f) f' (ite (isUniq f') f (SFrac (fVal f `smin` fVal f')))
 symGradeMeet (SExtNat x) (SExtNat y) = return $ SExtNat $
   ite (isInf x) y (ite (isInf y) x (SNatX (xVal x `smin` xVal y)))
 symGradeMeet (SInterval lb1 ub1) (SInterval lb2 ub2) =
@@ -348,6 +358,8 @@ symGradeJoin (SLevel s) (SLevel t) =
                         (literal privateRepresentation)
                   $ literal dunnoRepresentation -- meet Dunno Private = meet Private Dunno = meet Dunno Dunno = Dunno
 symGradeJoin (SFloat n1) (SFloat n2) = return $ SFloat (n1 `smax` n2)
+symGradeJoin (SFraction f) (SFraction f') = return $ SFraction $
+  ite (isUniq f .|| isUniq f') star (SFrac (fVal f `smax` fVal f'))
 symGradeJoin (SExtNat x) (SExtNat y) = return $ SExtNat $
   ite (isInf x .|| isInf y) inf (SNatX (xVal x `smax` xVal y))
 symGradeJoin (SInterval lb1 ub1) (SInterval lb2 ub2) =
@@ -387,6 +399,7 @@ symGradePlus (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.intersec
 symGradePlus (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
 symGradePlus (SLevel lev1) (SLevel lev2) = symGradeJoin (SLevel lev1) (SLevel lev2)
 symGradePlus (SFloat n1) (SFloat n2) = return $ SFloat $ n1 + n2
+symGradePlus (SFraction f) (SFraction f') = return $ SFraction (f + f')
 symGradePlus (SExtNat x) (SExtNat y) = return $ SExtNat (x + y)
 symGradePlus (SInterval lb1 ub1) (SInterval lb2 ub2) =
     liftM2 SInterval (lb1 `symGradePlus` lb2) (ub1 `symGradePlus` ub2)
@@ -436,6 +449,7 @@ symGradeTimes (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.union s
 symGradeTimes (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
 symGradeTimes (SLevel lev1) (SLevel lev2) = symGradeJoin (SLevel lev1) (SLevel lev2)
 symGradeTimes (SFloat n1) (SFloat n2) = return $ SFloat $ n1 * n2
+symGradeTimes (SFraction f) (SFraction f') = return $ SFraction (f * f')
 symGradeTimes (SExtNat x) (SExtNat y) = return $ SExtNat (x * y)
 symGradeTimes (SOOZ s) (SOOZ r) = pure . SOOZ $ s .&& r
 
@@ -493,6 +507,7 @@ symGradeTimes s t = solverError $ cannotDo "times" s t
 -- | (OPTIONAL)
 symGradeMinus :: SGrade -> SGrade -> Symbolic SGrade
 symGradeMinus (SNat n1) (SNat n2) = return $ SNat $ ite (n1 .< n2) 0 (n1 - n2)
+symGradeMinus (SFraction f) (SFraction f') = return $ SFraction (f - f')
 symGradeMinus (SSet p s) (SSet p' t) | p == p' = return $ SSet p (s S.\\ t)
 symGradeMinus (SExtNat x) (SExtNat y) = return $ SExtNat (x - y)
 symGradeMinus (SInterval lb1 ub1) (SInterval lb2 ub2) =
diff --git a/frontend/src/Language/Granule/Checker/Kinding.hs b/frontend/src/Language/Granule/Checker/Kinding.hs
index 587e64749..850937316 100644
--- a/frontend/src/Language/Granule/Checker/Kinding.hs
+++ b/frontend/src/Language/Granule/Checker/Kinding.hs
@@ -173,6 +173,11 @@ checkKind s t@(TyInt n) k =
     -- Not valid
     _ -> throw $ NaturalNumberAtWrongKind s t k
 
+checkKind s t@(TyName n) k =
+  case k of
+    TyCon (internalName -> "Name") -> return ([], t)
+    _ -> throw $ NaturalNumberAtWrongKind s t k
+
 -- KChk_effOne
 checkKind s t@(TyGrade mk n) k = do
   let k' = fromMaybe k mk
@@ -361,6 +366,9 @@ synthKindWithConfiguration s config t@(TyInfix op t1 t2) =
 synthKindWithConfiguration s _ t@(TyInt n) = do
   return (TyCon (Id "Nat" "Nat"), [], t)
 
+synthKindWithConfiguration s _ t@(TyName n) = do
+  return (TyCon (Id "Name" "Name"), [], t)
+
 -- KChkS_grade [with type already resolved]
 synthKindWithConfiguration s config t@(TyGrade (Just k) n) =
   return (k, [], t)
@@ -402,6 +410,13 @@ synthKindWithConfiguration s _ (Star g t) = do
   subst <- combineManySubstitutions s [subst0, subst1, subst2]
   return (ktype, subst, Star g' t')
 
+synthKindWithConfiguration s _ (Borrow p t) = do
+  (permissionTy, subst0, p') <- synthKindWithConfiguration s (defaultResolutionBehaviour p) p
+  (subst1, _) <- checkKind s permissionTy kpermission
+  (subst2, t') <- checkKind s t ktype
+  subst <- combineManySubstitutions s [subst0, subst1, subst2]
+  return (ktype, subst, Borrow p' t')
+
 synthKindWithConfiguration s _ t@(TyCon (internalName -> "Pure")) = do
   -- Create a fresh type variable
   var <- freshTyVarInContext (mkId $ "eff[" <> pretty (startPos s) <> "]") keffect
@@ -495,6 +510,8 @@ synthKindWithConfiguration s config t@(TyForall x k ty) = do
   registerTyVarInContextWith' x k ForallQ $ do
        (kind, subst, elabTy) <- synthKindWithConfiguration s config ty
        return (kind, subst, TyForall x k elabTy)
+synthKindWithConfiguration s config t@(TyFraction _) = do
+  return (TyCon $ mkId "Fraction", [], t)
 
 synthKindWithConfiguration s _ t =
   throw ImpossibleKindSynthesis { errLoc = s, errTy = t }
@@ -562,8 +579,16 @@ closedOperatorAtKind s TyOpTimes t = do
       -- If not, see if the type is an effect
       (result', putChecker') <- peekChecker (checkKind s t keffect)
       case result' of
-        -- Not a closed operator at this kind
-        Left  _ -> return Nothing
+        -- If not, see if the type is a permission
+        Left _ -> do
+          (result'', putChecker'') <- peekChecker (checkKind s t kpermission)
+          case result'' of
+            -- Not a closed operator at this kind
+            Left _ -> return Nothing
+            -- Yes it is a permission
+            Right (subst, _) -> do
+              putChecker''
+              return $ Just subst
         -- Yes it is an effect type
         Right (subst, _) -> do
           putChecker'
@@ -573,6 +598,26 @@ closedOperatorAtKind s TyOpTimes t = do
       putChecker
       return $ Just subst
 
+-- + case
+closedOperatorAtKind s TyOpPlus t = do
+  -- See if the type is a coeffect
+  (result, putChecker) <- peekChecker (checkKind s t kcoeffect)
+  case result of
+    Left _ -> do
+      -- If not, see if the type is a permission
+      (result', putChecker') <- peekChecker (checkKind s t kpermission)
+      case result' of
+        -- Not a closed operator at this kind
+        Left _ -> return Nothing
+        -- Yes it is a permission
+        Right (subst, _) -> do
+          putChecker'
+          return $ Just subst
+    -- Yes it is a coeffect type
+    Right (subst, _) -> do
+      putChecker
+      return $ Just subst
+
 -- Any other "coeffect operators" case
 closedOperatorAtKind s op t | coeffectResourceAlgebraOps op = do
   -- See if the type is a coeffect
@@ -596,7 +641,13 @@ predicateOperatorAtKind :: (?globals :: Globals) =>
 predicateOperatorAtKind s op t | predicateOperation op = do
   (result, putChecker) <- peekChecker (checkKind s t kcoeffect)
   case result of
-    Left _ -> return Nothing
+    Left _ -> do
+      (result', putChecker') <- peekChecker (checkKind s t kpermission)
+      case result' of
+        Left _ -> return Nothing
+        Right (subst', _) -> do
+          putChecker
+          return $ Just subst'
     Right (subst, _) -> do
       putChecker
       return $ Just subst
@@ -1225,7 +1276,7 @@ unify x y = runMaybeT $ unify' x y
 
 requiresSolver :: (?globals :: Globals) => Span -> Type -> Checker Bool
 requiresSolver s ty = do
-  (result, putChecker) <- peekChecker (checkKind s ty kcoeffect <|> checkKind s ty keffect)
+  (result, putChecker) <- peekChecker (checkKind s ty kcoeffect <|> checkKind s ty keffect <|> checkKind s ty kpermission)
   case result of
     -- Checking as coeffect or effect caused an error so ignore
     Left _  -> return False
@@ -1282,6 +1333,16 @@ instance Unifiable Type where
       u' <- unify' k k'
       lift $ combineSubstitutionsHere u u'
 
+    unify' (Borrow p t) (Borrow p' t') = do
+      u  <- unify' p p'
+      u' <- unify' t t'
+      lift $ combineSubstitutionsHere u u'
+
+    unify' (Star g t) (Star g' t') = do
+      u  <- unify' g g'
+      u' <- unify' t t'
+      lift $ combineSubstitutionsHere u u'
+
     -- No unification
     unify' t t' = do
       -- But try to generate a constraint if its a solver thing
diff --git a/frontend/src/Language/Granule/Checker/Monad.hs b/frontend/src/Language/Granule/Checker/Monad.hs
index d9cd22c2c..3d3a05e9a 100644
--- a/frontend/src/Language/Granule/Checker/Monad.hs
+++ b/frontend/src/Language/Granule/Checker/Monad.hs
@@ -671,7 +671,7 @@ data CheckerError
   | InvalidTypeDefinition
     { errLoc :: Span, errTy :: Type }
   | InvalidHolePosition
-    { errLoc :: Span }
+    { errLoc :: Span, context :: Ctxt Assumption, tyContext :: Ctxt (Type, Quantifier) }
   | UnknownResourceAlgebra
     { errLoc :: Span, errTy :: Type, errK :: Kind }
   | CaseOnIndexedType
@@ -709,7 +709,7 @@ instance UserMsg CheckerError where
   title KindsNotEqual{} = "Kind error"
   title IntervalGradeKindError{} = "Interval kind error"
   title LinearityError{} = "Linearity error"
-  title UniquenessError{} = "Uniqueness error"
+  title UniquenessError{} = "Ownership error"
   title UnpromotableError{} = "Unpromotable error"
   title PatternTypingError{} = "Pattern typing error"
   title PatternTypingMismatch{} = "Pattern typing mismatch"
@@ -776,7 +776,7 @@ instance UserMsg CheckerError where
     -- Print the context if there is anything to use
     (if null context
       then ""
-      else "\n\n   Context:" <> concatMap (\x -> "\n     " ++ pretty x) context)
+      else "\n\n   Context:" <> concatMap (\x -> "\n     " ++ pretty x) (nubContext context))
     <>
     (if null tyContext
       then ""
@@ -860,8 +860,8 @@ instance UserMsg CheckerError where
       "Linearity of Handler clauses does not match"
 
   msg UniquenessError{..} = case uniquenessMismatch of
-    NonUniqueUsedUniquely t ->
-      "Cannot guarantee uniqueness of reference to value of type `" <> pretty t <> "`."
+    NonUniqueUsedUniquely t1 t2 ->
+      "Cannot guarantee usage of reference to value of type `" <> pretty t1 <> "` at permission `" <> pretty t2 <> "`."
     UniquePromotion t ->
       "Cannot promote non-unique value of type `" <> pretty t <> "` to unique, since uniqueness is not a coeffect."
 
@@ -1072,7 +1072,19 @@ instance UserMsg CheckerError where
   msg InvalidTypeDefinition{ errTy }
     = "The type `" <> pretty errTy <> "` is not valid in a datatype definition."
 
-  msg InvalidHolePosition{} = "Hole occurs in synthesis position so the type is not yet known"
+  msg InvalidHolePosition{ errLoc , context , tyContext } = "Hole occurs in synthesis position so the type is not yet known"
+    <>
+    -- Print the context if there is anything to use
+    (if null context
+      then ""
+      else "\n\n   Context:" <> concatMap (\x -> "\n     " ++ pretty x) (nubContext context))
+    <>
+    (if null tyContext
+      then ""
+      else "\n\n   Type context:" <> concatMap (\(v, (t , _)) ->  "\n     "
+                                                <> pretty v
+                                                <> " : " <> pretty t) tyContext)
+
 
   msg UnknownResourceAlgebra{ errK, errTy }
     = "There is no resource algebra defined for `" <> pretty errK <> "`, arising from effect term `" <> pretty errTy <> "`"
@@ -1121,7 +1133,7 @@ data LinearityMismatch
   deriving (Eq, Show) -- for debugging
 
 data UniquenessMismatch
-  = NonUniqueUsedUniquely Type
+  = NonUniqueUsedUniquely Type Type
   | UniquePromotion Type
   deriving (Eq, Show)
 
diff --git a/frontend/src/Language/Granule/Checker/Predicates.hs b/frontend/src/Language/Granule/Checker/Predicates.hs
index 6dd0d77a8..9eff1e2fa 100644
--- a/frontend/src/Language/Granule/Checker/Predicates.hs
+++ b/frontend/src/Language/Granule/Checker/Predicates.hs
@@ -49,6 +49,7 @@ data Constraint =
     Eq  Span Type Type Type
   | Neq Span Type Type Type
   | ApproximatedBy Span Type Type Type
+  -- last argument is the kind of the coeffect
 
   -- (Least) upper bound; the last argument controls whether
   -- we do a check for leastness of the third argument (True) or not (False)
diff --git a/frontend/src/Language/Granule/Checker/Primitives.hs b/frontend/src/Language/Granule/Checker/Primitives.hs
index 232dd4a9b..62dfbdbde 100644
--- a/frontend/src/Language/Granule/Checker/Primitives.hs
+++ b/frontend/src/Language/Granule/Checker/Primitives.hs
@@ -58,10 +58,11 @@ typeConstructors =
                                        , (mkId "Dunno",    (tyCon "Level", [], []))])] []
  ++
   -- Everything else is always in scope
-    [ (mkId "Coeffect",  (Type 2, [], []))
-    , (mkId "Effect",    (Type 2, [], []))
-    , (mkId "Guarantee", (Type 2, [], []))
-    , (mkId "Predicate", (Type 2, [], []))
+    [ (mkId "Coeffect",  (Type 0, [], []))
+    , (mkId "Effect",    (Type 0, [], []))
+    , (mkId "Guarantee", (Type 0, [], []))
+    , (mkId "Permission", (Type 0, [], []))
+    , (mkId "Predicate", (Type 0, [], []))
     , (mkId "->",     (funTy (Type 0) (funTy (Type 0) (Type 0)), [], []))
     , (mkId ",,",     (funTy kcoeffect (funTy kcoeffect kcoeffect), [mkId ",,"], []))
     , (mkId "Int",    (Type 0, [], []))
@@ -75,15 +76,17 @@ typeConstructors =
     , (mkId "Dropable", (funTy (Type 0) kpredicate, [], [0]))
     -- TODO: add deriving for this
     -- , (mkId "Moveable", (funTy (Type 0) kpredicate, [], [0]))
+    , (mkId "Cloneable", (funTy (Type 0) kpredicate, [], [0]))
     -- Session type related things
     , (mkId "ExactSemiring", (funTy (tyCon "Semiring") (tyCon "Predicate"), [], []))
+    , (mkId "Mutable", (funTy (tyCon "Fraction") (tyCon "Predicate"), [], []))
     , (mkId "NonInterfering", (funTy (tyCon "Coeffect") (tyCon "Predicate"), [], []))
     , (mkId "Protocol", (Type 0, [], []))
     , (mkId "SingleAction", (funTy (tyCon "Protocol") (tyCon "Predicate"), [], [0]))
     , (mkId "ReceivePrefix", (funTy (tyCon "Protocol") (tyCon "Predicate"), [], [0]))
     , (mkId "Sends", (funTy (tyCon "Nat") (funTy (tyCon "Protocol") (tyCon "Predicate")), [], [0]))
     , (mkId "Graded", (funTy (tyCon "Nat") (funTy (tyCon "Protocol") (tyCon "Protocol")), [], [0]))
-
+    , (mkId "Rename", (funTy (tyCon "Name") (funTy (Type 0) (Type 0)), [], [0]))
     -- # Coeffect types
     , (mkId "Nat",      (kcoeffect, [], []))
     , (mkId "Q",        (kcoeffect, [], [])) -- Rationals
@@ -112,6 +115,8 @@ typeConstructors =
     -- Uniqueness
     , (mkId "Uniqueness", (kguarantee, [], []))
     , (mkId "Unique", (tyCon "Uniqueness", [], []))
+    , (mkId "Fraction", (tyCon "Permission", [], []))
+    , (mkId "Star", (tyCon "Fraction", [], []))
     -- Integrity
     , (mkId "Integrity", (kguarantee, [], []))
     , (mkId "Trusted", (tyCon "Integrity", [], []))
@@ -147,8 +152,10 @@ typeConstructors =
             (FunTy (Just $ mkId "sig") Nothing (funTy (tyVar "eff") (funTy (Type 0) (Type 0)))
               (funTy (tyVar "eff") (TyApp (TyApp (tyCon "GradedFree") (tyVar "eff")) (tyVar "sig")))), [], [0,1]))
 
-    -- Arrays
-    , (mkId "FloatArray", (Type 0, [], []))
+    -- Reference types
+    , (mkId "Name", (FunTy Nothing Nothing (Type 0) (Type 0), [], []))
+    , (mkId "FloatArray", (FunTy Nothing Nothing (TyCon $ mkId "Name") (Type 0), [], []))
+    , (mkId "Ref",  (FunTy Nothing Nothing (TyCon $ mkId "Name") (FunTy Nothing Nothing (Type 0) (Type 0)), [], []))
 
     -- Capability related things
     , (mkId "CapabilityType", (funTy (tyCon "Capability") (Type 0), [], [0]))
@@ -200,6 +207,7 @@ tyOps = \case
     TyOpConverge -> (kNat, kNat, kNat)
     TyOpImpl    -> (kpredicate, kpredicate, kpredicate)
     TyOpHsup    -> (tyVar "k", tyVar "k", kpredicate)
+    TyOpMutable    -> (tyVar "k", tyVar "k", kpredicate)
 
 dataTypes :: [DataDecl]
 dataTypes =
@@ -653,24 +661,17 @@ tick = BUILTIN
 --------------------------------------------------------------------------------
 
 uniqueReturn
-  : forall {a : Type}
-  . *a -> !a
+  : forall {a : Type, s : Semiring, r : s}
+  . *a -> a [r]
 uniqueReturn = BUILTIN
 
-uniqueBind
-  : forall {a b : Type}
-  . (*a -> !b) -> !a -> !b
-uniqueBind = BUILTIN
+-- Provided by clone
 
-uniquePush
-  : forall {a b : Type}
-  . *(a, b)  -> (*a, *b)
-uniquePush = BUILTIN
-
-uniquePull
-  : forall {a b : Type}
-  . (*a, *b) -> *(a, b)
-uniquePull = BUILTIN
+-- uniqueBind
+--   : forall {a b : Type, s : Semiring, r : s}
+--   . {(1 : s) <= r, Cloneable a}
+--  => ((exists {id : Name} . *(Rename id a)) -> b) -> a [r] -> b
+-- uniqueBind = BUILTIN
 
 reveal
   : forall {a : Type}
@@ -682,39 +683,76 @@ trustedBind
   . (a *{Trusted} -> b [Lo]) -> a [Lo] -> b [Lo]
 trustedBind = BUILTIN
 
+withBorrow
+  : forall {a b : Type}
+  . (& 1 a -> & 1 b) -> *a -> *b
+withBorrow = BUILTIN
+
+split
+  : forall {a : Type, f : Fraction}
+  . {f /= Star} => & f a -> (& (f * 1/2) a, & (f * 1/2) a)
+split = BUILTIN
+
+join
+  : forall {a : Type, f g : Fraction}
+  . {f /= Star, g /= Star} => (& f a, & g a) -> & (f+g) a
+join = BUILTIN
+
+borrowPush
+  : forall {a b : Type, p : Permission, f : p}
+  . & f (a, b) -> (& f a, & f b)
+borrowPush = BUILTIN
+
+borrowPull
+  : forall {a b : Type, p : Permission, f : p}
+  . (& f a, & f b) -> & f (a, b)
+borrowPull = BUILTIN
+
 --------------------------------------------------------------------------------
 --- # Mutable array operations
 --------------------------------------------------------------------------------
 
-newFloatArray : Int -> *FloatArray
+newFloatArray : Int -> exists {id : Name} . *(FloatArray id)
 newFloatArray = BUILTIN
 
-readFloatArray : *FloatArray -> Int -> (Float, *FloatArray)
+readFloatArray : forall {p : Permission, f : p, id : Name} . & f (FloatArray id) -> Int -> (Float, & f (FloatArray id))
 readFloatArray = BUILTIN
 
-writeFloatArray : *FloatArray -> Int -> Float -> *FloatArray
+writeFloatArray : forall {id : Name, f : Fraction} . {mut f} => & f (FloatArray id) -> Int -> Float -> & f (FloatArray id)
 writeFloatArray = BUILTIN
 
-lengthFloatArray : *FloatArray -> (Int, *FloatArray)
+lengthFloatArray : forall {p : Permission, f : p, id : Name} . & f (FloatArray id) -> (!Int, & f (FloatArray id))
 lengthFloatArray = BUILTIN
 
-deleteFloatArray : *FloatArray -> ()
+deleteFloatArray : forall {id : Name} . *(FloatArray id) -> ()
 deleteFloatArray = BUILTIN
 
+newRef : forall {a : Type} . a -> exists {id : Name} . *(Ref id a)
+newRef = BUILTIN
+
+swapRef : forall {a : Type, f : Fraction, id : Name} . {mut f} => & f (Ref id a) -> a -> (a, & f (Ref id a))
+swapRef = BUILTIN
+
+freezeRef : forall {a : Type, id : Name} . *(Ref id a) -> a
+freezeRef = BUILTIN
+
+readRef : forall {a : Type, s : Semiring, q r : s, p : Permission, f : p, id : Name} . & f (Ref id (a [q+r])) -> (a [q], & f (Ref id (a [r])))
+readRef = BUILTIN
+
 --------------------------------------------------------------------------------
 --- # Imuutable array operations
 --------------------------------------------------------------------------------
 
-newFloatArrayI : Int -> FloatArray
+newFloatArrayI : forall {id : Name} . Int -> (FloatArray id)
 newFloatArrayI = BUILTIN
 
-readFloatArrayI : FloatArray -> Int -> (Float, FloatArray)
+readFloatArrayI : forall {id : Name} . (FloatArray id) -> Int -> (Float, (FloatArray id))
 readFloatArrayI = BUILTIN
 
-writeFloatArrayI : FloatArray -> Int -> Float -> FloatArray
+writeFloatArrayI : forall {id : Name} . (FloatArray id) -> Int -> Float -> (FloatArray id)
 writeFloatArrayI = BUILTIN
 
-lengthFloatArrayI : FloatArray -> (Int, FloatArray)
+lengthFloatArrayI : forall {id : Name} . (FloatArray id) -> (Int, (FloatArray id))
 lengthFloatArrayI = BUILTIN
 
 --------------------------------------------------------------------------------
@@ -773,6 +811,7 @@ drop = BUILTIN
 
 copyShape : forall {a : Type, f : Type -> Type} . f a -> (f (), f a)
 copyShape = BUILTIN
+
 |]
 
 
@@ -793,4 +832,4 @@ builtins :: [(Id, TypeScheme)]
 
 -- List of primitives that can't be promoted in CBV
 unpromotables :: [String]
-unpromotables = ["newFloatArray", "forkLinear", "forkMulticast", "forkReplicate", "forkReplicateExactly"]
+unpromotables = ["newFloatArray", "newRef", "forkLinear", "forkMulticast", "forkReplicate", "forkReplicateExactly"]
diff --git a/frontend/src/Language/Granule/Checker/SubstitutionContexts.hs b/frontend/src/Language/Granule/Checker/SubstitutionContexts.hs
index 803562090..258e0066d 100644
--- a/frontend/src/Language/Granule/Checker/SubstitutionContexts.hs
+++ b/frontend/src/Language/Granule/Checker/SubstitutionContexts.hs
@@ -24,6 +24,9 @@ newtype Substitutors =
     SubstT  Type
   deriving (Eq, Show)
 
+instance Pretty Substitutors where
+  pretty (SubstT t) = pretty t
+
 instance {-# OVERLAPS #-} Pretty (Ctxt Substitutors) where
   pretty = (intercalate " | ") . (map prettyCoerce)
     where
diff --git a/frontend/src/Language/Granule/Checker/Types.hs b/frontend/src/Language/Granule/Checker/Types.hs
index 0369f6c45..04273deef 100644
--- a/frontend/src/Language/Granule/Checker/Types.hs
+++ b/frontend/src/Language/Granule/Checker/Types.hs
@@ -57,7 +57,7 @@ equalTypes s = equalTypesRelatedCoeffectsAndUnify s Eq SndIsSpec
 data SpecIndicator = FstIsSpec | SndIsSpec | PatternCtxt
   deriving (Eq, Show)
 
-data Mode = Types | Effects deriving Show
+data Mode = Types | Effects | Permissions deriving Show
 
 -- Abstracted equality/relation on grades
 relGrades :: (?globals :: Globals)
@@ -228,6 +228,38 @@ equalTypesRelatedCoeffectsInner s rel x@(Box c t) y@(Box c' t') k sp Types = do
   substU <- combineManySubstitutions s [subst, subst']
   return (eq, substU)
 
+-- ## UNIQUENESS TYPES
+
+equalTypesRelatedCoeffectsInner s rel (Star g1 t1) (Star g2 t2) _ sp mode = do
+  debugM "equalTypesRelatedCoeffectsInner (star)" $ "grades " <> show g1 <> " and " <> show g2
+  (eq, unif)      <- equalTypesRelatedCoeffects s rel t1 t2 sp mode
+  (eq', _, unif') <- equalTypes s g1 g2
+  u <- combineSubstitutions s unif unif'
+  return (eq && eq', u)
+
+equalTypesRelatedCoeffectsInner s rel (Borrow p1 t1) (Borrow p2 t2) _ sp Types = do
+  debugM "equalTypesRelatedCoeffectsInner (borrow)" $ "grades " <> show p1 <> " and " <> show p2
+  (eq, unif) <- equalTypesRelatedCoeffects s rel t1 t2 sp Types
+  debugM "equalTypesRelatedCoeffectsInner (borrow)" $ "unif = " <> pretty unif
+  (eq', unif') <- equalTypesRelatedCoeffects s rel (normalise p1) (normalise p2) sp Permissions
+  u <- combineSubstitutions s unif unif'
+  return (eq && eq', u)
+
+
+equalTypesRelatedCoeffectsInner s rel t0@(TyApp (TyApp (TyCon d) name) t) t' ind sp mode
+  | internalName d == "Rename" = do
+    debugM "RenameL" (pretty t <> " = " <> pretty t')
+    eqRenameFunction s rel name t t' sp
+
+equalTypesRelatedCoeffectsInner s rel t' t0@(TyApp (TyApp (TyCon d) name) t) ind sp mode
+  | internalName d == "Rename" = do
+    debugM "RenameR" (pretty t <> " = " <> pretty t')
+    eqRenameFunction s rel name t t' sp
+
+-- ## GENERAL EQUALITY
+
+-- Equality with variables
+
 equalTypesRelatedCoeffectsInner s rel ty1@(TyVar var1) ty2 kind _ _ = do
   useSolver <- requiresSolver s kind
   reportM ("Equality between " <> pretty ty1 <> " and " <> pretty ty2)
@@ -245,24 +277,7 @@ equalTypesRelatedCoeffectsInner s rel ty1 (TyVar var2) kind sp mode =
   -- Use the case above since it is symmetric
   equalTypesRelatedCoeffectsInner s rel (TyVar var2) ty1 kind sp mode
 
--- ## UNIQUNESS TYPES
-
-equalTypesRelatedCoeffectsInner s rel (Star g1 t1) (Star g2 t2) _ sp mode = do
-  (eq, unif)      <- equalTypesRelatedCoeffects s rel t1 t2 sp mode
-  (eq', _, unif') <- equalTypes s g1 g2
-  u <- combineSubstitutions s unif unif'
-  return (eq && eq', u)
-
-equalTypesRelatedCoeffectsInner s rel (Star g1 t1) t2 _ sp mode
-  | t1 == t2 = throw $ UniquenessError { errLoc = s, uniquenessMismatch = NonUniqueUsedUniquely t2}
-  | otherwise = do
-    (g, _, u) <- equalTypes s t1 t2
-    return (g, u)
-
-equalTypesRelatedCoeffectsInner s rel t1 (Star g2 t2) k sp mode =
-  equalTypesRelatedCoeffectsInner s rel (Star g2 t2) t1 k (flipIndicator sp) mode
-
--- ## SESSION TYPES
+-- -- ## SESSION TYPES
 -- Duality is idempotent (left)
 equalTypesRelatedCoeffectsInner s rel (TyApp (TyCon d') (TyApp (TyCon d) t)) t' k sp mode
   | internalName d == "Dual" && internalName d' == "Dual" =
@@ -289,8 +304,6 @@ equalTypesRelatedCoeffectsInner s rel t' t0@(TyApp (TyApp (TyCon d) grd) t) ind
   | internalName d == "Graded" = do
     eqGradedProtocolFunction s rel grd t t' sp
 
--- ## GENERAL EQUALITY
-
 -- Equality on existential types
 equalTypesRelatedCoeffectsInner s rel a@(TyExists x1 k1 t1) b@(TyExists x2 k2 t2) ind sp mode = do
   debugM "Compare existentials for equality" (pretty a <> " = " <> pretty b)
@@ -301,7 +314,9 @@ equalTypesRelatedCoeffectsInner s rel a@(TyExists x1 k1 t1) b@(TyExists x2 k2 t2
   registerTyVarInContextWith' x1 k1 ForallQ $ do
       (eqT, subst2) <- equalTypesRelatedCoeffectsInner s rel t1 t2' ind sp mode
       substFinal <- combineSubstitutions s subst1 subst2
-      return (eqK && eqT, substFinal)
+      -- remove from substFinal any substitutions which contain a use of x1 in their substituted type
+      let substFinal' = filter (\(x, SubstT t) -> not $ x1 `elem` freeVars t) substFinal
+      return (eqK && eqT, substFinal')
 
 -- Equality on rank-N forall types
 equalTypesRelatedCoeffectsInner s rel a@(TyForall x1 k1 t1) b@(TyForall x2 k2 t2) ind sp mode = do
@@ -377,6 +392,15 @@ equalTypesRelatedCoeffectsInner s rel t1 t2 k sp mode = do
           return (eq, [])
         Left _ -> throw $ KindMismatch s Nothing keffect k
 
+    Permissions -> do
+      (result, putChecker) <- peekChecker (checkKind s k kpermission)
+      case result of
+        Right res -> do
+          putChecker
+          eq <- permEquals s k t1 t2
+          return (eq, [])
+        Left _ -> throw $ KindMismatch s Nothing kpermission k
+
     Types ->
       case k of
 
@@ -533,6 +557,105 @@ eqGradedProtocolFunction sp rel grad (TyVar v) t ind = do
 eqGradedProtocolFunction sp _ grad t1 t2 _ = throw
   TypeError{ errLoc = sp, tyExpected = (TyApp (TyApp (TyCon $ mkId "Graded") grad) t1), tyActual = t2 }
 
+-- Compute the behaviour of `Rename id a` on a type `A`
+renameBeta :: (?globals :: Globals)
+  => Type -- name
+  -> Type -- type
+  -> Checker Type
+renameBeta name (TyApp (TyApp (TyCon c) t) s)
+  | internalName c == "Ref" = do
+    s' <- renameBeta name s
+    return $ (TyApp (TyApp (TyCon c) name) s')
+
+renameBeta name (TyApp (TyCon c) t)
+  | internalName c == "FloatArray" = do
+    return $ (TyApp (TyCon c) name)
+
+renameBeta name (TyApp (TyApp (TyCon c) t1) t2)
+  | internalName c == "," = do
+  t1' <- renameBeta name t1
+  t2' <- renameBeta name t2
+  return $ (TyApp (TyApp (TyCon c) t1') t2')
+
+renameBeta name (Star g t) = do
+  t' <- renameBeta name t
+  return $ (Star g t')
+
+renameBeta name (Borrow p t) = do
+  t' <- renameBeta name t
+  return $ (Borrow p t')
+
+renameBeta name t = return t
+
+renameBetaInvert :: (?globals :: Globals)
+  => Span
+  -- Explain how coeffects should be related by a solver constraint
+  -> (Span -> Coeffect -> Coeffect -> Type -> Constraint)
+  -> Type -- name
+  -> Type -- type
+  -- Indicates whether the first type or second type is a specification
+  -> SpecIndicator
+  -- Flag to say whether this type is actually an effect or not
+  -> Mode
+  -> Checker (Type, Substitution)
+
+-- Ref case
+-- i.e., Rename id a = Ref id' a'
+-- therefore check `id ~ id'` and then recurse
+renameBetaInvert sp rel name (TyApp (TyApp (TyCon c) name') s) spec mode
+  | internalName c == "Ref" = do
+    -- Compute equality on names
+    (_, subst) <- equalTypesRelatedCoeffects sp rel name name' spec mode
+    (s, subst') <- renameBetaInvert sp rel name s spec mode
+    substFinal <- combineSubstitutions sp subst subst'
+    return (TyApp (TyApp (TyCon c) name') s, substFinal)
+
+renameBetaInvert sp rel name (TyApp (TyCon c) name') spec mode
+  | internalName c == "FloatArray" = do
+    -- Compute equality on names
+    (_, subst) <- equalTypesRelatedCoeffects sp rel name name' spec mode
+    return (TyApp (TyCon c) name', subst)
+
+renameBetaInvert sp rel name (TyApp (TyApp (TyCon c) t1) t2) spec mode
+  | internalName c == "," = do
+    (t1', subst1) <- renameBetaInvert sp rel name t1 spec mode
+    (t2', subst2) <- renameBetaInvert sp rel name t2 spec mode
+    substFinal <- combineSubstitutions sp subst1 subst2
+    return (TyApp (TyApp (TyCon c) t1') t2', substFinal)
+
+renameBetaInvert _ _ name t _ _ = return (t, [])
+
+-- Check if `Rename id a ~ a'` which may involve some normalisation in the
+-- case where `a'` is a variable
+eqRenameFunction :: (?globals :: Globals)
+  => Span
+  -> (Span -> Coeffect -> Coeffect -> Type -> Constraint)
+  -- These two arguments are the arguments to `Rename id a`
+  -> Type -- name
+  -> Type -- type
+  -- This is the argument of the type which we are trying to see if it equal to `Rename id a`
+  -> Type -- compared against
+  -> SpecIndicator
+  -> Checker (Bool, Substitution)
+
+eqRenameFunction sp rel name t (TyApp (TyApp (TyCon d) name') t') ind
+  | internalName d == "Rename" = do
+  (_, subst) <- equalTypesRelatedCoeffects sp rel name name' ind Types
+  (eq, subst') <- eqRenameFunction sp rel name t t' ind
+  substFinal <- combineSubstitutions sp subst subst'
+  return (eq, substFinal)
+
+eqRenameFunction sp rel name (TyVar v) t ind = do
+  (t', subst) <- renameBetaInvert sp rel name t ind Types
+  (eq, subst') <- equalTypesRelatedCoeffects sp rel t' (TyVar v) ind Types
+  substFinal <- combineSubstitutions sp subst subst'
+  return (eq, substFinal)
+
+eqRenameFunction sp rel name t t' ind = do
+  t'' <- renameBeta name t
+  (eq, u) <- equalTypesRelatedCoeffects sp rel t'' t' ind Types
+  return (eq, u)
+
 -- | Is this protocol dual to the other?
 isDualSession :: (?globals :: Globals)
     => Span
@@ -593,6 +716,23 @@ twoEqualEffectTypes s ef1 ef2 = do
           Left k -> throw $ UnknownResourceAlgebra { errLoc = s, errTy = ef2 , errK = k }
       Left k -> throw $ UnknownResourceAlgebra { errLoc = s, errTy = ef1 , errK = k }
 
+permEquals :: (?globals :: Globals) => Span -> Type -> Type -> Type -> Checker Bool
+permEquals s _ p1 p2 = do
+    mpTy1 <- isPermission s p1
+    mpTy2 <- isPermission s p2
+    case mpTy1 of
+      Right pTy1 ->
+        case mpTy2 of
+          Right pTy2 -> do
+            -- Check that the types of the effect terms match
+            (eq, _, u) <- equalTypes s pTy1 pTy2
+            if eq then do
+              addConstraint (Eq s p1 p2 pTy1)
+              return True
+            else throw $ KindMismatch { errLoc = s, tyActualK = Just p1, kExpected = pTy1, kActual = pTy2 }
+          Left k -> throw $ UnknownResourceAlgebra { errLoc = s, errTy = p2 , errK = k }
+      Left k -> throw $ UnknownResourceAlgebra { errLoc = s, errTy = p1 , errK = k }
+
 -- | Find out if a type is indexed overall (i.e., is a GADT)
 isIndexedType :: Type -> Checker Bool
 isIndexedType t = do
@@ -605,17 +745,20 @@ isIndexedType t = do
       , tfBox = \_ (Const x) -> return $ Const x
       , tfDiamond = \_ (Const x) -> return $ Const x
       , tfStar = \_ (Const x) -> return $ Const x
+      , tfBorrow = \_ (Const x) -> return $ Const x
       , tfTyVar = \_ -> return $ Const False
       , tfTyApp = \(Const x) (Const y) -> return $ Const (x || y)
       , tfTyInt = \_ -> return $ Const False
       , tfTyRational = \_ -> return $ Const False
+      , tfTyFraction = \_ -> return $ Const False
       , tfTyGrade = \_ _ -> return $ Const False
       , tfTyInfix = \_ (Const x) (Const y) -> return $ Const (x || y)
       , tfSet = \_ _ -> return $ Const False
       , tfTyCase = \_ _ -> return $ Const False
       , tfTySig = \(Const b) _ _ -> return $ Const b
       , tfTyExists = \_ _ (Const a) -> return $ Const a
-      , tfTyForall = \_ _ (Const a) -> return $ Const a } t
+      , tfTyForall = \_ _ (Const a) -> return $ Const a
+      , tfTyName = \_ -> return $ Const False } t
   return $ getConst b
 
 -- Given a type term, works out if its kind is actually an effect type
@@ -648,6 +791,7 @@ refineBinderQuantification ctxt ty = mapM computeQuantifier ctxt
     aux id (Box _ t)       = aux id t
     aux id (Diamond _ t)   = aux id t
     aux id (Star _ t)      = aux id t
+    aux id (Borrow _ t)      = aux id t
     aux id t@(TyApp _ t2)   =
       case leftmostOfApplication t of
         TyCon tyConId -> do
@@ -670,4 +814,14 @@ refineBinderQuantification ctxt ty = mapM computeQuantifier ctxt
     aux id (TyCase t ts)     = liftM2 (||) (aux id t) (anyM (\(_, t) -> aux id t) ts)
       where
         anyM f xs = mapM f xs >>= (return . or)
-    aux id _ = return False
\ No newline at end of file
+    aux id _ = return False
+
+isPermission :: (?globals :: Globals) => Span -> Type -> Checker (Either Kind Type)
+isPermission s ty = do
+  (pTy, _, _) <- synthKind s ty
+  (result, putChecker) <- peekChecker (checkKind s pTy kpermission)
+  case result of
+    Right res -> do
+      putChecker
+      return $ Right pTy
+    Left err -> return $ Left pTy
diff --git a/frontend/src/Language/Granule/Context.hs b/frontend/src/Language/Granule/Context.hs
index 0ddee24df..53ca8591f 100644
--- a/frontend/src/Language/Granule/Context.hs
+++ b/frontend/src/Language/Granule/Context.hs
@@ -8,7 +8,7 @@ module Language.Granule.Context where
 
 import Data.Maybe (isJust)
 import Data.List (sortBy)
-import Language.Granule.Syntax.Identifiers (Id)
+import Language.Granule.Syntax.Identifiers (Id, sourceName)
 
 -- | Type of contexts
 type Ctxt t = [(Id, t)]
@@ -91,4 +91,11 @@ lookupAndCutoutBy f v ((v', t'):ctxt) = do
   Just ((v', t') : ctxt', t)
 
 getCtxtIds :: Ctxt t -> [Id]
-getCtxtIds = map fst
\ No newline at end of file
+getCtxtIds = map fst
+
+nubContext :: Ctxt t -> Ctxt t
+nubContext = aux []
+  where
+    aux seen [] = []
+    aux seen ((x, t) : ctxt) | sourceName x `elem` seen = aux seen ctxt
+                             | otherwise = (x, t) : aux (sourceName x : seen) ctxt
\ No newline at end of file
diff --git a/frontend/src/Language/Granule/Syntax/Expr.hs b/frontend/src/Language/Granule/Syntax/Expr.hs
index a8d49a087..9b5c9d54a 100755
--- a/frontend/src/Language/Granule/Syntax/Expr.hs
+++ b/frontend/src/Language/Granule/Syntax/Expr.hs
@@ -53,6 +53,7 @@ data ValueF ev a value expr =
     | PromoteF a expr
     | PureF a expr
     | NecF a expr
+    | RefF a expr
     | ConstrF a Id [value]
     | VarF a Id
     | NumIntF Int
@@ -89,6 +90,9 @@ pattern Pure a ex = (ExprFix2 (PureF a ex))
 pattern Nec :: a -> ExprFix2 g ValueF ev a -> ExprFix2 ValueF g ev a
 pattern Nec a ex = (ExprFix2 (NecF a ex))
 
+pattern Ref :: a -> ExprFix2 g ValueF ev a -> ExprFix2 ValueF g ev a
+pattern Ref a ex = (ExprFix2 (RefF a ex))
+
 pattern Constr :: a -> Id -> [ExprFix2 ValueF g ev a] -> ExprFix2 ValueF g ev a
 pattern Constr a ident vals = (ExprFix2 (ConstrF a ident vals))
 
@@ -274,6 +278,7 @@ instance Functor (Value ev) where
   fmap f (Promote a e)     = Promote (f a) (fmap f e)
   fmap f (Pure a e)        = Pure (f a) (fmap f e)
   fmap f (Nec a e)         = Nec (f a) (fmap f e)
+  fmap f (Ref a e)         = Ref (f a) (fmap f e)
   fmap f (Constr a idv vals) = Constr (f a) idv (map (fmap f) vals)
   fmap f (Var a idv)       = Var (f a) idv
   fmap f (Ext a ev)        = Ext (f a) ev
@@ -380,6 +385,7 @@ instance Term (Value ev a) where
     freeVars (Pure _ e)    = freeVars e
     freeVars (Promote _ e) = freeVars e
     freeVars (Nec _ e)    = freeVars e
+    freeVars (Ref _ e)    = freeVars e
     freeVars NumInt{}        = []
     freeVars NumFloat{}      = []
     freeVars Constr{}        = []
@@ -394,6 +400,7 @@ instance Term (Value ev a) where
     hasHole (Promote _ e) = hasHole e
     hasHole (Nec _ e)    = hasHole e
     hasHole (Pack s a ty e1 var k ty') = hasHole e1
+    hasHole (Ref _ e)    = hasHole e
     hasHole _             = False
 
     isLexicallyAtomic Abs{} = False
@@ -405,6 +412,7 @@ instance Substitutable Value where
     subst es v (Pure a e)         = Val (nullSpanInFile $ getSpan es) a False $ Pure a (subst es v e)
     subst es v (Promote a e)      = Val (nullSpanInFile $ getSpan es) a False $ Promote a (subst es v e)
     subst es v (Nec a e)          = Val (nullSpanInFile $ getSpan es) a False $ Nec a (subst es v e)
+    subst es v (Ref a e)          = Val (nullSpanInFile $ getSpan es) a False $ Ref a (subst es v e)
     subst es v (Var a w) | v == w = es
     subst es _ v@NumInt{}        = Val (nullSpanInFile $ getSpan es) (getFirstParameter v) False v
     subst es _ v@NumFloat{}      = Val (nullSpanInFile $ getSpan es) (getFirstParameter v) False v
@@ -440,6 +448,10 @@ instance Monad m => Freshenable m (Value v a) where
       e' <- freshen e
       return $ Nec a e'
 
+    freshen (Ref a e) = do
+      e' <- freshen e
+      return $ Ref a e'
+
     freshen (Var a v) = do
       v' <- lookupVar ValueL v
       case v' of
diff --git a/frontend/src/Language/Granule/Syntax/Lexer.x b/frontend/src/Language/Granule/Syntax/Lexer.x
index bce01266a..23c1bca17 100755
--- a/frontend/src/Language/Granule/Syntax/Lexer.x
+++ b/frontend/src/Language/Granule/Syntax/Lexer.x
@@ -63,6 +63,7 @@ tokens :-
   pack                          { \p s -> TokenPack p }
   unpack                        { \p s -> TokenUnpack p }
   exists                        { \p s -> TokenExists p }
+  mut                       { \p s -> TokenMutable p }
   "∃"                           { \p s -> TokenExists p }
   ∞                             { \p s -> TokenInfinity p }
   @float                        { \p s -> TokenFloat p s }
@@ -204,6 +205,7 @@ data Token
   | TokenPack AlexPosn
   | TokenUnpack AlexPosn
   | TokenExists AlexPosn
+  | TokenMutable AlexPosn
   | TokenHash AlexPosn
   | TokenPercent AlexPosn
   | TokenStar AlexPosn
diff --git a/frontend/src/Language/Granule/Syntax/Parser.y b/frontend/src/Language/Granule/Syntax/Parser.y
index 2564aa30c..36f10b07a 100644
--- a/frontend/src/Language/Granule/Syntax/Parser.y
+++ b/frontend/src/Language/Granule/Syntax/Parser.y
@@ -16,6 +16,7 @@ import Data.Foldable (toList)
 import Data.List (intercalate, nub, stripPrefix)
 import Data.Maybe (mapMaybe)
 import Data.Set (Set, (\\), fromList, insert, empty, singleton)
+import Data.Ratio ((%))
 import qualified Data.Map as M
 import Numeric
 import System.FilePath ((</>), takeBaseName)
@@ -75,6 +76,7 @@ import Language.Granule.Utils hiding (mkSpan)
     CHAR   { TokenCharLiteral _ _ }
     STRING { TokenStringLiteral _ _ }
     forall { TokenForall _ }
+    mutable { TokenMutable _ }
     '∞'   { TokenInfinity _ }
     '\\'  { TokenLambda _ }
     '/'  { TokenForwardSlash _ }
@@ -390,13 +392,14 @@ Type :: { Type }
   | '(' VAR ':' Type ')' '%' Coeffect '->' Type { FunTy (Just . mkId . symString $ $2) (Just $7) $4 $9 }
   | TyJuxt                         { $1 }
   | '!' TyAtom                     { Box (TyCon $ mkId "Many") $2 }
-  | '*' TyAtom                     { Star (TyCon $ mkId "Unique") $2 }
+  | '*' TyAtom                     { Borrow (TyCon $ mkId "Star") $2 }
   | Type '->' Type                 { FunTy Nothing Nothing $1 $3 }
   | Type '%' Coeffect '->' Type    { FunTy Nothing (Just $3) $1 $5 }
   | Type '×' Type                  { TyApp (TyApp (TyCon $ mkId ",") $1) $3 }
   | Type '&' Type                  { TyApp (TyApp (TyCon $ mkId "&") $1) $3 }
   | TyAtom '[' Coeffect ']'        { Box $3 $1 }
   | TyAtom '*{' Guarantee '}'      { Star $3 $1 }
+  | '&' Permission TyAtom          { Borrow $2 $3 }
   | TyAtom '[' ']'                 { Box (TyInfix TyOpInterval (TyGrade (Just extendedNat) 0) infinity) $1 }
   | TyAtom '<' Effect '>'          { Diamond $3 $1 }
   | case Type of TyCases { TyCase $2 $4 }
@@ -438,6 +441,7 @@ TyCase :: { (Type, Type) }
 
 Constraint :: { Type }
   : TyJuxt TyAtom             { TyApp $1 $2 }
+  | mutable TyAtom          { TyInfix TyOpMutable $2 $2}
   | TyAtom '>' TyAtom         { TyInfix TyOpGreaterNat $1 $3 }
   | TyAtom '<' TyAtom         { TyInfix TyOpLesserNat $1 $3 }
   | TyAtom '<=' TyAtom        { TyInfix TyOpLesserEq $1 $3 }
@@ -533,6 +537,14 @@ TyAbsNamed :: { [(Id, Type)] }
 TyAbsImplicit :: { [Id] }
   : VAR ',' TyAbsImplicit       { (mkId $ symString $1) : $3 }
   | VAR                         { [mkId $ symString $1] }
+Permission :: { Type }
+  : CONSTR                  { TyCon $ mkId $ constrString $1 }
+  | VAR                     { TyVar (mkId $ symString $1) }
+  | INT '/' INT             { TyFraction $ let TokenInt _ n = $1 in let TokenInt _ d = $3 in (toInteger n) % (toInteger d) }
+  | INT                     { TyFraction $ let TokenInt _ n = $1 in (toInteger n) % 1}
+  | Permission '+' Permission         { TyInfix TyOpPlus $1 $3 }
+  | Permission '*' Permission         { TyInfix TyOpTimes $1 $3 }
+  | '(' Permission ')'              { $2 }
 
 Expr :: { Expr () () }
   : let LetBind MultiLet
diff --git a/frontend/src/Language/Granule/Syntax/Pretty.hs b/frontend/src/Language/Granule/Syntax/Pretty.hs
index 04cde11b8..b694272bf 100644
--- a/frontend/src/Language/Granule/Syntax/Pretty.hs
+++ b/frontend/src/Language/Granule/Syntax/Pretty.hs
@@ -14,6 +14,7 @@ module Language.Granule.Syntax.Pretty where
 
 import Data.Foldable (toList)
 import Data.List (intercalate)
+import Data.Ratio (numerator, denominator)
 import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Type
 import Language.Granule.Syntax.Pattern
@@ -102,6 +103,11 @@ instance Pretty Type where
     pretty (TyGrade Nothing n)  = show n
     pretty (TyGrade (Just t) n)  = "(" <> show n <> " : " <> pretty t <> ")"
     pretty (TyRational n) = show n
+    pretty (TyFraction f) = let (n, d) = (numerator f, denominator f) in
+      if d == 1 then
+        show n
+      else
+        show n <> "/" <> show d
 
     -- Non atoms
     pretty (Type 0) = docSpan "constName" "Type"
@@ -136,6 +142,11 @@ instance Pretty Type where
         (TyCon (Id "Unique" "Unique")) -> docSpan "uniq" ("*" <> prettyNested t)
         otherwise -> prettyNested t <> " *" <> docSpan "uniq" (pretty g)
 
+    pretty (Borrow p t) =
+      case p of
+        (TyCon (Id "Star" "Star")) -> docSpan "uniq" ("*" <> prettyNested t)
+        otherwise -> docSpan "perm" ("& " <> prettyNested p <> " " <> prettyNested t)
+
     pretty (TyApp (TyApp (TyCon x) t1) t2) | sourceName x == "," =
       "(" <> pretty t1 <> ", " <> pretty t2 <> ")"
 
@@ -154,6 +165,9 @@ instance Pretty Type where
     pretty (TyInfix TyOpInterval t1 t2) =
       prettyNested t1 <> pretty TyOpInterval <> prettyNested t2
 
+    pretty (TyInfix TyOpMutable t1 _) =
+      pretty TyOpMutable <> " " <> prettyNested t1
+
     pretty (TyInfix op t1 t2) =
       prettyNested t1 <> " " <> pretty op <> " " <> prettyNested t2
 
@@ -174,6 +188,8 @@ instance Pretty Type where
 
     pretty (TyForall var k t) =
       docSpan "keyword" "forall" <> " {" <> pretty var <> " : " <> pretty k <> "} . " <> pretty t
+    
+    pretty (TyName n) = "id" ++ show n
 
 instance Pretty TypeOperator where
   pretty = \case
@@ -195,6 +211,7 @@ instance Pretty TypeOperator where
    TyOpConverge        -> "#"
    TyOpImpl            -> "=>"
    TyOpHsup            -> "⨱"
+   TyOpMutable         -> "mut"
 
 instance Pretty v => Pretty (AST v a) where
   pretty (AST dataDecls defs imprts hidden name) =
@@ -282,6 +299,7 @@ instance Pretty v => Pretty (Value v a) where
     pretty (Promote _ e) = "[" <> pretty e <> "]"
     pretty (Pure _ e)    = "<" <> pretty e <> ">"
     pretty (Nec _ e)     = "*" <> pretty e
+    pretty (Ref _ e)     = "&" <> pretty e
     pretty (Var _ x)     = pretty x
     pretty (NumInt n)    = show n
     pretty (NumFloat n)  = show n
diff --git a/frontend/src/Language/Granule/Syntax/Type.hs b/frontend/src/Language/Granule/Syntax/Type.hs
index 44d959861..d29899f1d 100644
--- a/frontend/src/Language/Granule/Syntax/Type.hs
+++ b/frontend/src/Language/Granule/Syntax/Type.hs
@@ -37,6 +37,7 @@ Example: `List n Int` in Granule
 type Coeffect = Type
 type Effect   = Type
 type Guarantee = Type
+type Permission = Type
 type Kind     = Type
 
 -- Represents polairty information for lattices
@@ -52,10 +53,12 @@ data Type where
     Box     :: Coeffect -> Type -> Type             -- ^ Graded modal necessity
     Diamond :: Effect   -> Type -> Type             -- ^ Graded modal possibility
     Star    :: Guarantee -> Type -> Type
+    Borrow  :: Permission -> Type -> Type
     TyVar   :: Id -> Type                           -- ^ Type variable
     TyApp   :: Type -> Type -> Type                 -- ^ Type application
     TyInt   :: Int -> Type                          -- ^ Type-level Int
     TyRational :: Rational -> Type                  -- ^ Type-level Rational
+    TyFraction :: Rational -> Type
     TyGrade :: Maybe Type -> Int -> Type            -- ^ Graded element
     TyInfix :: TypeOperator -> Type -> Type -> Type -- ^ Infix type operator
 
@@ -65,6 +68,7 @@ data Type where
     TySig   :: Type -> Kind -> Type           -- ^ Kind signature
     TyExists :: Id -> Kind -> Type -> Type    -- ^ Exists
     TyForall :: Id -> Kind -> Type -> Type    -- ^ RankNForall
+    TyName :: Int -> Type
 
 deriving instance Show Type
 deriving instance Eq Type
@@ -92,6 +96,7 @@ data TypeOperator
   | TyOpConverge
   | TyOpImpl
   | TyOpHsup
+  | TyOpMutable
   deriving (Eq, Ord, Show, Data)
 
 -- ## Type schemes
@@ -156,6 +161,9 @@ keffect = tyCon "Effect"
 kguarantee :: Type
 kguarantee = tyCon "Guarantee"
 
+kpermission :: Type
+kpermission = tyCon "Permission"
+
 kpredicate :: Type
 kpredicate = tyCon "Predicate"
 
@@ -225,17 +233,20 @@ containsTypeSig =
       , tfBox = \x y -> return (x || y)
       , tfDiamond = \x y -> return $ (x || y)
       , tfStar = \x y -> return $ (x || y)
+      , tfBorrow = \x y -> return $ (x || y)
       , tfTyVar = \_ -> return False
       , tfTyApp = \x y -> return (x || y)
       , tfTyInt = \_ -> return False
       , tfTyRational = \_ -> return False
+      , tfTyFraction = \_ -> return False
       , tfTyGrade = \_ _ -> return False
       , tfTyInfix = \_ x y -> return (x || y)
       , tfSet = \_ _ -> return  False
       , tfTyCase = \_ _ -> return False
       , tfTySig = \_ _ _ -> return True
       , tfTyExists = \_ _ x -> return x
-      , tfTyForall = \_ _ x -> return x})
+      , tfTyForall = \_ _ x -> return x
+      , tfTyName = \_ -> return False})
 
 -- | Compute the arity of a function type
 arity :: Type -> Int
@@ -298,6 +309,8 @@ mDiamond :: Monad m => Type -> Type -> m Type
 mDiamond e y = return (Diamond e y)
 mStar :: Monad m => Guarantee -> Type -> m Type
 mStar g y    = return (Star g y)
+mBorrow :: Monad m => Permission -> Type -> m Type
+mBorrow p y = return (Borrow p y)
 mTyVar :: Monad m => Id -> m Type
 mTyVar       = return . TyVar
 mTyApp :: Monad m => Type -> Type -> m Type
@@ -306,6 +319,8 @@ mTyInt :: Monad m => Int -> m Type
 mTyInt       = return . TyInt
 mTyRational :: Monad m => Rational -> m Type
 mTyRational          = return . TyRational
+mTyFraction :: Monad m => Rational -> m Type
+mTyFraction  = return . TyFraction
 mTyGrade :: Monad m => Maybe Type -> Int -> m Type
 mTyGrade t c = return $ TyGrade t c
 mTyInfix :: Monad m => TypeOperator -> Type -> Type -> m Type
@@ -320,6 +335,8 @@ mTyExists :: Monad m => Id -> Kind -> Type -> m Type
 mTyExists v k t   = return (TyExists v k t)
 mTyForall :: Monad m => Id -> Kind -> Type -> m Type
 mTyForall v k t   = return (TyForall v k t)
+mTyName :: Monad m => Int -> m Type
+mTyName = return . TyName
 
 -- Monadic algebra for types
 data TypeFold m a = TypeFold
@@ -329,10 +346,12 @@ data TypeFold m a = TypeFold
   , tfBox     :: a -> a             -> m a
   , tfDiamond :: a -> a             -> m a
   , tfStar    :: a -> a             -> m a
+  , tfBorrow  :: a -> a             -> m a
   , tfTyVar   :: Id                 -> m a
   , tfTyApp   :: a -> a             -> m a
   , tfTyInt   :: Int                -> m a
   , tfTyRational :: Rational        -> m a
+  , tfTyFraction :: Rational        -> m a
   , tfTyGrade :: Maybe a   -> Int  -> m a
   , tfTyInfix :: TypeOperator -> a -> a -> m a
   , tfSet     :: Polarity -> [a]    -> m a
@@ -340,12 +359,13 @@ data TypeFold m a = TypeFold
   , tfTySig   :: a -> Type -> (a -> m a)
   , tfTyExists :: Id -> a -> a      -> m a
   , tfTyForall :: Id -> a -> a      -> m a
+  , tfTyName :: Int -> m a
   }
 
 -- Base monadic algebra
 baseTypeFold :: Monad m => TypeFold m Type --Type
 baseTypeFold =
-  TypeFold mTy mFunTy mTyCon mBox mDiamond mStar mTyVar mTyApp mTyInt mTyRational mTyGrade mTyInfix mTySet mTyCase mTySig mTyExists mTyForall
+  TypeFold mTy mFunTy mTyCon mBox mDiamond mStar mBorrow mTyVar mTyApp mTyInt mTyRational mTyFraction mTyGrade mTyInfix mTySet mTyCase mTySig mTyExists mTyForall mTyName
 
 -- | Monadic fold on a `Type` value
 typeFoldM :: forall m a . Monad m => TypeFold m a -> Type -> m a
@@ -371,6 +391,10 @@ typeFoldM algebra = go
      t' <- go t
      g' <- go g
      (tfStar algebra) g' t'
+   go (Borrow p t) = do
+     t' <- go t
+     p' <- go p
+     (tfBorrow algebra) p' t'
    go (TyVar v) = (tfTyVar algebra) v
    go (TyApp t1 t2) = do
      t1' <- go t1
@@ -378,6 +402,7 @@ typeFoldM algebra = go
      (tfTyApp algebra) t1' t2'
    go (TyInt i) = (tfTyInt algebra) i
    go (TyRational i) = (tfTyRational algebra) i
+   go (TyFraction i) = (tfTyFraction algebra) i
    go (TyGrade Nothing i) = (tfTyGrade algebra) Nothing i
    go (TyGrade (Just t) i) = do
      t' <- go t
@@ -412,6 +437,7 @@ typeFoldM algebra = go
     k' <- go k
     t' <- go t
     (tfTyForall algebra) var k' t'
+   go (TyName i) = (tfTyName algebra) i
 
 ----------------------------------------------------------------------
 -- # Types are terms
@@ -424,10 +450,12 @@ instance Term Type where
       , tfBox     = \(Const c) (Const t) -> return $ Const (c <> t)
       , tfDiamond = \(Const e) (Const t) -> return $ Const (e <> t)
       , tfStar    = \(Const g) (Const t) -> return $ Const (g <> t)
+      , tfBorrow  = \(Const p) (Const t) -> return $ Const (p <> t)
       , tfTyVar   = \v -> return $ Const [v] -- or: return . return
       , tfTyApp   = \(Const x) (Const y) -> return $ Const (x <> y)
       , tfTyInt   = \_ -> return (Const [])
       , tfTyRational  = \_ -> return (Const [])
+      , tfTyFraction = \_ -> return (Const [])
       , tfTyGrade     = \_ _ -> return (Const [])
       , tfTyInfix = \_ (Const y) (Const z) -> return $ Const (y <> z)
       , tfSet     = \_ -> return . Const . concat . map getConst
@@ -435,16 +463,19 @@ instance Term Type where
       , tfTySig   = \(Const t) _ (Const k) -> return $ Const (t <> k)
       , tfTyExists = \v _ (Const fvs) -> return $ Const [v' | v' <- fvs, v /= v']
       , tfTyForall = \v _ (Const fvs) -> return $ Const [v' | v' <- fvs, v /= v']
+      , tfTyName = \_ -> return (Const [])
       }
 
     isLexicallyAtomic TyInt{} = True
     isLexicallyAtomic TyRational{} = True
+    isLexicallyAtomic TyFraction{} = True
     isLexicallyAtomic TyGrade{} = True
     isLexicallyAtomic TyVar{} = True
     isLexicallyAtomic TySet{} = True
     isLexicallyAtomic TyCon{} = True
     isLexicallyAtomic (Type 0) = True
     isLexicallyAtomic (TyApp (TyApp (TyCon (sourceName -> ",")) _) _) = True
+    isLexicallyAtomic TyName{} = True
     isLexicallyAtomic _ = False
 
 substType :: Type -> Id -> Type -> Type
@@ -511,11 +542,14 @@ instance Freshenable m Type where
 --   local evaluation of natural numbers
 --   There is plenty more scope to make this more comprehensive
 --   None of this is stricly necessary but it improves type errors
---   and speeds up some constarint solving.
+--   and speeds up some constraint solving.
 normalise :: Type -> Type
 normalise (TyInfix TyOpPlus (TyRational n) (TyRational m)) = TyRational (n + m)
 normalise (TyInfix TyOpTimes (TyRational n) (TyRational m)) = TyRational (n * m)
 
+normalise (TyInfix TyOpPlus (TyFraction n) (TyFraction m)) = TyFraction (n + m)
+normalise (TyInfix TyOpTimes (TyFraction n) (TyFraction m)) = TyFraction (n * m)
+
 -- exempt Uniquness from multiplicative unit
 normalise g@(TyInfix TyOpTimes r (TyGrade (Just (TyCon (internalName -> "Uniqueness"))) 1)) = g
 normalise g@(TyInfix TyOpTimes (TyGrade (Just (TyCon (internalName -> "Uniqueness"))) 1) r) = g
diff --git a/frontend/src/Language/Granule/Synthesis/Splitting.hs b/frontend/src/Language/Granule/Synthesis/Splitting.hs
index ee6d94576..e9e0cd109 100644
--- a/frontend/src/Language/Granule/Synthesis/Splitting.hs
+++ b/frontend/src/Language/Granule/Synthesis/Splitting.hs
@@ -229,11 +229,13 @@ getAssumConstr a =
     getTypeConstr (Box _ t) = getTypeConstr t
     getTypeConstr (Diamond t1 _) = getTypeConstr t1
     getTypeConstr (Star _ t) = getTypeConstr t
+    getTypeConstr (Borrow _ t) = getTypeConstr t
     getTypeConstr (TyApp t1 t2) = getTypeConstr t1
     getTypeConstr (TySig t _) = getTypeConstr t
     getTypeConstr (TyVar _) = Nothing
     getTypeConstr (TyInt _) = Nothing
     getTypeConstr (TyRational _) = Nothing
+    getTypeConstr (TyFraction _) = Nothing
     getTypeConstr (TyGrade _ _) = Nothing
     getTypeConstr (TyInfix _ _ _) = Nothing
     getTypeConstr (TySet _ _) = Nothing
@@ -248,6 +250,7 @@ getAssumConstr a =
        allSame [x] = True
        allSame (x:(y:xs)) =
          if x == y then allSame xs else False
+    getTypeConstr (TyName _) = Nothing
 
 -- Given a function type, expand grades on parameters to be more permissive,
 -- for the purpose of generating theorems. Exact natural number grades greater
diff --git a/frontend/tests/cases/negative/flatten/flattenSec.gr b/frontend/tests/cases/negative/flatten/flattenSec.gr
index 524616535..01ad1559f 100644
--- a/frontend/tests/cases/negative/flatten/flattenSec.gr
+++ b/frontend/tests/cases/negative/flatten/flattenSec.gr
@@ -1,8 +1,8 @@
 leak : forall {a : Type} . a [Private] -> a [Public]
-leak x = join (split x)
+leak x = joiner (spliter x)
 
-split : forall {a : Type} . a [Private] -> (a [Private]) [Public]
-split [x] = [[x]]
+spliter : forall {a : Type} . a [Private] -> (a [Private]) [Public]
+spliter [x] = [[x]]
 
-join : forall {a : Type} . (a [Private]) [Public] -> a [Public]
-join [[x]] = [x]
\ No newline at end of file
+joiner : forall {a : Type} . (a [Private]) [Public] -> a [Public]
+joiner [[x]] = [x]
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/flatten/flattenSec.gr.output b/frontend/tests/cases/negative/flatten/flattenSec.gr.output
index 901906eb9..66eb85206 100644
--- a/frontend/tests/cases/negative/flatten/flattenSec.gr.output
+++ b/frontend/tests/cases/negative/flatten/flattenSec.gr.output
@@ -1,3 +1,3 @@
 Type checking failed: 
 Falsifiable theorem: frontend/tests/cases/negative/flatten/flattenSec.gr:8:1:
-  When checking `join`, public is not approximatable by Public * Private for type Sec
\ No newline at end of file
+  When checking `joiner`, public is not approximatable by Public * Private for type Sec
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/unique/badClone.gr b/frontend/tests/cases/negative/unique/badClone.gr
new file mode 100644
index 000000000..9836f15a5
--- /dev/null
+++ b/frontend/tests/cases/negative/unique/badClone.gr
@@ -0,0 +1,13 @@
+nonShareable : exists {id : Name} . ((FloatArray id) [0])
+nonShareable =
+  unpack <id , a> = newFloatArray 3
+  in
+     (pack <id, (share a)> as exists {id : Name} . (FloatArray id) [0])
+
+example : ()
+example = unpack <id , a> = nonShareable in
+  clone a as x in
+    unpack <id' , a'> = x in (deleteFloatArray a')
+
+-- main : ()
+-- main = example
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/unique/badClone.gr.output b/frontend/tests/cases/negative/unique/badClone.gr.output
new file mode 100644
index 000000000..7ca8a1394
--- /dev/null
+++ b/frontend/tests/cases/negative/unique/badClone.gr.output
@@ -0,0 +1,3 @@
+Type checking failed: 
+Falsifiable theorem: frontend/tests/cases/negative/unique/badClone.gr:8:1:
+  When checking `example`, expected 0 uses, but instead there are (1 : Nat) actual uses.
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/unique/cloneNonCloneable.gr b/frontend/tests/cases/negative/unique/cloneNonCloneable.gr
new file mode 100644
index 000000000..b33d2ac2c
--- /dev/null
+++ b/frontend/tests/cases/negative/unique/cloneNonCloneable.gr
@@ -0,0 +1,4 @@
+example : Int [1]
+example =
+  clone [42] as x
+    in (unpack <id' , a'> = x in (share a'))
diff --git a/frontend/tests/cases/negative/unique/cloneNonCloneable.gr.output b/frontend/tests/cases/negative/unique/cloneNonCloneable.gr.output
new file mode 100644
index 000000000..48e048bb8
--- /dev/null
+++ b/frontend/tests/cases/negative/unique/cloneNonCloneable.gr.output
@@ -0,0 +1,3 @@
+Type checking failed: 
+Type constraint error: frontend/tests/cases/negative/unique/cloneNonCloneable.gr:1:1:
+Constraint `Cloneable Int` does not hold or is not provided by the type constraint assumptions here.
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/unique/uniqueProduct.gr b/frontend/tests/cases/negative/unique/uniqueProduct.gr
index 0189e4eed..409bdfe52 100644
--- a/frontend/tests/cases/negative/unique/uniqueProduct.gr
+++ b/frontend/tests/cases/negative/unique/uniqueProduct.gr
@@ -1,9 +1,9 @@
-writeTwoArrays : (*FloatArray, *FloatArray) -> (*FloatArray, *FloatArray)
+writeTwoArrays : forall {id id' : Name} . (*(FloatArray id), *(FloatArray id')) -> (*(FloatArray id), *(FloatArray id'))
 writeTwoArrays (arr1, arr2) = (writeFloatArray arr1 0 2.3, writeFloatArray arr2 1 4.5)
 
-haveAndEatTwo : (*FloatArray, *FloatArray) -> ((*FloatArray, *FloatArray), (*FloatArray, *FloatArray))
+haveAndEatTwo : forall {id id' : Name} . (*(FloatArray id), *(FloatArray id')) -> ((*(FloatArray id), *(FloatArray id')), (*(FloatArray id), *(FloatArray id')))
 haveAndEatTwo arrs = (writeTwoArrays arrs, arrs)
 
--- products are *linear* in Granule rather than unique, so we cannot sneakily 
+-- products are *linear* in Granule rather than unique, so we cannot sneakily
 -- copy a uniqueness guarantee by duplicating a product of two arrays rather
 -- than having to duplicate the individual arrays themselves
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/unique/uniqueProduct.gr.output b/frontend/tests/cases/negative/unique/uniqueProduct.gr.output
index fb2acb372..60ee47024 100644
--- a/frontend/tests/cases/negative/unique/uniqueProduct.gr.output
+++ b/frontend/tests/cases/negative/unique/uniqueProduct.gr.output
@@ -1,3 +1,6 @@
 Type checking failed: 
+Ownership error: frontend/tests/cases/negative/unique/uniqueProduct.gr:2:58:
+Cannot guarantee usage of reference to value of type `FloatArray id` at permission `Star`.
+
 Linearity error: frontend/tests/cases/negative/unique/uniqueProduct.gr:5:22:
 Linear variable `arrs` is used more than once.
\ No newline at end of file
diff --git a/frontend/tests/cases/positive/unique/simpleClone.gr b/frontend/tests/cases/positive/unique/simpleClone.gr
new file mode 100644
index 000000000..a4cff8d33
--- /dev/null
+++ b/frontend/tests/cases/positive/unique/simpleClone.gr
@@ -0,0 +1,7 @@
+example : ()
+example = unpack <id , a> = newFloatArray 3 in
+  clone (share a) as x in
+    unpack <id' , a'> = x in (deleteFloatArray a')
+
+main : ()
+main = example
\ No newline at end of file
diff --git a/frontend/tests/cases/positive/unique/simpleClone.gr.output b/frontend/tests/cases/positive/unique/simpleClone.gr.output
new file mode 100644
index 000000000..dd626a0f3
--- /dev/null
+++ b/frontend/tests/cases/positive/unique/simpleClone.gr.output
@@ -0,0 +1 @@
+()
\ No newline at end of file
diff --git a/interpreter/granule-interpreter.cabal b/interpreter/granule-interpreter.cabal
index 6dfc96114..a2f623c97 100644
--- a/interpreter/granule-interpreter.cabal
+++ b/interpreter/granule-interpreter.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.35.2.
 --
 -- see: https://github.com/sol/hpack
 
diff --git a/interpreter/src/Language/Granule/Interpreter/Eval.hs b/interpreter/src/Language/Granule/Interpreter/Eval.hs
index 4fad83e9f..ce6f828bf 100755
--- a/interpreter/src/Language/Granule/Interpreter/Eval.hs
+++ b/interpreter/src/Language/Granule/Interpreter/Eval.hs
@@ -18,6 +18,7 @@ import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Pattern
 import Language.Granule.Syntax.Pretty
 import Language.Granule.Syntax.Span (nullSpanNoFile)
+import Language.Granule.Syntax.Type
 import Language.Granule.Context
 import Language.Granule.Utils (nullSpan, Globals, globalsExtensions, entryPoint, Extension(..))
 import Language.Granule.Runtime as RT
@@ -37,6 +38,7 @@ import qualified System.IO as SIO
 --import System.IO.Error (mkIOError)
 import Data.Bifunctor
 import Control.Monad.Extra (void)
+import Data.Unique
 
 type RValue = Value (Runtime ()) ()
 type RExpr = Expr (Runtime ()) ()
@@ -60,7 +62,7 @@ data Runtime a =
   | PureWrapper (IO (Expr (Runtime a) ()))
 
   -- | Data managed by the runtime module (mutable arrays)
-  | Runtime RuntimeData
+  | Runtime (RuntimeData RValue)
 
   -- | Free monad representation
   | FreeMonadImpure (Expr (Runtime a) ())
@@ -151,7 +153,8 @@ instance Show (Runtime a) where
   show (PrimitiveClosure _) = "Some primitive closure"
   show (Handle _) = "Some handle"
   show (PureWrapper _) = "<suspended IO>"
-  show (Runtime _) = "<array>"
+  show (Runtime (RT.FA _)) = "<array>"
+  show (Runtime (RT.PR _)) = "<ref>"
   show (FreeMonadImpure r) = "Impure(" <> show r <> ")"
   show (FreeMonadBind r p k) = "do {... <- " <> show r <> "; ...}"
 
@@ -800,19 +803,26 @@ builtIns =
   -- , (mkId "freePtr", free)
   , (mkId "uniqueReturn",  Ext () $ Primitive uniqueReturn)
   , (mkId "uniqueBind",    Ext () $ PrimitiveClosure uniqueBind)
-  , (mkId "uniquePush",    Ext () $ Primitive uniquePush)
-  , (mkId "uniquePull",    Ext () $ Primitive uniquePull)
   , (mkId "reveal",  Ext () $ Primitive reveal)
   , (mkId "trustedBind",    Ext () $ PrimitiveClosure trustedBind)
+  , (mkId "withBorrow",     Ext () $ PrimitiveClosure withBorrow)
+  , (mkId "split",     Ext () $ Primitive split)
+  , (mkId "join",     Ext () $ Primitive join)
+  , (mkId "borrowPush",     Ext () $ Primitive borrowPush)
+  , (mkId "borrowPull",     Ext () $ Primitive borrowPull)
   , (mkId "newFloatArray",  Ext () $ Primitive newFloatArray)
-  , (mkId "lengthFloatArray",  Ext () $ Primitive lengthFloatArray)
-  , (mkId "readFloatArray",  Ext () $ Primitive readFloatArray)
-  , (mkId "writeFloatArray",  Ext () $ Primitive writeFloatArray)
   , (mkId "newFloatArrayI",  Ext () $ Primitive newFloatArrayI)
   , (mkId "lengthFloatArrayI",  Ext () $ Primitive lengthFloatArrayI)
   , (mkId "readFloatArrayI",  Ext () $ Primitive readFloatArrayI)
   , (mkId "writeFloatArrayI",  Ext () $ Primitive writeFloatArrayI)
+  , (mkId "lengthFloatArray",  Ext () $ Primitive lengthFloatArray)
+  , (mkId "readFloatArray",  Ext () $ Primitive readFloatArray)
+  , (mkId "writeFloatArray",  Ext () $ Primitive writeFloatArray)
   , (mkId "deleteFloatArray", Ext () $ Primitive deleteFloatArray)
+  , (mkId "newRef",  Ext () $ Primitive newRef)
+  , (mkId "swapRef",  Ext () $ Primitive swapRef)
+  , (mkId "freezeRef",  Ext () $ Primitive freezeRef)
+  , (mkId "readRef", Ext () $ Primitive readRef)
   -- Additive conjunction (linear logic)
   , (mkId "with", Ext () $ Primitive $ \v -> return $ Ext () $ Primitive $ \w -> return $ Constr () (mkId "&") [v, w])
   , (mkId "projL", Ext () $ Primitive $ \(Constr () (Id "&" "&") [v, w]) -> return $ v)
@@ -980,21 +990,29 @@ builtIns =
     uniqueReturn :: RValue -> IO RValue
     uniqueReturn (Nec () v) =
       case v of
-        (Val nullSpan () False (Ext () (Runtime fa))) -> do
+        (Val nullSpan () False (Ext () (Runtime (RT.FA fa)))) -> do
           borrowed <- borrowFloatArraySafe fa
-          return $ Promote () (Val nullSpan () False (Ext () (Runtime borrowed)))
+          return $ Promote () (Val nullSpan () False (Ext () (Runtime (RT.FA borrowed))))
         _otherwise -> return $ Promote () v
     uniqueReturn v = error $ "Bug in Granule. Can't borrow a non-unique: " <> prettyDebug v
 
     uniqueBind :: (?globals :: Globals) => Ctxt RValue -> RValue -> IO RValue
     uniqueBind ctxt f = return $ Ext () $ Primitive $ \(Promote () v) ->
       case v of
-        (Val nullSpan () False (Ext () (Runtime fa))) -> do
+        (Val nullSpan () False (Ext () (Runtime (RT.FA fa)))) -> do
           copy <- copyFloatArraySafe fa
+          name <- newUnique
           evalIn ctxt
               (App nullSpan () False
                 (Val nullSpan () False f)
-                (Val nullSpan () False (Nec () (Val nullSpan () False (Ext () (Runtime copy))))))
+                (Val nullSpan () False (Pack nullSpan () (TyName (hashUnique name)) (valExpr $ Nec () $ Val nullSpan () False $ Ext () $ Runtime (RT.FA copy)) (mkId ("id" ++ show (hashUnique name))) (TyCon (mkId "Name")) (Borrow (TyCon $ mkId "Star") (TyCon $ mkId "FloatArray")))))
+        (Val nullSpan () False (Ext () (Runtime (RT.PR pr)))) -> do
+          copy <- copyRefSafe pr
+          name <- newUnique
+          evalIn ctxt
+              (App nullSpan () False
+                (Val nullSpan () False f)
+                (Val nullSpan () False (Pack nullSpan () (TyName (hashUnique name)) (valExpr $ Nec () $ Val nullSpan () False $ Ext () $ Runtime (RT.PR copy)) (mkId ("id" ++ show (hashUnique name))) (TyCon (mkId "Name")) (Borrow (TyCon $ mkId "Star") (TyCon $ mkId "Ref")))))
         _otherwise -> do
           evalIn ctxt
             (App nullSpan () False
@@ -1008,27 +1026,46 @@ builtIns =
     trustedBind :: (?globals :: Globals) => Ctxt RValue -> RValue -> IO RValue
     trustedBind ctxt f = return $ Ext () $ Primitive $ \(Promote () v) -> return $
       case v of
-        (Val nullSpan () False (Ext () (Runtime fa))) ->
+        (Val nullSpan () False (Ext () (Runtime (RT.FA fa)))) ->
           let copy = copyFloatArray' fa in
           unsafePerformIO $ evalIn ctxt
               (App nullSpan () False
                 (Val nullSpan () False f)
-                (Val nullSpan () False (Nec () (Val nullSpan () False (Ext () (Runtime copy))))))
+                (Val nullSpan () False (Nec () (Val nullSpan () False (Ext () (Runtime (RT.FA copy)))))))
         _otherwise ->
           unsafePerformIO $ evalIn ctxt
             (App nullSpan () False
              (Val nullSpan () False f)
              (Val nullSpan () False (Nec () v)))
 
-    uniquePush :: RValue -> IO RValue
-    uniquePush (Nec () (Val nullSpan () False (Constr () (Id "," ",") [x, y])))
+    withBorrow :: (?globals :: Globals) => Ctxt RValue -> RValue -> IO RValue
+    withBorrow ctxt f = return $ Ext () $ Primitive $ \(Nec () v) -> return $
+      let (Ref () v') = unsafePerformIO $ evalIn ctxt
+            (App nullSpan () False
+             (Val nullSpan () False f)
+             (Val nullSpan () False (Ref () v))) in (Nec () v')
+
+    split :: RValue -> IO RValue
+    split v = return $ Constr () (mkId ",") [v, v]
+
+    join :: RValue -> IO RValue
+    join (Constr () (Id "," ",") [Ref () (Val nullSpan () False x), Ref () (Val _ () False _)])
+     = return $ Ref () (Val nullSpan () False x)
+    join v = error $ "Bug in Granule. Can't join unborrowed types: " <> prettyDebug v
+
+    borrowPush :: RValue -> IO RValue
+    borrowPush (Ref () (Val nullSpan () False (Constr () (Id "," ",") [x, y])))
+     = return $ Constr () (mkId ",") [Ref () (Val nullSpan () False x), Ref () (Val nullSpan () False y)]
+    borrowPush (Nec () (Val nullSpan () False (Constr () (Id "," ",") [x, y])))
      = return $ Constr () (mkId ",") [Nec () (Val nullSpan () False x), Nec () (Val nullSpan () False y)]
-    uniquePush v = error $ "Bug in Granule. Can't push through a non-unique: " <> prettyDebug v
+    borrowPush v = error $ "Bug in Granule. Can't push through an unborrowed: " <> prettyDebug v
 
-    uniquePull :: RValue -> IO RValue
-    uniquePull (Constr () (Id "," ",") [Nec () (Val nullSpan () False x), Nec () (Val _ () False y)])
+    borrowPull :: RValue -> IO RValue
+    borrowPull (Constr () (Id "," ",") [Ref () (Val nullSpan () False x), Ref () (Val _ () False y)])
+      = return $ Ref () (Val nullSpan () False (Constr () (mkId ",") [x, y]))
+    borrowPull (Constr () (Id "," ",") [Nec () (Val nullSpan () False x), Nec () (Val _ () False y)])
       = return $ Nec () (Val nullSpan () False (Constr () (mkId ",") [x, y]))
-    uniquePull v = error $ "Bug in Granule. Can't pull through a non-unique: " <> prettyDebug v
+    borrowPull v = error $ "Bug in Granule. Can't pull through an unborrowed: " <> prettyDebug v
 
     recv :: (?globals :: Globals) => RValue -> IO RValue
     recv (Ext _ (Chan c)) = do
@@ -1132,52 +1169,94 @@ builtIns =
     newFloatArray :: RValue -> IO RValue
     newFloatArray = \(NumInt i) -> do
       arr <- RT.newFloatArraySafe i
-      return $ Nec () $ Val nullSpan () False $ Ext () $ Runtime arr
+      name <- newUnique
+      return $ Pack nullSpan () (TyName (hashUnique name)) (valExpr $ Nec () $ Val nullSpan () False $ Ext () $ Runtime (RT.FA arr)) (mkId ("id" ++ show (hashUnique name))) (TyCon (mkId "Name")) (Borrow (TyCon $ mkId "Star") (TyCon $ mkId "FloatArray"))
+
+    newRef :: RValue -> IO RValue
+    newRef = \v -> do
+      ref <- RT.newRefSafe v
+      name <- newUnique
+      return $ Pack nullSpan () (TyName (hashUnique name)) (valExpr $ Nec () $ Val nullSpan () False $ Ext () $ Runtime (RT.PR ref)) (mkId ("id" ++ show (hashUnique name))) (TyCon (mkId "Name")) (Borrow (TyCon $ mkId "Star") (TyCon $ mkId "Ref"))
 
     newFloatArrayI :: RValue -> IO RValue
     newFloatArrayI = \(NumInt i) -> do
       arr <- RT.newFloatArrayISafe i
-      return $ Ext () $ Runtime arr
+      return $ Ext () $ Runtime (RT.FA arr)
 
     readFloatArray :: RValue -> IO RValue
-    readFloatArray = \(Nec () (Val _ _ _ (Ext () (Runtime fa)))) -> return $ Ext () $ Primitive $ \(NumInt i) -> do
+    readFloatArray (Nec () (Val _ _ _ (Ext () (Runtime (RT.FA fa))))) = return $ Ext () $ Primitive $ \(NumInt i) -> do
+      (e,fa') <- RT.readFloatArraySafe fa i
+      return $ Constr () (mkId ",") [NumFloat e, Nec () (Val nullSpan () False $ Ext () $ Runtime (RT.FA fa'))]
+    readFloatArray (Ref () (Val _ _ _ (Ext () (Runtime (RT.FA fa))))) = return $ Ext () $ Primitive $ \(NumInt i) -> do
       (e,fa') <- RT.readFloatArraySafe fa i
-      return $ Constr () (mkId ",") [NumFloat e, Nec () (Val nullSpan () False $ Ext () $ Runtime fa')]
+      return $ Constr () (mkId ",") [NumFloat e, Ref () (Val nullSpan () False $ Ext () $ Runtime (RT.FA fa'))]
+    readFloatArray _ = error "Runtime exception: trying to read from a non-array value"
 
     readFloatArrayI :: RValue -> IO RValue
-    readFloatArrayI = \(Ext () (Runtime fa)) -> return $ Ext () $ Primitive $ \(NumInt i) -> do
+    readFloatArrayI = \(Ext () (Runtime (RT.FA fa))) -> return $ Ext () $ Primitive $ \(NumInt i) -> do
       (e,fa') <- RT.readFloatArrayISafe fa i
-      return $ Constr () (mkId ",") [NumFloat e, Ext () $ Runtime fa']
+      return $ Constr () (mkId ",") [NumFloat e, Ext () $ Runtime (RT.FA fa')]
+
+    swapRef :: RValue -> IO RValue
+    swapRef (Nec () (Val _ _ _ (Ext () (Runtime (RT.PR pr))))) = return $ Ext () $ Primitive $ \v -> do
+      (e,pr') <- RT.swapRefSafe pr v
+      return $ Constr () (mkId ",") [e, Nec () (Val nullSpan () False $ Ext () $ Runtime (RT.PR pr'))]
+    swapRef (Ref () (Val _ _ _ (Ext () (Runtime (RT.PR pr))))) = return $ Ext () $ Primitive $ \v -> do
+      (e,pr') <- RT.swapRefSafe pr v
+      return $ Constr () (mkId ",") [e, Ref () (Val nullSpan () False $ Ext () $ Runtime (RT.PR pr'))]
+    swapRef _ = error "Runtime exception: trying to swap a non-reference value"
+
+    readRef :: RValue -> IO RValue
+    readRef (Nec () (Val _ _ _ (Ext () (Runtime (RT.PR pr))))) = do
+      (e,pr') <- RT.readRefSafe pr
+      return $ Constr () (mkId ",") [e, Nec () (Val nullSpan () False $ Ext () $ Runtime (RT.PR pr'))]
+    readRef (Ref () (Val _ _ _ (Ext () (Runtime (RT.PR pr))))) = return $ Ext () $ Primitive $ \v -> do
+      (e,pr') <- RT.readRefSafe pr
+      return $ Constr () (mkId ",") [e, Ref () (Val nullSpan () False $ Ext () $ Runtime (RT.PR pr'))]
+    readRef _ = error "Runtime exception: trying to read a non-reference value"
 
     lengthFloatArray :: RValue -> IO RValue
-    lengthFloatArray = \(Nec () (Val _ _ _ (Ext () (Runtime fa)))) ->
+    lengthFloatArray (Nec () (Val _ _ _ (Ext () (Runtime (RT.FA fa))))) =
       let (e,fa') = RT.lengthFloatArray fa
-      in return $ Constr () (mkId ",") [NumInt e, Nec () (Val nullSpan () False $ Ext () $ Runtime fa')]
+      in return $ Constr () (mkId ",") [Promote () (Val nullSpan () False $ (NumInt e)), Nec () (Val nullSpan () False $ Ext () $ Runtime (RT.FA fa'))]
+    lengthFloatArray (Ref () (Val _ _ _ (Ext () (Runtime (RT.FA fa))))) =
+      let (e,fa') = RT.lengthFloatArray fa
+      in return $ Constr () (mkId ",") [Promote () (Val nullSpan () False $ (NumInt e)), Ref () (Val nullSpan () False $ Ext () $ Runtime (RT.FA fa'))]
+    lengthFloatArray _ = error "Runtime exception: trying to take the length of a non-array value"
 
     lengthFloatArrayI :: RValue -> IO RValue
-    lengthFloatArrayI = \(Ext () (Runtime fa)) ->
+    lengthFloatArrayI = \(Ext () (Runtime (RT.FA fa))) ->
       let (e,fa') = RT.lengthFloatArray fa
-      in return $ Constr () (mkId ",") [NumInt e, Ext () $ Runtime fa']
+      in return $ Constr () (mkId ",") [Promote () (Val nullSpan () False $ (NumInt e)), Ext () $ Runtime (RT.FA fa')]
 
     writeFloatArray :: RValue -> IO RValue
-    writeFloatArray = \(Nec _ (Val _ _ _ (Ext _ (Runtime fa)))) -> return $
+    writeFloatArray (Nec _ (Val _ _ _ (Ext _ (Runtime (RT.FA fa))))) = return $
       Ext () $ Primitive $ \(NumInt i) -> return $
         Ext () $ Primitive $ \(NumFloat v) -> do
           arr <- RT.writeFloatArraySafe fa i v
-          return $ Nec () $ Val nullSpan () False $ Ext () $ Runtime arr
+          return $ Nec () $ Val nullSpan () False $ Ext () $ Runtime (RT.FA arr)
+    writeFloatArray (Ref _ (Val _ _ _ (Ext _ (Runtime (RT.FA fa))))) = return $
+      Ext () $ Primitive $ \(NumInt i) -> return $
+        Ext () $ Primitive $ \(NumFloat v) -> do
+          arr <- RT.writeFloatArraySafe fa i v
+          return $ Ref () $ Val nullSpan () False $ Ext () $ Runtime (RT.FA arr)
+    writeFloatArray _ = error "Runtime exception: trying to write to a non-array value"
 
     writeFloatArrayI :: RValue -> IO RValue
-    writeFloatArrayI = \(Ext () (Runtime fa)) -> return $
+    writeFloatArrayI = \(Ext () (Runtime (RT.FA fa))) -> return $
       Ext () $ Primitive $ \(NumInt i) -> return $
       Ext () $ Primitive $ \(NumFloat v) -> do
         arr <- RT.writeFloatArrayISafe fa i v
-        return $ Ext () $ Runtime arr
+        return $ Ext () $ Runtime (RT.FA arr)
 
     deleteFloatArray :: RValue -> IO RValue
-    deleteFloatArray = \(Nec _ (Val _ _ _ (Ext _ (Runtime fa)))) -> do
+    deleteFloatArray = \(Nec _ (Val _ _ _ (Ext _ (Runtime (RT.FA fa))))) -> do
       deleteFloatArraySafe fa
       return $ Constr () (mkId "()") []
 
+    freezeRef :: RValue -> IO RValue
+    freezeRef = \(Nec _ (Val _ _ _ (Ext _ (Runtime (RT.PR pr))))) -> freezeRefSafe pr
+
 -- Convert a Granule value representation of `N n` type into an Int
 natToInt :: RValue -> Int
 natToInt (Constr () c [])  | internalName c == "Z" =  0
diff --git a/repl/granule-repl.cabal b/repl/granule-repl.cabal
index 77821f472..d3dae1717 100644
--- a/repl/granule-repl.cabal
+++ b/repl/granule-repl.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.35.2.
 --
 -- see: https://github.com/sol/hpack
 
diff --git a/runtime/src/Language/Granule/Runtime.hs b/runtime/src/Language/Granule/Runtime.hs
index 35eb22f2b..ffbc8ee71 100644
--- a/runtime/src/Language/Granule/Runtime.hs
+++ b/runtime/src/Language/Granule/Runtime.hs
@@ -2,11 +2,11 @@
 
 {-# LANGUAGE NamedFieldPuns, Strict, NoImplicitPrelude, TypeFamilies,
              DataKinds, GADTs #-}
-{-# OPTIONS_GHC -fno-full-laziness #-}
+{-# OPTIONS_GHC -fno-full-laziness -fno-warn-unused-binds #-}
 module Language.Granule.Runtime
   (
     -- Granule runtime-specific data structures
-    FloatArray(..), BenchList(..), RuntimeData
+    FloatArray(..), BenchList(..), RuntimeData(..)
 
     -- Granule runtime-specific procedures
   , pure
@@ -18,6 +18,7 @@ module Language.Granule.Runtime
   , newFloatArraySafe,newFloatArrayISafe,writeFloatArraySafe,writeFloatArrayISafe
   , readFloatArraySafe,readFloatArrayISafe,deleteFloatArraySafe,copyFloatArraySafe
   , uniquifyFloatArraySafe,borrowFloatArraySafe
+  , newRefSafe, freezeRefSafe, swapRefSafe, readRefSafe, copyRefSafe
   , cap, Cap(..), Capability(..), CapabilityType
 
   -- Re-exported from Prelude
@@ -45,9 +46,10 @@ import Data.Function (const)
 import Data.Text
 import Data.Text.IO
 import Data.Time.Clock
+import qualified Data.IORef as MR
 
 -- ^ Eventually this can be expanded with other kinds of runtime-managed data
-type RuntimeData = FloatArray
+data RuntimeData a = FA FloatArray | PR (PolyRef a)
 
 -- ^ Granule calls doubles floats
 type Float = Double
@@ -143,6 +145,11 @@ data FloatArray =
     -- | Pointer to a block of memory
     grPtr :: Ptr Float }
 
+data PolyRef a =
+  HaskellRef {
+    haskRef :: MR.IORef a
+  }
+
 {-# NOINLINE newFloatArray #-}
 newFloatArray :: Int -> FloatArray
 newFloatArray = unsafePerformIO . newFloatArraySafe
@@ -152,6 +159,15 @@ newFloatArraySafe size = do
   ptr <- callocArray size
   return $ PointerArray size ptr
 
+{-# NOINLINE newRef #-}
+newRef :: a -> PolyRef a
+newRef = unsafePerformIO . newRefSafe
+
+newRefSafe :: a -> IO (PolyRef a)
+newRefSafe v = do
+  r <- MR.newIORef v
+  return $ HaskellRef r
+
 {-# NOINLINE newFloatArrayI #-}
 newFloatArrayI :: Int -> FloatArray
 newFloatArrayI = unsafePerformIO . newFloatArrayISafe
@@ -190,6 +206,25 @@ writeFloatArrayISafe a i v =
       () <- MA.writeArray arr' i v
       return $ HaskellArray len arr'
 
+{-# NOINLINE swapRef #-}
+swapRef :: PolyRef a -> a -> (a, PolyRef a)
+swapRef r v = unsafePerformIO $ swapRefSafe r v
+
+swapRefSafe :: PolyRef a -> a -> IO (a, PolyRef a)
+swapRefSafe HaskellRef{haskRef} v = do
+  x <- MR.readIORef haskRef
+  MR.writeIORef haskRef v
+  return $ (x, HaskellRef haskRef)
+
+{-# NOINLINE readRef #-}
+readRef :: PolyRef a -> (a, PolyRef a)
+readRef = unsafePerformIO . readRefSafe
+
+readRefSafe :: PolyRef a -> IO (a, PolyRef a)
+readRefSafe HaskellRef{haskRef} = do
+  x <- MR.readIORef haskRef
+  return $ (x, HaskellRef haskRef)
+
 {-# NOINLINE readFloatArray #-}
 readFloatArray :: FloatArray -> Int -> (Float, FloatArray)
 readFloatArray a i = unsafePerformIO $ readFloatArraySafe a i
@@ -231,6 +266,14 @@ deleteFloatArraySafe PointerArray{grPtr} =
 deleteFloatArraySafe HaskellArray{grArr} =
   void (MA.mapArray (const undefined) grArr)
 
+{-# NOINLINE freezeRef #-}
+freezeRef :: PolyRef a -> a
+freezeRef = unsafePerformIO . freezeRefSafe
+
+freezeRefSafe :: PolyRef a -> IO a
+freezeRefSafe HaskellRef{haskRef} =
+  MR.readIORef haskRef
+
 {-# NOINLINE copyFloatArray' #-}
 copyFloatArray' :: FloatArray -> FloatArray
 copyFloatArray' = unsafePerformIO . copyFloatArraySafe
@@ -243,6 +286,16 @@ copyFloatArraySafe a =
       arr' <- MA.mapArray id arr
       return $ uniquifyFloatArray $ HaskellArray len arr'
 
+{-# NOINLINE copyRef #-}
+copyRef :: PolyRef a -> PolyRef a
+copyRef = unsafePerformIO . copyRefSafe
+
+copyRefSafe :: PolyRef a -> IO (PolyRef a)
+copyRefSafe HaskellRef{haskRef} = do
+  val <- MR.readIORef haskRef
+  haskRef' <- MR.newIORef val
+  return $ HaskellRef haskRef'
+
 {-# NOINLINE uniquifyFloatArray #-}
 uniquifyFloatArray :: FloatArray -> FloatArray
 uniquifyFloatArray = unsafePerformIO . uniquifyFloatArraySafe
diff --git a/server/granule-language-server.cabal b/server/granule-language-server.cabal
index 7c8c951b3..cec871ab9 100644
--- a/server/granule-language-server.cabal
+++ b/server/granule-language-server.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.35.2.
 --
 -- see: https://github.com/sol/hpack
 
diff --git a/work-in-progress/Fractional.gr b/work-in-progress/Fractional.gr
new file mode 100644
index 000000000..d56f637e1
--- /dev/null
+++ b/work-in-progress/Fractional.gr
@@ -0,0 +1,70 @@
+import Parallel
+import Vec
+import Nat
+
+data Colour = Colour (Int, (Int, Int))
+
+example' : *Colour -> (Colour, Colour)
+example' scarlet = let [s] : (Colour [0..2]) = share scarlet in
+                   let x = s in
+                   let y = s in (x, y)
+
+observe : forall {p : Permission, f : p} . & f Colour -> & f Colour
+observe x = x -- placeholder for the sake of example
+
+persimmon : *Colour -> *Colour
+persimmon c =
+  withBorrow (\b -> let (x, y) = split b;
+                         x' = observe x;
+                         f = join (x', y) in f) c
+
+mutate : & 1 Colour -> & 1 Colour
+mutate x = x -- placeholder for the sake of example
+
+viridian : *Colour -> *Colour
+viridian c =
+    withBorrow mutate c
+
+transform : & 1 Int -> & 1 Int
+transform x = x -- placeholder for the sake of example
+
+indigo : *(Int, (Int, Int)) -> *(Int, (Int, Int))
+indigo c =
+    let (r, p) = uniquePush c;
+        r' = withBorrow transform r
+        in uniquePull (r', p)
+
+-- would be much neater if we could derive push and pull for Colour
+indigo' : *(Int, (Int, Int)) -> *(Int, (Int, Int))
+indigo' c =
+    let (r, p) = uniquePush c;
+        (g, b) = uniquePush p;
+        (r', b') = par (\() -> withBorrow transform r) (\() -> withBorrow transform b);
+        p' = uniquePull (g, b') in uniquePull (r', p')
+
+amethyst : *Colour -> *Colour
+amethyst c =
+    withBorrow (\b -> let (x, y) = split b;
+                          (l, r) = split x;
+                          x' = join (l, r);
+                          f = join (x', y) in f) c
+
+test : & 2/4 Colour -> & 1/2 Colour
+test x = x
+
+arrToRefs : *FloatArray -> exists {n : Nat} . Vec n (*(Ref Float))
+arrToRefs arr = let ([l], arr') = lengthFloatArray arr in loopAR arr' [l] [0]
+
+refsToArr : forall {n : Nat} . Vec n (*(Ref Float)) -> *FloatArray
+refsToArr Nil = newFloatArray 0;
+refsToArr vec = let (l, vec') = length' vec in loopRA (newFloatArray (natToInt l)) vec' [0]
+
+loopAR : *FloatArray -> !Int -> !Int -> exists {n : Nat} . Vec n (*(Ref Float))
+loopAR arr [l] [c] = if (c == l) then let () = deleteFloatArray arr in
+        (pack <0 , Nil> as exists {n : Nat} . Vec n (*(Ref Float)))
+    else let (v, arr') = readFloatArray arr c in
+        (unpack <n , vec> = loopAR arr' [l] [c+1] in (pack <(n+1) , (Cons (newRef v) vec)> as exists {n : Nat} . Vec n (*(Ref Float))))
+
+loopRA : forall {n : Nat} . *FloatArray -> Vec n (*(Ref Float)) -> !Int -> *FloatArray
+loopRA arr Nil [_] = arr;
+loopRA arr (Cons v vec) [c] = let arr' = writeFloatArray arr c (freezeRef v) in loopRA arr' vec [c+1]
\ No newline at end of file
diff --git a/work-in-progress/oopsla-ex.gr b/work-in-progress/oopsla-ex.gr
new file mode 100644
index 000000000..5f2a52568
--- /dev/null
+++ b/work-in-progress/oopsla-ex.gr
@@ -0,0 +1,5 @@
+example : Float
+example = unpack <id , a> = newFloatArray 3 in let
+  a'       = writeFloatArray a 1 4.2;
+  (f, a'') = readFloatArray a' 1;
+  ()       = deleteFloatArray a'' in f
\ No newline at end of file
diff --git a/work-in-progress/simple-ref.gr b/work-in-progress/simple-ref.gr
new file mode 100644
index 000000000..469db32a2
--- /dev/null
+++ b/work-in-progress/simple-ref.gr
@@ -0,0 +1,14 @@
+simpleLinear : (Float, Float)
+simpleLinear = unpack <id , ref> = newRef 0.0 in let
+    (x, ref') = swapRef ref 42.0;
+    y = freezeRef ref'
+    in (x, y)
+
+simpleGraded : (Float [4], Float [2])
+simpleGraded = unpack <id , ref> = newRef test in let
+    ([x], ref') : (Float [4], *(Ref id (Float [2]))) = readRef ref;
+    [y] : Float [2] = freezeRef ref'
+    in ([x], [y])
+
+test : Float [6]
+test = [42.0]
\ No newline at end of file