From c54b856f0be0fa91ad941636c8aad4f5d1faadee Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Fri, 20 Feb 2026 16:12:54 -0800
Subject: [PATCH] Don't allow uppercase pattern variables

---
 src/Lib/Common.newt         |  3 +++
 src/Lib/Elab.newt           |  5 ++++-
 tests/LowerPatVar.newt      |  6 ++++++
 tests/LowerPatVar.newt.fail | 10 ++++++++++
 tests/Tree.newt             |  2 +-
 5 files changed, 24 insertions(+), 2 deletions(-)
 create mode 100644 tests/LowerPatVar.newt
 create mode 100644 tests/LowerPatVar.newt.fail

diff --git a/src/Lib/Common.newt b/src/Lib/Common.newt
index 5d24add..2ae3f0f 100644
--- a/src/Lib/Common.newt
+++ b/src/Lib/Common.newt
@@ -212,3 +212,6 @@ record OpDef where
 
 Operators : U
 Operators = SortedMap String OpDef
+
+isUpperName : String → Bool
+isUpperName nm = isUpper $ strIndex nm 0
diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt
index 3e8379d..30c905e 100644
--- a/src/Lib/Elab.newt
+++ b/src/Lib/Elab.newt
@@ -1001,7 +1001,10 @@ mkPat (tm, icit) = do
                 -- Just _ => error (getFC tm) "\{show nm} is not a data constructor"
                 _ => case b of
                     -- TODO maybe check case?
-                    Nil => pure $ PatVar fc icit nm
+                    Nil =>
+                      if isUpperName nm
+                        then error (getFC tm) "\{nm} not in scope"
+                        else pure $ PatVar fc icit nm
                     _ => error (getFC tm) "patvar applied to args"
     ((RImplicit fc), Nil) => pure $ PatWild fc icit
     ((RImplicit fc), _) => error fc "implicit pat can't be applied to arguments"
diff --git a/tests/LowerPatVar.newt b/tests/LowerPatVar.newt
new file mode 100644
index 0000000..75cb5ec
--- /dev/null
+++ b/tests/LowerPatVar.newt
@@ -0,0 +1,6 @@
+module LowerPatVar
+
+import Prelude
+
+foo : Nat × Nat → Nat
+foo (ZZ , y) = Z
diff --git a/tests/LowerPatVar.newt.fail b/tests/LowerPatVar.newt.fail
new file mode 100644
index 0000000..60edb4a
--- /dev/null
+++ b/tests/LowerPatVar.newt.fail
@@ -0,0 +1,10 @@
+*** Process tests/LowerPatVar.newt
+module Prelude
+module LowerPatVar
+ERROR at tests/LowerPatVar.newt:6:6--6:8: ZZ not in scope
+  
+  foo : Nat × Nat → Nat
+  foo (ZZ , y) = Z
+       ^^
+
+ERROR at tests/LowerPatVar.newt:1:1--1:1: Compile failed
diff --git a/tests/Tree.newt b/tests/Tree.newt
index f4c2e94..859b8d3 100644
--- a/tests/Tree.newt
+++ b/tests/Tree.newt
@@ -66,7 +66,7 @@ data Sg : (A : U) -> (A -> U) -> U where
   _,_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B
 
 _*_ : U -> U -> U
-A * B = Sg A (\ _ => B)
+a * b = Sg a (\ _ => b)
 
 TooBig : Bnd -> Bnd -> Nat -> U
 TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)