diff --git a/Ivor/CtxtTT.lhs b/Ivor/CtxtTT.lhs
--- a/Ivor/CtxtTT.lhs
+++ b/Ivor/CtxtTT.lhs
@@ -36,7 +36,10 @@
 > tt (Right v) = Right v
 
 > getError :: IError -> TTError
-> getError (ICantUnify l r) = CantUnify (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))
+> getError (ICantUnify l r) -- = CantUnify (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))
+
+>                           = Message $ "Can't unify " ++ show (view (Term (l, Ind TTCore.Star))) ++ "  and " ++ show (view (Term (r, Ind TTCore.Star)))
+
 > getError (INotConvertible l r) = NotConvertible (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))
 > getError (IMessage s) = Message s
 > getError (IUnbound clause clty rhs rhsty names) 
diff --git a/Ivor/Nobby.lhs b/Ivor/Nobby.lhs
--- a/Ivor/Nobby.lhs
+++ b/Ivor/Nobby.lhs
@@ -74,6 +74,7 @@
 >     where bty = eval stage gamma g ty
 >  eval stage gamma g (Const x) = (MR (RdConst x))
 >  eval stage gamma g Star = MR RdStar
+>  eval stage gamma g LinStar = MR RdLinStar
 >  eval stage gamma g Erased = MR RdErased
 >  eval stage gamma (VG g) (Bind n (B Lambda ty) (Sc sc)) =
 >      (MR (RdBind n (B Lambda (eval stage gamma (VG g) ty))
@@ -239,6 +240,7 @@
 >     weakenp i (RdBind n bind sc) = RdBind n (weakenp i bind) (weakenp i sc)
 >     weakenp i (RdConst x) = RdConst x
 >     weakenp i RdStar = RdStar
+>     weakenp i RdLinStar = RdLinStar
 >     weakenp i RdErased = RdErased
 >     weakenp i (RCon t n sp) = RCon t n (fmap (weakenp i) sp)
 >     weakenp i (RTyCon n sp) = RTyCon n (fmap (weakenp i) sp)
@@ -294,6 +296,7 @@
 > instance Quote (Ready Kripke) (Ready Scope) where
 >     quote' ns (RdConst x) = RdConst x
 >     quote' ns RdStar = RdStar
+>     quote' ns RdLinStar = RdLinStar
 >     quote' ns RdErased = RdErased
 >     quote' ns (RdBind n b@(B _ ty) sc)
 >             = let n' = mkUnique n ns in
@@ -390,6 +393,7 @@
 >     forget (RdBind n b (Sc sc)) = Bind n (forget b) (Sc (forget sc))
 >     forget (RdConst x) = (Const x)
 >     forget RdStar = Star
+>     forget RdLinStar = LinStar
 >     forget RdErased = Erased
 >     forget (RCon t c sp) = makeApp (Con t c (size sp)) (fmap forget sp)
 >     forget (RTyCon c sp) = makeApp (TyCon c (size sp)) (fmap forget sp)
diff --git a/Ivor/TTCore.lhs b/Ivor/TTCore.lhs
--- a/Ivor/TTCore.lhs
+++ b/Ivor/TTCore.lhs
@@ -22,6 +22,7 @@
 >     | RBind Name (Binder Raw) Raw
 >     | forall c.(Constant c) => RConst !c
 >     | RStar
+>     | RLinStar
 >     | RInfer -- Term to be inferred by the typechecker
 >     | RMeta Name -- a metavariable, to be implemented separately
 >     | RLabel Raw RComputation
@@ -30,6 +31,8 @@
 >     | RAnnot String -- Debugging hack
 >     | RFileLoc FilePath Int Raw -- For more helpful type error messages
 >     | RStage RStage
+>     | RLin Raw -- linear value
+>     | RLinTy Raw -- linear type
 
 > data RComputation = RComp Name [Raw]
 >   deriving Eq
@@ -59,6 +62,9 @@
 >     | Return (TT n)
 >     | forall c. Constant c => Const !c
 >     | Star
+>     | LinStar
+>     | Lin (TT n)
+>     | LinTy (TT n)
 >     | Stage (Stage n)
 >     | Erased -- Forced, so deleted
 
@@ -86,6 +92,7 @@
 > data Bind n
 >     = Lambda
 >     | Pi
+>     | LinPi
 >     | Let n
 >     | Hole
 >     | Guess n
@@ -257,7 +264,10 @@
 >     fmap f (Call c t) = Call (fmap f c) (fmap f t)
 >     fmap f (Return t) = Return (fmap f t)
 >     fmap f (Stage t) = Stage (fmap f t)
+>     fmap f (Lin t) = Lin (fmap f t)
+>     fmap f (LinTy t) = LinTy (fmap f t)
 >     fmap f Star = Star
+>     fmap f LinStar = LinStar
 
 > instance Functor Stage where
 >     fmap f (Quote t) = Quote (fmap f t)
@@ -319,6 +329,8 @@
 >         = Call (Comp n (fmap (v' ctx) cs)) (v' ctx t)
 >     v' ctx (Return t) = Return (v' ctx t)
 >     v' ctx (Stage t) = Stage (sLift (v' ctx) t)
+>     v' ctx (Lin t) = Lin (v' ctx t)
+>     v' ctx (LinTy t) = LinTy (v' ctx t)
 >     v' ctx x = x
 
 > indexise :: Levelled n -> Indexed n
