diff --git a/scripts/stats.py b/scripts/stats.py
index 4702c60..0e1eb79 100755
--- a/scripts/stats.py
+++ b/scripts/stats.py
@@ -5,7 +5,7 @@ stats = {}
 acc = ''
 name = ''
 for line in open(fn):
-    if line.startswith('const'):
+    if line.startswith('const') or line.startswith('let'):
         if name: stats[name] = len(acc)
         acc = line
         name = line.split()[1]
diff --git a/src/Lib/LiftWhere.newt b/src/Lib/LiftWhere.newt
index 585410c..a9fc775 100644
--- a/src/Lib/LiftWhere.newt
+++ b/src/Lib/LiftWhere.newt
@@ -52,7 +52,7 @@ liftWhereTm name env (LetRec fc nm ty t u) = do
   modifyRef Defs (updateMap qn (Fn $ wrapLam qs t'))
 
   -- The rest
-  u' <- liftWhereTm qn env' u
+  u' <- liftWhereTm name env' u
   pure $ LetRec fc nm (Erased fc) (Erased fc) u'
   where
     -- TODO might be nice if we could nest the names (Foo.go.go) for nested where
diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt
index 3c98095..0888425 100644
--- a/src/Lib/ProcessDecl.newt
+++ b/src/Lib/ProcessDecl.newt
@@ -54,6 +54,8 @@ logMetas (Unsolved fc k ctx ty User cons :: rest) = do
       let msg = "\{env}\n  -----------\n  \{render 90 $ pprint names ty'}"
       info fc "User Hole\n\{msg}"
       logMetas rest
+-- error is reported separately
+logMetas (Unsolved fc k ctx ty ErrorHole cons :: rest) = logMetas rest
 logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
       ty' <- forceMeta ty
       tm <- quote ctx.lvl ty'