Repository: polarity-lang/polarity (rust)

Issue:
Remove "Type" from Lexer + Parser + CST
We currently have "Type" specialcased in the Lexer + Parser + CST, but we could just treat it as an ordinary call and handle it appropriately in the lowering.

Pull request:
Remove type cst
Fixes #439 

Simplifies the parser, and is also forwards compatible if we ever want to pass arguments to type universes. (E.g. `Type(0)`, `Type(1)` etc.

Patch:
diff --git a/lang/lowering/src/lower/decls/mod.rs b/lang/lowering/src/lower/decls/mod.rs
index 0da744e8..cbb35b07 100644
--- a/lang/lowering/src/lower/decls/mod.rs
+++ b/lang/lowering/src/lower/decls/mod.rs
@@ -1,6 +1,6 @@
 use ast::VarBind;
+use exp::bs_to_name;
 use miette_util::ToMiette;
-use parser::cst::exp::BindingSite;
 use parser::cst::{self};
 
 use super::*;
@@ -154,12 +154,7 @@ where
             let mut params_out = params_out?;
             let cst::decls::Param { implicit, name, names: _, typ } = param; // The `names` field has been removed by `desugar_telescope`.
             let typ_out = typ.lower(ctx)?;
-            let name = match name {
-                BindingSite::Var { name, .. } => name.clone(),
-                BindingSite::Wildcard { span } => {
-                    parser::cst::ident::Ident { span: *span, id: "_".to_owned() }
-                }
-            };
+            let name = bs_to_name(name)?;
             let name = VarBind { span: Some(name.span), id: name.id.clone() };
             let param_out = ast::Param { implicit: *implicit, name, typ: typ_out, erased: false };
             params_out.push(param_out);
diff --git a/lang/lowering/src/lower/exp/mod.rs b/lang/lowering/src/lower/exp/mod.rs
index 08e72050..f4cb6af0 100644
--- a/lang/lowering/src/lower/exp/mod.rs
+++ b/lang/lowering/src/lower/exp/mod.rs
@@ -28,7 +28,6 @@ impl Lower for cst::exp::Exp {
             cst::exp::Exp::Call(e) => e.lower(ctx),
             cst::exp::Exp::DotCall(e) => e.lower(ctx),
             cst::exp::Exp::Anno(e) => e.lower(ctx),
-            cst::exp::Exp::TypeUniv(e) => e.lower(ctx),
             cst::exp::Exp::LocalMatch(e) => e.lower(ctx),
             cst::exp::Exp::LocalComatch(e) => e.lower(ctx),
             cst::exp::Exp::Hole(e) => e.lower(ctx),
@@ -50,7 +49,7 @@ fn lower_telescope_inst<T, F: FnOnce(&mut Ctx, ast::TelescopeInst) -> Result<T,
         |_ctx, params_out, param| {
             let mut params_out = params_out?;
             let span = bs_to_span(param);
-            let name = bs_to_name(param);
+            let name = bs_to_name(param)?;
             let param_out = ast::ParamInst {
                 span: Some(span),
                 info: None,
@@ -155,7 +154,7 @@ fn lower_args(
     ) -> Result<(), LoweringError> {
         let Some(arg) = given.next() else {
             return Err(LoweringError::MissingArgForParam {
-                expected: bs_to_name(expected_bs).to_owned(),
+                expected: bs_to_name(expected_bs)?.to_owned(),
                 span: span.to_miette(),
             });
         };
@@ -293,6 +292,15 @@ impl Lower for cst::exp::Call {
     fn lower(&self, ctx: &mut Ctx) -> Result<Self::Target, LoweringError> {
         let cst::exp::Call { span, name, args } = self;
 
+        // The type universe "Type" is treated as an ordinary call in the lexer and parser.
+        // For this reason we have to special case the logic for lowering the type universe here.
+        if name.id == "Type" {
+            if !args.is_empty() {
+                return Err(LoweringError::TypeUnivArgs { span: span.to_miette() });
+            }
+            return Ok(TypeUniv { span: Some(*span) }.into());
+        }
+
         // If we find the identifier in the local context then we have to lower
         // it to a variable.
         if let Some(idx) = ctx.lookup_local(name) {
@@ -403,15 +411,6 @@ impl Lower for cst::exp::Anno {
     }
 }
 
-impl Lower for cst::exp::TypeUniv {
-    type Target = ast::Exp;
-
-    fn lower(&self, _ctx: &mut Ctx) -> Result<Self::Target, LoweringError> {
-        let cst::exp::TypeUniv { span } = self;
-        Ok(TypeUniv { span: Some(*span) }.into())
-    }
-}
-
 impl Lower for cst::exp::LocalMatch {
     type Target = ast::Exp;
 
@@ -573,10 +572,16 @@ impl Lower for cst::exp::Lam {
     }
 }
 
-fn bs_to_name(bs: &cst::exp::BindingSite) -> Ident {
+pub fn bs_to_name(bs: &cst::exp::BindingSite) -> Result<Ident, LoweringError> {
     match bs {
-        BindingSite::Var { name, .. } => name.clone(),
-        BindingSite::Wildcard { span } => Ident { span: *span, id: "_".to_owned() },
+        BindingSite::Var { name, span } => {
+            if name.id == "Type" {
+                Err(LoweringError::TypeUnivIdentifier { span: span.to_miette() })
+            } else {
+                Ok(name.clone())
+            }
+        }
+        BindingSite::Wildcard { span } => Ok(Ident { span: *span, id: "_".to_owned() }),
     }
 }
 
@@ -598,7 +603,7 @@ impl Lower for cst::exp::Motive {
             param: ast::ParamInst {
                 span: Some(bs_to_span(param)),
                 info: None,
-                name: ast::VarBind { span: Some(bs_to_span(param)), id: bs_to_name(param).id },
+                name: ast::VarBind { span: Some(bs_to_span(param)), id: bs_to_name(param)?.id },
                 typ: None,
                 erased: false,
             },
diff --git a/lang/lowering/src/result.rs b/lang/lowering/src/result.rs
index 3d9fd132..66cfc4e5 100644
--- a/lang/lowering/src/result.rs
+++ b/lang/lowering/src/result.rs
@@ -94,6 +94,19 @@ pub enum LoweringError {
         #[label]
         span: SourceSpan,
     },
+    #[error("Type universe \"Type\" does not take arguments")]
+    #[diagnostic(code("L-015"))]
+    TypeUnivArgs {
+        #[label]
+        span: SourceSpan,
+    },
+    #[error("\"Type\" is not a valid identifier")]
+    #[diagnostic(code("L-016"))]
+    #[diagnostic(help("\"Type\" is the name of the impredicative type universe."))]
+    TypeUnivIdentifier {
+        #[label]
+        span: SourceSpan,
+    },
     #[error("An unexpected internal error occurred: {message}")]
     #[diagnostic(code("L-XXX"))]
     /// This error should not occur.
diff --git a/lang/lowering/src/symbol_table/build.rs b/lang/lowering/src/symbol_table/build.rs
index c6f94eef..2f83496b 100644
--- a/lang/lowering/src/symbol_table/build.rs
+++ b/lang/lowering/src/symbol_table/build.rs
@@ -1,4 +1,5 @@
 use ast::HashMap;
+use codespan::Span;
 use decls::*;
 use miette_util::ToMiette;
 use parser::cst::*;
@@ -19,6 +20,24 @@ pub fn build_symbol_table(module: &Module) -> Result<ModuleSymbolTable, Lowering
     Ok(symbol_table)
 }
 
+/// Checks whether the identifier is reserved or already defined.
+fn check_name(
+    symbol_table: &mut ModuleSymbolTable,
+    name: &Ident,
+    span: &Span,
+) -> Result<(), LoweringError> {
+    if name.id == "Type" {
+        return Err(LoweringError::TypeUnivIdentifier { span: span.to_miette() });
+    }
+    if symbol_table.get(name).is_some() {
+        return Err(LoweringError::AlreadyDefined {
+            name: name.to_owned(),
+            span: span.to_miette(),
+        });
+    }
+    Ok(())
+}
+
 trait BuildSymbolTable {
     fn build(&self, symbol_table: &mut ModuleSymbolTable) -> Result<(), LoweringError>;
 }
@@ -38,18 +57,12 @@ impl BuildSymbolTable for Decl {
 impl BuildSymbolTable for Data {
     fn build(&self, symbol_table: &mut ModuleSymbolTable) -> Result<(), LoweringError> {
         let Data { span, name, params, ctors, .. } = self;
-        match symbol_table.get(name) {
-            Some(_) => {
-                return Err(LoweringError::AlreadyDefined {
-                    name: name.to_owned(),
-                    span: span.to_miette(),
-                });
-            }
-            None => {
-                let meta = DeclMeta::Data { params: params.clone() };
-                symbol_table.insert(name.clone(), meta);
-            }
-        }
+
+        check_name(symbol_table, name, span)?;
+
+        let meta = DeclMeta::Data { params: params.clone() };
+        symbol_table.insert(name.clone(), meta);
+
         for ctor in ctors {
             ctor.build(symbol_table)?;
         }
@@ -60,18 +73,11 @@ impl BuildSymbolTable for Data {
 impl BuildSymbolTable for Ctor {
     fn build(&self, symbol_table: &mut ModuleSymbolTable) -> Result<(), LoweringError> {
         let Ctor { span, name, params, .. } = self;
-        match symbol_table.get(name) {
-            Some(_) => {
-                return Err(LoweringError::AlreadyDefined {
-                    name: name.to_owned(),
-                    span: span.to_miette(),
-                });
-            }
-            None => {
-                let meta = DeclMeta::Ctor { params: params.clone() };
-                symbol_table.insert(name.clone(), meta);
-            }
-        }
+        check_name(symbol_table, name, span)?;
+
+        let meta = DeclMeta::Ctor { params: params.clone() };
+        symbol_table.insert(name.clone(), meta);
+
         Ok(())
     }
 }
@@ -79,18 +85,11 @@ impl BuildSymbolTable for Ctor {
 impl BuildSymbolTable for Codata {
     fn build(&self, symbol_table: &mut ModuleSymbolTable) -> Result<(), LoweringError> {
         let Codata { span, name, params, dtors, .. } = self;
-        match symbol_table.get(name) {
-            Some(_) => {
-                return Err(LoweringError::AlreadyDefined {
-                    name: name.to_owned(),
-                    span: span.to_miette(),
-                });
-            }
-            None => {
-                let meta = DeclMeta::Codata { params: params.clone() };
-                symbol_table.insert(name.clone(), meta);
-            }
-        }
+        check_name(symbol_table, name, span)?;
+
+        let meta = DeclMeta::Codata { params: params.clone() };
+        symbol_table.insert(name.clone(), meta);
+
         for dtor in dtors {
             dtor.build(symbol_table)?;
         }
@@ -101,18 +100,11 @@ impl BuildSymbolTable for Codata {
 impl BuildSymbolTable for Dtor {
     fn build(&self, symbol_table: &mut ModuleSymbolTable) -> Result<(), LoweringError> {
         let Dtor { span, name, params, .. } = self;
-        match symbol_table.get(name) {
-            Some(_) => {
-                return Err(LoweringError::AlreadyDefined {
-                    name: name.to_owned(),
-                    span: span.to_miette(),
-                });
-            }
-            None => {
-                let meta = DeclMeta::Dtor { params: params.clone() };
-                symbol_table.insert(name.clone(), meta);
-            }
-        }
+        check_name(symbol_table, name, span)?;
+
+        let meta = DeclMeta::Dtor { params: params.clone() };
+        symbol_table.insert(name.clone(), meta);
+
         Ok(())
     }
 }
@@ -120,19 +112,11 @@ impl BuildSymbolTable for Dtor {
 impl BuildSymbolTable for Def {
     fn build(&self, symbol_table: &mut ModuleSymbolTable) -> Result<(), LoweringError> {
         let Def { span, name, params, .. } = self;
+        check_name(symbol_table, name, span)?;
+
+        let meta = DeclMeta::Def { params: params.clone() };
+        symbol_table.insert(name.clone(), meta);
 
-        match symbol_table.get(name) {
-            Some(_) => {
-                return Err(LoweringError::AlreadyDefined {
-                    name: name.to_owned(),
-                    span: span.to_miette(),
-                });
-            }
-            None => {
-                let meta = DeclMeta::Def { params: params.clone() };
-                symbol_table.insert(name.clone(), meta);
-            }
-        }
         Ok(())
     }
 }
@@ -140,19 +124,11 @@ impl BuildSymbolTable for Def {
 impl BuildSymbolTable for Codef {
     fn build(&self, symbol_table: &mut ModuleSymbolTable) -> Result<(), LoweringError> {
         let Codef { span, name, params, .. } = self;
+        check_name(symbol_table, name, span)?;
+
+        let meta = DeclMeta::Codef { params: params.clone() };
+        symbol_table.insert(name.clone(), meta);
 
-        match symbol_table.get(name) {
-            Some(_) => {
-                return Err(LoweringError::AlreadyDefined {
-                    name: name.to_owned(),
-                    span: span.to_miette(),
-                });
-            }
-            None => {
-                let meta = DeclMeta::Codef { params: params.clone() };
-                symbol_table.insert(name.clone(), meta);
-            }
-        }
         Ok(())
     }
 }
@@ -160,18 +136,11 @@ impl BuildSymbolTable for Codef {
 impl BuildSymbolTable for Let {
     fn build(&self, symbol_table: &mut ModuleSymbolTable) -> Result<(), LoweringError> {
         let Let { span, name, params, .. } = self;
-        match symbol_table.get(name) {
-            Some(_) => {
-                return Err(LoweringError::AlreadyDefined {
-                    name: name.to_owned(),
-                    span: span.to_miette(),
-                });
-            }
-            None => {
-                let meta = DeclMeta::Let { params: params.clone() };
-                symbol_table.insert(name.clone(), meta);
-            }
-        }
+        check_name(symbol_table, name, span)?;
+
+        let meta = DeclMeta::Let { params: params.clone() };
+        symbol_table.insert(name.clone(), meta);
+
         Ok(())
     }
 }
diff --git a/lang/parser/src/cst/exp.rs b/lang/parser/src/cst/exp.rs
index 570805f5..2c5ce836 100644
--- a/lang/parser/src/cst/exp.rs
+++ b/lang/parser/src/cst/exp.rs
@@ -54,7 +54,6 @@ pub enum Exp {
     Call(Call),
     DotCall(DotCall),
     Anno(Anno),
-    TypeUniv(TypeUniv),
     LocalMatch(LocalMatch),
     LocalComatch(LocalComatch),
     Hole(Hole),
@@ -69,7 +68,6 @@ impl Exp {
             Exp::Call(call) => call.span,
             Exp::DotCall(dot_call) => dot_call.span,
             Exp::Anno(anno) => anno.span,
-            Exp::TypeUniv(type_univ) => type_univ.span,
             Exp::LocalMatch(local_match) => local_match.span,
             Exp::LocalComatch(local_comatch) => local_comatch.span,
             Exp::Hole(hole) => hole.span,
@@ -105,12 +103,6 @@ pub struct Anno {
     pub typ: Box<Exp>,
 }
 
-#[derive(Debug, Clone)]
-/// The Type universe (Type in Type)
-pub struct TypeUniv {
-    pub span: Span,
-}
-
 #[derive(Debug, Clone)]
 /// Pattern match, e.g. expr.match { A => .., ..}
 pub struct LocalMatch {
diff --git a/lang/parser/src/grammar/cst.lalrpop b/lang/parser/src/grammar/cst.lalrpop
index 2848c764..b0704562 100644
--- a/lang/parser/src/grammar/cst.lalrpop
+++ b/lang/parser/src/grammar/cst.lalrpop
@@ -28,7 +28,6 @@ extern {
     "as" => Token::As,
     "comatch" => Token::Comatch,
     "absurd" => Token::Absurd,
-    "Type" => Token::Type,
     "implicit" => Token::Implicit,
     "use" => Token::Use,
 
@@ -247,11 +246,6 @@ pub Ops = {
 pub App = {
     <e: CallWithArgs> => Box::new(Exp::Call(e)),
     <e: LocalComatch> => Box::new(Exp::LocalComatch(e)),
-    Builtins,
-}
-
-pub Builtins: Box<Exp> = {
-    <e: TypeUniv> => Box::new(Exp::TypeUniv(e)),
     Holes,
 }
 
@@ -294,9 +288,6 @@ CallWithoutArgs: Call = <l: @L> <name: Ident> <r: @R> =>
 LocalComatch: LocalComatch = <l: @L> "comatch" <name: Ident?> "{" <cases: Comma<Case<Copattern>>> "}" <r: @R> =>
   LocalComatch { span: span(l, r), name, is_lambda_sugar: false, cases };
 
-TypeUniv: TypeUniv = <l: @L> "Type" <r: @R> =>
-  TypeUniv { span: span(l, r) };
-
 Hole: Hole = {
   <l: @L> "_" <r: @R> => Hole { span: span(l, r), kind: HoleKind::MustSolve },
   <l: @L> "?" <r: @R> => Hole { span: span(l, r), kind: HoleKind::CanSolve },
diff --git a/lang/parser/src/lexer/mod.rs b/lang/parser/src/lexer/mod.rs
index cfb3886e..9a90c80f 100644
--- a/lang/parser/src/lexer/mod.rs
+++ b/lang/parser/src/lexer/mod.rs
@@ -39,8 +39,6 @@ pub enum Token {
     Comatch,
     #[token("absurd")]
     Absurd,
-    #[token("Type")]
-    Type,
     #[token("implicit")]
     Implicit,
     #[token("use")]


Test patch:
diff --git a/test/suites/fail-lower/L-015.expected b/test/suites/fail-lower/L-015.expected
new file mode 100644
index 00000000..125314af
--- /dev/null
+++ b/test/suites/fail-lower/L-015.expected
@@ -0,0 +1,7 @@
+L-015
+
+  × Type universe "Type" does not take arguments
+   ╭─[L-015.pol:1:13]
+ 1 │ let foo() : Type(?) { ? }
+   ·             ───────
+   ╰────
diff --git a/test/suites/fail-lower/L-015.pol b/test/suites/fail-lower/L-015.pol
new file mode 100644
index 00000000..43a3b626
--- /dev/null
+++ b/test/suites/fail-lower/L-015.pol
@@ -0,0 +1,1 @@
+let foo() : Type(?) { ? }
\ No newline at end of file
diff --git a/test/suites/fail-lower/L-016a.expected b/test/suites/fail-lower/L-016a.expected
new file mode 100644
index 00000000..a288e910
--- /dev/null
+++ b/test/suites/fail-lower/L-016a.expected
@@ -0,0 +1,8 @@
+L-016
+
+  × "Type" is not a valid identifier
+   ╭─[L-016a.pol:1:1]
+ 1 │ data Type {}
+   · ────────────
+   ╰────
+  help: "Type" is the name of the impredicative type universe.
diff --git a/test/suites/fail-lower/L-016a.pol b/test/suites/fail-lower/L-016a.pol
new file mode 100644
index 00000000..c073f61c
--- /dev/null
+++ b/test/suites/fail-lower/L-016a.pol
@@ -0,0 +1,1 @@
+data Type {}
\ No newline at end of file
diff --git a/test/suites/fail-lower/L-016b.expected b/test/suites/fail-lower/L-016b.expected
new file mode 100644
index 00000000..ea898a97
--- /dev/null
+++ b/test/suites/fail-lower/L-016b.expected
@@ -0,0 +1,8 @@
+L-016
+
+  × "Type" is not a valid identifier
+   ╭─[L-016b.pol:1:1]
+ 1 │ codata Type {}
+   · ──────────────
+   ╰────
+  help: "Type" is the name of the impredicative type universe.
diff --git a/test/suites/fail-lower/L-016b.pol b/test/suites/fail-lower/L-016b.pol
new file mode 100644
index 00000000..5673dbfa
--- /dev/null
+++ b/test/suites/fail-lower/L-016b.pol
@@ -0,0 +1,1 @@
+codata Type {}
\ No newline at end of file
diff --git a/test/suites/fail-lower/L-016c.expected b/test/suites/fail-lower/L-016c.expected
new file mode 100644
index 00000000..5944d7bf
--- /dev/null
+++ b/test/suites/fail-lower/L-016c.expected
@@ -0,0 +1,8 @@
+L-016
+
+  × "Type" is not a valid identifier
+   ╭─[L-016c.pol:1:12]
+ 1 │ data Foo { Type : Foo }
+   ·            ───────────
+   ╰────
+  help: "Type" is the name of the impredicative type universe.
diff --git a/test/suites/fail-lower/L-016c.pol b/test/suites/fail-lower/L-016c.pol
new file mode 100644
index 00000000..fac8f0b1
--- /dev/null
+++ b/test/suites/fail-lower/L-016c.pol
@@ -0,0 +1,1 @@
+data Foo { Type : Foo }
\ No newline at end of file
diff --git a/test/suites/fail-lower/L-016d.expected b/test/suites/fail-lower/L-016d.expected
new file mode 100644
index 00000000..b51d167d
--- /dev/null
+++ b/test/suites/fail-lower/L-016d.expected
@@ -0,0 +1,9 @@
+L-016
+
+  × "Type" is not a valid identifier
+   ╭─[L-016d.pol:2:14]
+ 1 │ data Bool { T, F }
+ 2 │ codata Foo { .Type : Bool }
+   ·              ────────────
+   ╰────
+  help: "Type" is the name of the impredicative type universe.
diff --git a/test/suites/fail-lower/L-016d.pol b/test/suites/fail-lower/L-016d.pol
new file mode 100644
index 00000000..45141680
--- /dev/null
+++ b/test/suites/fail-lower/L-016d.pol
@@ -0,0 +1,2 @@
+data Bool { T, F }
+codata Foo { .Type : Bool }
\ No newline at end of file
diff --git a/test/suites/fail-lower/L-016e.expected b/test/suites/fail-lower/L-016e.expected
new file mode 100644
index 00000000..daa4d398
--- /dev/null
+++ b/test/suites/fail-lower/L-016e.expected
@@ -0,0 +1,9 @@
+L-016
+
+  × "Type" is not a valid identifier
+   ╭─[L-016e.pol:2:1]
+ 1 │ data Bool { T, F }
+ 2 │ let Type : Bool { T }
+   · ─────────────────────
+   ╰────
+  help: "Type" is the name of the impredicative type universe.
diff --git a/test/suites/fail-lower/L-016e.pol b/test/suites/fail-lower/L-016e.pol
new file mode 100644
index 00000000..b4fe5d60
--- /dev/null
+++ b/test/suites/fail-lower/L-016e.pol
@@ -0,0 +1,2 @@
+data Bool { T, F }
+let Type : Bool { T }
\ No newline at end of file
diff --git a/test/suites/fail-lower/L-016f.expected b/test/suites/fail-lower/L-016f.expected
new file mode 100644
index 00000000..c6f32a05
--- /dev/null
+++ b/test/suites/fail-lower/L-016f.expected
@@ -0,0 +1,9 @@
+L-016
+
+  × "Type" is not a valid identifier
+   ╭─[L-016f.pol:1:9]
+ 1 │ let foo(Type: Type): Type {
+   ·         ────
+ 2 │    Type
+   ╰────
+  help: "Type" is the name of the impredicative type universe.
diff --git a/test/suites/fail-lower/L-016f.pol b/test/suites/fail-lower/L-016f.pol
new file mode 100644
index 00000000..cb3ffb4f
--- /dev/null
+++ b/test/suites/fail-lower/L-016f.pol
@@ -0,0 +1,3 @@
+let foo(Type: Type): Type {
+   Type
+}
\ No newline at end of file