@@ -91,26 +91,32 @@ fn is_unit_arg(expr: &ast::Expr) -> bool {
9191}
9292
9393/// Map a value-spine unit argument to its `UnitExpr` AST.
94−fn unit_arg_to_ast(expr: &ast::Expr) -> ast::UnitExpr {
95− match &expr.node {
96− ast::ExprKind::Lit(ast::Literal::Int(n)) if n == "1" => ast::UnitExpr::Dimensionless,
97− ast::ExprKind::Constructor(name) => ast::UnitExpr::Named(name.clone()),
94+fn unit_arg_to_ast(expr: &ast::Expr) -> ast::Type {
95+ let span = expr.span;
96+ let node = match &expr.node {
97+ ast::ExprKind::Lit(ast::Literal::Int(n)) if n == "1" => {
98+ ast::TypeKind::Unit(ast::UnitExpr::Dimensionless)
99+ }
100+ ast::ExprKind::Constructor(name) => {
101+ ast::TypeKind::Unit(ast::UnitExpr::Named(name.clone()))
102+ }
98103 ast::ExprKind::Var(ast::Binding::User(name)) => {
99− ast::UnitExpr::Named(name.clone())
104+ ast::TypeKind::Unit(ast::UnitExpr::Named(name.clone()))
100105 }
101− ast::ExprKind::TypeHole => ast::UnitExpr::Hole,
106+ ast::ExprKind::TypeHole => ast::TypeKind::Unit(ast::UnitExpr::Hole),
102107 // Compound unit in value-spine form: `(M / S)` arrives as a `BinOp`.
103108 ast::ExprKind::BinOp { op, lhs, rhs } => {
104109 let l = unit_arg_to_ast(lhs);
105110 let r = unit_arg_to_ast(rhs);
106111 match op {
107− ast::BinOp::Mul => ast::UnitExpr::Mul(Box::new(l), Box::new(r)),
108− ast::BinOp::Div => ast::UnitExpr::Div(Box::new(l), Box::new(r)),
109− _ => ast::UnitExpr::Dimensionless,
112+ ast::BinOp::Mul => ast::TypeKind::UnitMul(Box::new(l), Box::new(r)),
113+ ast::BinOp::Div => ast::TypeKind::UnitDiv(Box::new(l), Box::new(r)),
114+ _ => ast::TypeKind::Unit(ast::UnitExpr::Dimensionless),
110115 }
111116 }
112− _ => ast::UnitExpr::Dimensionless,
113− }
117+ _ => ast::TypeKind::Unit(ast::UnitExpr::Dimensionless),
118+ };
119+ ast::Spanned::new(node, span)
114120}
115121
116122// ── Monad info (shared with codegen) ──────────────────────────────
@@ -2094,6 +2100,29 @@ impl Infer {
20942100 }
20952101 }
20962102
2103+ /// Interpret a unit-shaped type argument of `Int`/`Float` as a unit.
2104+ /// Returns `Some` only when the argument is built entirely from unit atoms
2105+ /// (`Unit`) and unit algebra (`UnitMul`/`UnitDiv`); any other type (`Record`,
2106+ /// `Function`, a real type `App`, …) yields `None` so the caller falls back
2107+ /// to ordinary type application. This is the single place that knows the
2108+ /// argument of `Int`/`Float` is a unit dimension.
2109+ fn ast_type_to_unit_ty(&mut self, ty: &ast::Type) -> Option<UnitTy> {
2110+ match &ty.node {
2111+ ast::TypeKind::Unit(u) => Some(self.ast_unit_to_unit_ty(u)),
2112+ ast::TypeKind::UnitMul(a, b) => {
2113+ let a = self.ast_type_to_unit_ty(a)?;
2114+ let b = self.ast_type_to_unit_ty(b)?;
2115+ Some(a.mul(&b))
2116+ }
2117+ ast::TypeKind::UnitDiv(a, b) => {
2118+ let a = self.ast_type_to_unit_ty(a)?;
2119+ let b = self.ast_type_to_unit_ty(b)?;
2120+ Some(a.div(&b))
2121+ }
2122+ _ => None,
2123+ }
2124+ }
2125+
20972126 fn error(&mut self, msg: String, span: Span) {
20982127 // Dedup identical diagnostics: the alias fixpoint and multi-pass
20992128 // collection can re-derive the same error at the same span several
@@ -4608,22 +4637,25 @@ impl Infer {
46084637 // A numeric base as a type argument. Optionally followed by a
46094638 // unit argument (`1`, a unit atom like `Ms`, or a unit var) —
46104639 // `Float 1`, `Int Ms`. Bare (no unit) means dimensionless.
4611− let unit = match spine.get(consumed) {
4640+ // Built as ordinary application `App(Int, unit)`; the `App`
4641+ // normalization in `ast_type_to_ty` produces the unit-bearing
4642+ // `Con("Int", [Unit(..)])`.
4643+ match spine.get(consumed) {
46124644 Some(u_expr) if is_unit_arg(u_expr) => {
46134645 consumed += 1;
46144646 // The unit argument is erased with the type: record its
46154647 // span so codegen drops it from the value spine.
46164648 self.type_arg_spans.insert(u_expr.span);
4617− unit_arg_to_ast(u_expr)
4649+ let base = knot::ast::Spanned {
4650+ node: TypeKind::Named(name.clone()),
4651+ span: head.span,
4652+ };
4653+ TypeKind::App {
4654+ func: Box::new(base),
4655+ arg: Box::new(unit_arg_to_ast(u_expr)),
4656+ }
46184657 }
4619− _ => knot::ast::UnitExpr::Dimensionless,
4620− };
4621− TypeKind::UnitAnnotated {
4622− base: Box::new(knot::ast::Spanned {
4623− node: TypeKind::Named(name.clone()),
4624− span: head.span,
4625− }),
4626− unit,
4658+ _ => TypeKind::Named(name.clone()),
46274659 }
46284660 } else {
46294661 TypeKind::Named(name.clone())
@@ -4818,6 +4850,34 @@ impl Infer {
48184850 if let Some(t) = self.expand_param_alias(ty) {
48194851 return t;
48204852 }
4853+ // Unit normalization (the ONLY unit-aware front-end step): an
4854+ // `Int`/`Float` applied to a unit-shaped argument — `Int M`,
4855+ // `Float u`, `Int 1`, `Int (M / S)` — becomes the canonical
4856+ // unit-bearing type `Con("Int"/"Float", [Unit(u)])`. The
4857+ // argument is interpreted as unit algebra; see `ast_type_to_unit_ty`.
4858+ if let ast::TypeKind::Named(n) = &func.node
4859+ && (n == "Int" || n == "Float")
4860+ && let Some(unit_ty) = self.ast_type_to_unit_ty(arg)
4861+ {
4862+ let saved_flag = self.in_type_annotation;
4863+ let saved_enforce = self.enforce_units;
4864+ self.in_type_annotation = false;
4865+ self.enforce_units = false;
4866+ let base_ty = self.ast_type_to_ty(func);
4867+ self.in_type_annotation = saved_flag;
4868+ self.enforce_units = saved_enforce;
4869+ return match base_ty {
4870+ Ty::Int => Ty::int_with_unit(unit_ty),
4871+ Ty::Float => Ty::float_with_unit(unit_ty),
4872+ _ => {
4873+ self.error(
4874+ "unit annotations are only allowed on Int and Float types".into(),
4875+ ty.span,
4876+ );
4877+ Ty::Error
4878+ }
4879+ };
4880+ }
48214881 let arg_ty = self.ast_type_to_ty(arg);
48224882 let func_ty = self.ast_type_to_ty(func);
48234883 match func_ty {
@@ -4857,35 +4917,20 @@ impl Infer {
48574917 Ty::Variant(ctor_tys, row_var)
48584918 }
48594919 ast::TypeKind::IO { ty: inner_ty } => Ty::IO(Box::new(self.ast_type_to_ty(inner_ty))),
4860− ast::TypeKind::UnitAnnotated { base, unit } => {
4861− // Convert the base (`Int`/`Float`) without the bare-numeric
4862− // check — the unit is supplied right here.
4863− let saved_flag = self.in_type_annotation;
4864− let saved_enforce = self.enforce_units;
4865− self.in_type_annotation = false;
4866− self.enforce_units = false;
4867− let base_ty = self.ast_type_to_ty(base);
4868− self.in_type_annotation = saved_flag;
4869− self.enforce_units = saved_enforce;
4870− let unit_ty = self.ast_unit_to_unit_ty(unit);
4871− match base_ty {
4872− Ty::Int => Ty::int_with_unit(unit_ty),
4873− Ty::Float => Ty::float_with_unit(unit_ty),
4874− _ => {
4875− self.error(
4876− "unit annotations are only allowed on Int and Float types".into(),
4877− ty.span,
4878− );
4879− Ty::Error
4880− }
4881− }
4882− }
48834920 ast::TypeKind::Unit(_unit) => {
4884− // A standalone type-level unit expression. Only meaningful as
4885− // the argument of `Con("Int"/"Float", [Unit(u)])`, which is
4886− // built via `UnitAnnotated`. Reaching here means the unit
4887− // appeared bare in a type position — treat it as an error
4888− // since a unit is not a value-inhabited type.
4921+ // A standalone type-level unit atom. Only meaningful as the
4922+ // argument of `Int`/`Float` (handled by the `App` unit
4923+ // normalization). Reaching here means the unit appeared bare in
4924+ // a type position — an error, since a unit is not a
4925+ // value-inhabited type.
4926+ self.error(
4927+ "a unit expression cannot appear as a standalone type — it must be the argument of Int or Float".into(),
4928+ ty.span,
4929+ );
4930+ Ty::Error
4931+ }
4932+ ast::TypeKind::UnitMul(..) | ast::TypeKind::UnitDiv(..) => {
4933+ // Unit algebra outside an `Int`/`Float` argument.
48894934 self.error(
48904935 "a unit expression cannot appear as a standalone type — it must be the argument of Int or Float".into(),
48914936 ty.span,
@@ -7441,7 +7486,17 @@ impl Infer {
74417486 break;
74427487 };
74437488 let Some(ty_ast) = first_ty.take() else { break };
7489+ // A type WITNESS argument is written in
7490+ // value position (`asT (Maybe Int) …`), so
7491+ // the unit annotation requirement does not
7492+ // apply — suppress it while interpreting.
7493+ let saved_flag = self.in_type_annotation;
7494+ let saved_enforce = self.enforce_units;
7495+ self.in_type_annotation = false;
7496+ self.enforce_units = false;
74447497 let arg_ty = self.ast_type_to_ty(&ty_ast);
7498+ self.in_type_annotation = saved_flag;
7499+ self.enforce_units = saved_enforce;
74457500 self.type_arg_spans.insert(ty_ast.span);
74467501 let mut mapping: HashMap<TyVar, Ty> = HashMap::new();
74477502 mapping.insert(witness_var, arg_ty);
@@ -7502,7 +7557,15 @@ impl Infer {
75027557 flatten_type_tokens(arg, &mut flat);
75037558 if let Some((ty_ast, consumed)) = self.consume_type_arg(&flat) {
75047559 self.type_arg_spans.insert(ty_ast.span);
7560+ // Type-witness argument in value position: units not
7561+ // enforced (see the other witness site above).
7562+ let saved_flag = self.in_type_annotation;
7563+ let saved_enforce = self.enforce_units;
7564+ self.in_type_annotation = false;
7565+ self.enforce_units = false;
75057566 let ascribed = self.ast_type_to_ty(&ty_ast);
7567+ self.in_type_annotation = saved_flag;
7568+ self.enforce_units = saved_enforce;
75067569 // The witness type is the value's type: pin `rest`
75077570 // (`a -> a`) to `ascribed -> ascribed`. The result of
75087571 // consuming ONLY the type argument is the partially
@@ -15912,10 +15975,11 @@ fn collect_alias_refs(ty: &ast::Type, alias_names: &HashSet<String>, out: &mut H
1591215975 ast::TypeKind::IO { ty, .. } => {
1591315976 collect_alias_refs(ty, alias_names, out);
1591415977 }
15915− ast::TypeKind::UnitAnnotated { base, .. } => {
15916− collect_alias_refs(base, alias_names, out);
15917− }
1591815978 ast::TypeKind::Unit(_) => {}
15979+ ast::TypeKind::UnitMul(a, b) | ast::TypeKind::UnitDiv(a, b) => {
15980+ collect_alias_refs(a, alias_names, out);
15981+ collect_alias_refs(b, alias_names, out);
15982+ }
1591915983 ast::TypeKind::Refined { base, .. } => {
1592015984 collect_alias_refs(base, alias_names, out);
1592115985 }