diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt
index df1d98e..0f5a657 100644
--- a/src/Lib/Elab.newt
+++ b/src/Lib/Elab.newt
@@ -490,7 +490,7 @@ unify env mode t u = do
           vtm <- eval Nil CBN tm
           appvtm <- vappSpine vtm sp'
           unify env mode t appvtm
-        _ => error fc' "unify failed \{show t} =?= \{show u} (no Fn :: Nil)\n  env is \{show env}"
+        _ => error fc' "unify failed \{show t} =?= \{show u} [no Fn]\n  env is \{show env}"
 
     unifyRef t@(VRef fc k sp) u = do
       debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}"
@@ -500,7 +500,7 @@ unify env mode t u = do
           vtm <- eval Nil CBN tm
           tmsp <- vappSpine vtm sp
           unify env mode tmsp u
-        _ => error fc "unify failed \{show t} (no Fn :: Nil) =?= \{show u}\n  env is \{show env}"
+        _ => error fc "unify failed \{show t} [no Fn] =?= \{show u}\n  env is \{show env}"
     unifyRef t u = unifyRest t u
 
     unifyVar : Val -> Val -> M UnifyResult
diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt
index bfb14cb..74eb7d2 100644
--- a/src/Lib/Types.newt
+++ b/src/Lib/Types.newt
@@ -259,7 +259,7 @@ instance Show Val where
   show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> Nil)})"
   show (VRef _ nm Lin) = show nm
   show (VRef _ nm sp) = "(\{show nm} \{unwords $ map show (sp <>> Nil)})"
-  show (VMeta _ ix sp) = "(%meta \{show ix} (\{show $ snoclen sp} sp :: Nil))"
+  show (VMeta _ ix sp) = "(%meta \{show ix} [\{show $ snoclen sp} sp])"
   show (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{showClosure x})"
   show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show  x}}. \{showClosure  y})"
   show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show  x}). \{showClosure  y})"
@@ -272,7 +272,7 @@ instance Show Val where
   show (VErased _) = "ERASED"
 
 
-showClosure (MkClosure xs t) = "(%cl (\{show $ length xs} env :: Nil) \{show t})"
+showClosure (MkClosure xs t) = "(%cl [\{show $ length xs} env] \{show t})"
 
 -- instance Show Closure where
 --   show = showClosure