Fix var bind (#449)

* Replace VarBind with Enum

* Add wildcard variant

* Fix bug

* Reenable check

* Implement hover correctly

* Small fix

lang/ast/src/decls.rs

@@ -893,8 +893,8 @@ impl Print for SelfParam {
         cfg.print_function_sugar = false;
 
         match name {
-            Some(name) => alloc
-                .text(&name.id)
+            Some(name) => name
+                .print(&cfg, alloc)
                 .append(COLON)
                 .append(alloc.space())
                 .append(typ.print(&cfg, alloc))
@@ -987,7 +987,7 @@ impl Print for Telescope {
                     if shift_and_clone(rtype, (0, 1)) == **typ && rimplicit == *implicit =>
                 {
                     // We are adding another parameter of the same type.
-                    output = output.append(alloc.space()).append(alloc.text(&name.id));
+                    output = output.append(alloc.space()).append(name.print(cfg, alloc));
                 }
                 Some((rtype, _)) => {
                     // We are adding another parameter with a different type,
@@ -1002,9 +1002,9 @@ impl Print for Telescope {
                         output = output
                             .append(IMPLICIT)
                             .append(alloc.space())
-                            .append(alloc.text(&name.id));
+                            .append(name.print(cfg, alloc));
                     } else {
-                        output = output.append(alloc.text(&name.id));
+                        output = output.append(name.print(cfg, alloc));
                     }
                 }
                 None => {
@@ -1015,7 +1015,7 @@ impl Print for Telescope {
                         output = output.append(IMPLICIT).append(alloc.space())
                     }
 
-                    output = output.append(alloc.text(&name.id));
+                    output = output.append(name.print(cfg, alloc));
                 }
             }
             running = Some((typ, *implicit));
@@ -1196,12 +1196,12 @@ impl Print for Param {
             alloc
                 .text(IMPLICIT)
                 .append(alloc.space())
-                .append(&name.id)
+                .append(name.print(cfg, alloc))
                 .append(COLON)
                 .append(alloc.space())
                 .append(typ.print(cfg, alloc))
         } else {
-            alloc.text(&name.id).append(COLON).append(alloc.space()).append(typ.print(cfg, alloc))
+            name.print(cfg, alloc).append(COLON).append(alloc.space()).append(typ.print(cfg, alloc))
         }
     }
 }

lang/ast/src/exp/local_comatch.rs

@@ -93,7 +93,7 @@ fn print_lambda_sugar<'a>(cases: &'a [Case], cfg: &PrintCfg, alloc: &'a Alloc<'a
         .name;
     alloc
         .backslash_anno(cfg)
-        .append(&var_name.id)
+        .append(var_name.print(cfg, alloc))
         .append(DOT)
         .append(alloc.space())
         .append(body.print(cfg, alloc))

lang/ast/src/exp/telescope_inst.rs

@@ -80,9 +80,9 @@ pub struct ParamInst {
 }
 
 impl Print for ParamInst {
-    fn print<'a>(&'a self, _cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
+    fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
         let ParamInst { span: _, info: _, name, typ: _, erased: _ } = self;
-        alloc.text(&name.id)
+        name.print(cfg, alloc)
     }
 }
 

lang/ast/src/ident.rs

@@ -20,27 +20,58 @@ use crate::HasSpan;
 /// E.g. on the left-hand side of a pattern or in a parameter list
 #[derive(Debug, Clone, Derivative)]
 #[derivative(Eq, PartialEq, Hash)]
