diff --git a/port/Lib/Elab.newt b/port/Lib/Elab.newt
index c4b3181..f8f3d5d 100644
--- a/port/Lib/Elab.newt
+++ b/port/Lib/Elab.newt
@@ -1361,7 +1361,7 @@ check ctx tm ty = do
           pure $ MkClause (getFC pat) ((scnm, pat') :: Nil) Nil rawRHS
       -- buildCase expects scrutinee to be a name in the context, so we need to let it.
       -- if it's a Bnd and not shadowed we could skip the let, but that's messy.
-      let ctx' = extend ctx scnm scty
+      let ctx' = withPos (extend ctx scnm scty) (getFC tm)
       tree <- buildTree ctx' $ MkProb clauses ty
       pure $ Let fc scnm sc tree