@@ -345,6 +357,8 @@
 >         = Call (Comp n (fmap (v') cs)) (v' t)
 >     v' (Return t) = Return (v' t)
 >     v' (Stage t) = Stage (sLift (v') t)
+>     v' (Lin t) = Lin (v' t)
+>     v' (LinTy t) = LinTy (v' t)
 >     v' x = x
 
 FIXME: This needs to rename all duplicated binder names first, otherwise
@@ -397,6 +411,12 @@
 > uniqifyAllState (Stage t) =
 >     do t' <- sLiftM uniqifyAllState t
 >        return (Stage t')
+> uniqifyAllState (Lin t) =
+>     do t' <- uniqifyAllState t
+>        return (Lin t')
+> uniqifyAllState (LinTy t) =
+>     do t' <- uniqifyAllState t
+>        return (LinTy t')
 > uniqifyAllState x = return $ x
 
 > uniqifyAllStateB (B Lambda ty) =
@@ -405,6 +425,9 @@
 > uniqifyAllStateB (B Pi ty) =
 >     do ty' <- uniqifyAllState ty
 >        return (B Pi ty')
+> uniqifyAllStateB (B LinPi ty) =
+>     do ty' <- uniqifyAllState ty
+>        return (B LinPi ty')
 > uniqifyAllStateB (B Hole ty) =
 >     do ty' <- uniqifyAllState ty
 >        return (B Hole ty')
@@ -714,6 +737,7 @@
 >                                    Just x' -> x'==y
 >                                    Nothing -> False
 >     (==) RStar RStar = True
+>     (==) RLinStar RLinStar = True
 >     (==) (RLabel t (RComp n cs)) (RLabel t' (RComp n' cs')) =
 >         t==t' && n==n' && cs == cs'
 >     (==) (RCall (RComp n cs) t) (RCall (RComp n' cs') t') =
@@ -747,6 +771,7 @@
 >                                   Just x' -> x'==y
 >                                   Nothing -> False
 >     (==) Star Star = True
+>     (==) LinStar LinStar = True
 >     (==) (Label t (Comp n cs)) (Label t' (Comp n' cs')) =
 >         t==t' -- && n==n' && cs == cs'
 >     (==) (Call (Comp n cs) t) (Call (Comp n' cs') t') =
@@ -808,6 +833,7 @@
 >       fPrec _ (RStage (REscape t)) = "~" ++ fPrec 0 t
 >       fPrec _ (RConst x) = show x
 >       fPrec _ (RStar) = "*"
+>       fPrec _ (RLinStar) = "!*"
 >       fPrec _ (RInfer) = "_"
 >       fPrec _ (RMeta n) = "[?"++forget n++"]"
 >       fPrec p (RFileLoc f l t) = fPrec p t
@@ -873,6 +899,7 @@
 >        forgetTT (Stage t) = RStage (forget t)
 >        forgetTT (Const x) = RConst x
 >        forgetTT Star = RStar
+>        forgetTT LinStar = RLinStar
 >        forgetTT Erased = RInfer
 
 > instance (Show n) => Forget (TT n) Raw where
@@ -915,6 +942,7 @@
 >        forgetTT (Stage t) = RStage (forget t)
 >        forgetTT (Const x) = RConst x
 >        forgetTT Star = RStar
+>        forgetTT LinStar = RLinStar
 >        forgetTT Erased = RInfer
 
 > instance Show n => Forget (Stage n) RStage where
@@ -1042,4 +1070,5 @@
 > pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t)
 > pToV2 v p (Const x) = Sc (Const x)
 > pToV2 v p Star = Sc Star
+> pToV2 v p LinStar = Sc LinStar
 > pToV2 v p Erased = Sc Erased
diff --git a/Ivor/Typecheck.lhs b/Ivor/Typecheck.lhs
--- a/Ivor/Typecheck.lhs
+++ b/Ivor/Typecheck.lhs
@@ -141,12 +141,13 @@
 >                  let y' = papp s' y
 >                  let (Ind y'') = -- trace ("Unifying with " ++ show x' ++ " and " ++ show (papp s' y) ++ "[" ++ show (x,y) ++ "]") $ 
 >                                 eval_nf gam (Ind (papp s' y))
+>                  let (Ind x'') = eval_nf gam (Ind (papp s' x))
 >                  uns <- case unifyenvErr ok gam env (Ind y') (Ind x') of
 >                           Right uns -> return uns
 >                           Left err -> -- trace (showeqn all) $
 >                             case unifyenvErr ok gam env (Ind y'') (Ind x') of
 >                               Right uns -> return uns
->                               Left err -> ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))
+>                               Left err -> ifail (errCtxt fc (ICantUnify (Ind y'') (Ind x'')))
 
                          Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms
 
@@ -416,6 +417,7 @@
 >                         return (rv,rt)
 >  tc env lvl (RConst x) _ = lift $ tcConst x
 >  tc env lvl RStar _ = return (Ind Star, Ind Star)
+>  tc env lvl RLinStar _ = return (Ind LinStar, Ind Star)
 >  tc env lvl (RFileLoc f l t) exp = 
 >     do (next, infer, bindings, errs, mvs, fc) <- get
 >        put (next, infer, bindings, errs, mvs, Just (FC f l))
@@ -567,13 +569,14 @@
 >     let (Ind tvnf) = eval_nf_env env gamma (Ind tv)
 >     let ttnf = -- trace ("PI: " ++ show (tv, tvnf, debugTT tv)) $ 
 >                eval_nf_env env gamma (Ind tt)
->     checkConvSt env gamma ttnf (Ind Star)
+>     -- checkConvSt env gamma ttnf (Ind AnyKind)
+>     case ttnf of
+>       (Ind Star) -> return (B Pi tv)
+>       (Ind LinStar) -> return (B Pi tv)
+>       (Ind (P (MN ("INFER",_)))) -> return (B Pi tv)
+>       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
 >     return (B Pi tvnf)
 
-     case ttnf of
-       (Ind Star) -> return (B Pi tv)
-       (Ind (P (MN ("INFER",_)))) -> return (B Pi tv)
-       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
 
 >  checkbinder gamma env lvl n (B (Let v) RInfer) = do
 >     (Ind vv,Ind vt) <- tcfixup env lvl v Nothing
@@ -710,7 +713,10 @@
 >    let lv = Bind n (B Lambda t) scv
 >    return (Ind lv,Ind lt)
 > discharge gamma n (B Pi t) scv (Sc sct) = do
->    checkConvSt [] gamma (Ind Star) (Ind sct)
+>    case sct of
+>      Star -> return ()
+>      LinStar -> return ()
+>      _ -> checkConvSt [] gamma (Ind Star) (Ind sct)
 >    let lt = Star
 >    let lv = Bind n (B Pi t) scv
 >    return (Ind lv,Ind lt)
diff --git a/Ivor/Values.lhs b/Ivor/Values.lhs
--- a/Ivor/Values.lhs
+++ b/Ivor/Values.lhs
@@ -191,6 +191,7 @@
 >     | RTyCon Name (Spine (Model s))
 >     | forall c. Constant c => RdConst c
 >     | RdStar
+>     | RdLinStar
 >     | RdErased
 >     | RdLabel (Model s) (MComp s)
 >     | RdCall (MComp s) (Model s)
diff --git a/Ivor/ViewTerm.lhs b/Ivor/ViewTerm.lhs
--- a/Ivor/ViewTerm.lhs
+++ b/Ivor/ViewTerm.lhs
@@ -77,6 +77,7 @@
 >     | Return { returnterm :: ViewTerm }
 >     | forall c. Constant c => Constant c
 >     | Star
+>     | LinStar
 >     | Quote { quotedterm :: ViewTerm } -- ^ Staging annotation
 >     | Code { codetype :: ViewTerm } -- ^ Staging annotation
 >     | Eval { evalterm :: ViewTerm } -- ^ Staging annotation
@@ -114,6 +115,7 @@
 >     (==) (Ivor.ViewTerm.Call _ _ t) (Ivor.ViewTerm.Call _ _ t') = t == t'
 >     (==) (Ivor.ViewTerm.Return t) (Ivor.ViewTerm.Return t') = t==t'
 >     (==) Ivor.ViewTerm.Star Ivor.ViewTerm.Star = True
+>     (==) Ivor.ViewTerm.LinStar Ivor.ViewTerm.LinStar = True
 >     (==) Placeholder Placeholder = True
 >     (==) (Metavar x) (Metavar y) = x == y
 >     (==) (Constant x) (Constant y) = case cast x of
@@ -163,6 +165,7 @@
 >     forget (Ivor.ViewTerm.Return ty) = RReturn (forget ty)
 >     forget (Constant c) = RConst c
 >     forget (Ivor.ViewTerm.Star) = TTCore.RStar
+>     forget (Ivor.ViewTerm.LinStar) = TTCore.RLinStar
 >     forget Placeholder = RInfer
 >     forget (Metavar x) = RMeta x
 >     forget (Ivor.ViewTerm.Quote t) = RStage (RQuote (forget t))
@@ -215,6 +218,7 @@
 >         Ivor.ViewTerm.Let n (vtaux ctxt ty) (vtaux ctxt val) (vtaux (n:ctxt) sc)
 >     vtaux ctxt (Const c) = Constant c
 >     vtaux ctxt TTCore.Star = Ivor.ViewTerm.Star
+>     vtaux ctxt TTCore.LinStar = Ivor.ViewTerm.LinStar
 >     vtaux ctxt (TTCore.Label ty (Comp n ts)) =
 >         Ivor.ViewTerm.Label n (fmap (vtaux ctxt) ts) (vtaux ctxt ty)
 >     vtaux ctxt (TTCore.Call (Comp n ts) ty) =
diff --git a/ivor.cabal b/ivor.cabal
--- a/ivor.cabal
+++ b/ivor.cabal
@@ -1,5 +1,5 @@
 Name:		ivor
-Version:	0.1.14
+Version:	0.1.14.1
 Author:		Edwin Brady
 License:	BSD3
 License-file:	LICENSE