-pub struct VarBind {
-    #[derivative(PartialEq = "ignore", Hash = "ignore")]
-    pub span: Option<Span>,
-    pub id: String,
+pub enum VarBind {
+    Var {
+        #[derivative(PartialEq = "ignore", Hash = "ignore")]
+        span: Option<Span>,
+        id: String,
+    },
+    Wildcard {
+        #[derivative(PartialEq = "ignore", Hash = "ignore")]
+        span: Option<Span>,
+    },
 }
 
 impl VarBind {
     pub fn from_string(id: &str) -> Self {
-        VarBind { span: None, id: id.to_owned() }
+        VarBind::Var { span: None, id: id.to_owned() }
     }
 }
 
 impl fmt::Display for VarBind {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{}", self.id)
+        match self {
+            VarBind::Var { id, .. } => write!(f, "{}", id),
+            VarBind::Wildcard { .. } => write!(f, "_"),
+        }
+    }
+}
+
+impl Print for VarBind {
+    fn print<'a>(&'a self, _cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
+        match self {
+            VarBind::Var { id, .. } => alloc.text(id),
+            VarBind::Wildcard { .. } => alloc.text(UNDERSCORE),
+        }
+    }
+}
+
+/// TODO: Remove this instance!
+impl From<VarBind> for VarBound {
+    fn from(var: VarBind) -> Self {
+        match var {
+            VarBind::Var { span, id } => VarBound { span, id },
+            VarBind::Wildcard { span } => VarBound { span, id: "_".to_string() },
+        }
     }
 }
 
 impl HasSpan for VarBind {
     fn span(&self) -> Option<Span> {
-        self.span
+        match self {
+            VarBind::Var { span, .. } => *span,
+            VarBind::Wildcard { span } => *span,
+        }
     }
 }
 
@@ -75,9 +106,9 @@ impl HasSpan for VarBound {
     }
 }
 
-impl From<VarBind> for VarBound {
-    fn from(var: VarBind) -> Self {
-        VarBound { span: var.span, id: var.id }
+impl Print for VarBound {
+    fn print<'a>(&'a self, _cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
+        alloc.text(self.id.clone())
     }
 }
 

lang/driver/src/info/data.rs

@@ -319,9 +319,9 @@ pub struct Ctx {
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Binder {
-    pub name: String,
-    pub typ: String,
+pub enum Binder {
+    Var { name: String, typ: String },
+    Wildcard { typ: String },
 }
 
 impl From<TypeCtx> for Ctx {
@@ -334,6 +334,13 @@ impl From<TypeCtx> for Ctx {
 
 impl From<TypeCtxBinder> for Binder {
     fn from(binder: TypeCtxBinder) -> Self {
-        Binder { name: binder.name.id, typ: binder.typ.print_to_string(None) }
+        match binder.name {
+            ast::VarBind::Var { id, .. } => {
+                Binder::Var { name: id, typ: binder.typ.print_to_string(None) }
+            }
+            ast::VarBind::Wildcard { .. } => {
+                Binder::Wildcard { typ: binder.typ.print_to_string(None) }
+            }
+        }
     }
 }

lang/lowering/Cargo.toml

@@ -21,6 +21,7 @@ log = { workspace = true }
 url = { workspace = true }
 
 # workspace members
+printer = { path = "../printer" }
 parser = { path = "../parser" }
 ast = { path = "../ast" }
 miette_util = { path = "../miette_util" }

lang/lowering/src/lower/decls/mod.rs

@@ -1,5 +1,3 @@
-use ast::VarBind;
-use exp::bs_to_name;
 use miette_util::ToMiette;
 use parser::cst::{self};
 
@@ -98,7 +96,7 @@ fn lower_self_param<T, F: FnOnce(&mut Ctx, ast::SelfParam) -> Result<T, Lowering
                 ctx,
                 ast::SelfParam {
                     info: Some(*span),
-                    name: name.clone().map(|name| ast::VarBind { span: None, id: name.id }),
+                    name: name.clone().map(|name| ast::VarBind::Var { span: None, id: name.id }),
                     typ: typ_ctor,
                 },
             )
@@ -154,8 +152,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 = bs_to_name(name)?;
-            let name = VarBind { span: Some(name.span), id: name.id.clone() };
+            let name = name.lower(ctx)?;
             let param_out = ast::Param { implicit: *implicit, name, typ: typ_out, erased: false };
             params_out.push(param_out);
             Ok(params_out)

lang/lowering/src/lower/exp/mod.rs

@@ -1,6 +1,5 @@
 use ast::IdBound;
 use ast::MetaVarKind;
-use ast::VarBind;
 use ast::VarBound;
 use codespan::Span;
 use num_bigint::BigUint;
@@ -13,6 +12,7 @@ use parser::cst;
 use parser::cst::decls::Telescope;
 use parser::cst::exp::BindingSite;
 use parser::cst::ident::Ident;
+use printer::Print;
 
 use crate::ctx::*;
 use crate::result::*;
@@ -46,14 +46,13 @@ fn lower_telescope_inst<T, F: FnOnce(&mut Ctx, ast::TelescopeInst) -> Result<T,
     ctx.bind_fold(
         tel_inst.iter(),
         Ok(vec![]),
-        |_ctx, params_out, param| {
+        |ctx, params_out, param| {
             let mut params_out = params_out?;
             let span = bs_to_span(param);
-            let name = bs_to_name(param)?;
             let param_out = ast::ParamInst {
                 span: Some(span),
                 info: None,
-                name: VarBind { span: Some(span), id: name.id.clone() },
+                name: param.lower(ctx)?,
                 typ: None,
                 erased: false,
             };
@@ -153,10 +152,9 @@ fn lower_args(
         ctx: &mut Ctx,
     ) -> Result<(), LoweringError> {
         let Some(arg) = given.next() else {
-            return Err(LoweringError::MissingArgForParam {
-                expected: bs_to_name(expected_bs)?.to_owned(),
-                span: span.to_miette(),
-            });
+            let expected = expected_bs.lower(ctx)?;
+            let expected = expected.print_to_string(None);
+            return Err(LoweringError::MissingArgForParam { expected, span: span.to_miette() });
         };
         match arg {
             cst::exp::Arg::UnnamedArg(exp) => {
@@ -572,26 +570,30 @@ impl Lower for cst::exp::Lam {
     }
 }
 
-pub fn bs_to_name(bs: &cst::exp::BindingSite) -> Result<Ident, LoweringError> {
-    match bs {
-        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() }),
-    }
-}
-
 fn bs_to_span(bs: &cst::exp::BindingSite) -> Span {
     match bs {
         BindingSite::Var { span, .. } => *span,
         BindingSite::Wildcard { span } => *span,
     }
 }
 
+impl Lower for cst::exp::BindingSite {
+    type Target = ast::VarBind;
+
+    fn lower(&self, _ctx: &mut Ctx) -> Result<Self::Target, LoweringError> {
+        match self {
+            BindingSite::Var { span, name } => {
+                if name.id == "Type" {
+                    Err(LoweringError::TypeUnivIdentifier { span: span.to_miette() })
+                } else {
+                    Ok(ast::VarBind::Var { span: Some(*span), id: name.id.clone() })
+                }
+            }
+            BindingSite::Wildcard { span } => Ok(ast::VarBind::Wildcard { span: Some(*span) }),
+        }
+    }
+}
+
 impl Lower for cst::exp::Motive {
     type Target = ast::Motive;
 
@@ -603,7 +605,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: param.lower(ctx)?,
                 typ: None,
                 erased: false,
             },

lang/lowering/src/result.rs

@@ -81,10 +81,10 @@ pub enum LoweringError {
         #[label]
         span: SourceSpan,
     },
-    #[error("Missing argument for parameter {}", expected.id)]
+    #[error("Missing argument for parameter {}", expected)]
     #[diagnostic(code("L-013"))]
     MissingArgForParam {
-        expected: Ident,
+        expected: String,
         #[label]
         span: SourceSpan,
     },

lang/lsp/src/hover.rs

@@ -41,15 +41,17 @@ fn ctx_to_markdown(ctx: &Ctx, value: &mut String) {
     value.push_str("**Context**\n\n");
     value.push_str("| | |\n");
     value.push_str("|-|-|\n");
-    for Binder { name, typ } in ctx.bound.iter().rev().flatten() {
-        if name == "_" {
-            continue;
+    for binder in ctx.bound.iter().rev().flatten() {
+        match binder {
+            Binder::Var { name, typ } => {
+                value.push_str("| ");
+                value.push_str(name);
+                value.push_str(" | `");
+                value.push_str(typ);
+                value.push_str("` |\n");
+            }
+            Binder::Wildcard { .. } => continue,
         }
-        value.push_str("| ");
-        value.push_str(name);
-        value.push_str(" | `");
-        value.push_str(typ);
-        value.push_str("` |\n");
     }
 }