Relax enum row conflict (tweag#1831)

The current design of structural ADTs is to clearly separate
syntactically unapplied variants (enum tags) from enum variants with an
argument, both when constructing them or when deconstructing them
(pattern matching).

However, the previous handling of row conflicts would still forbid types
like [| 'Foo, 'Foo Number |]. Because they are constructed separately,
and because they can be matched on separately, this type is actually
unproblematic. Thus, this commit relaxes the notion of row conflicts for
enums by basically ignoring unapplied enum rows (corresponding to enum
tags) within enum row types. This makes it possible to typecheck
expressions like `match { 'Foo => .., 'Foo x => ..}`

core/src/error/mod.rs

@@ -290,7 +290,7 @@ pub enum TypecheckError {
  /// of some expression is inferred to be `{ field: Type; t}`, then `t` must not be unified
  /// later with a type including a different declaration for field, such as `field: Type2`.
  ///
- /// A [constraint][crate::typecheck::unif::RowConstr] is added accordingly, and if this
+ /// A [constraint][crate::typecheck::unif::RowConstrs] is added accordingly, and if this
  /// constraint is violated (that is if `t` does end up being unified with a type of the form `{
  /// .., field: Type2, .. }`), [Self::RecordRowConflict] is raised. We do not necessarily have
  /// access to the original `field: Type` declaration, as opposed to [Self::RecordRowMismatch],

core/src/parser/uniterm.rs

@@ -805,7 +805,7 @@ impl FixTypeVars for EnumRows {
  bound_vars: BoundVarEnv,
  span: RawSpan,
  ) -> Result<(), ParseError> {
- fn helper(
+ fn do_fix(
  erows: &mut EnumRows,
  bound_vars: BoundVarEnv,
  span: RawSpan,
@@ -828,18 +828,19 @@ impl FixTypeVars for EnumRows {
  ref mut row,
  ref mut tail,
  } => {
- maybe_excluded.insert(row.id.ident());
-
  if let Some(ref mut typ) = row.typ {
+ // Enum tags (when `typ` is `None`) can't create a conflict, so we ignore them
+ // for constraints. See the documentation of `typecheck::unif::RowConstrs`.
+ maybe_excluded.insert(row.id.ident());
  typ.fix_type_vars_env(bound_vars.clone(), span)?;
  }
 
- helper(tail, bound_vars, span, maybe_excluded)
+ do_fix(tail, bound_vars, span, maybe_excluded)
  }
  }
  }
 
- helper(self, bound_vars, span, HashSet::new())
+ do_fix(self, bound_vars, span, HashSet::new())
  }
 }
 

core/src/typ.rs

@@ -851,8 +851,11 @@ impl Subcontract for Type {
  let sealing_key = Term::SealingKey(*sy);
  let contract = match var_kind {
  VarKind::Type => mk_app!(internals::forall_var(), sealing_key.clone()),
- kind @ VarKind::RecordRows { excluded }
- | kind @ VarKind::EnumRows { excluded } => {
+ // For now, the enum contract doesn't enforce parametricity: see the
+ // implementation of `forall_enum_tail` inside the internal module for more
+ // details.
+ VarKind::EnumRows { .. } => internals::forall_enum_tail(),
+ VarKind::RecordRows { excluded } => {
  let excluded_ncl: RichTerm = Term::Array(
  Array::from_iter(
  excluded
@@ -863,13 +866,11 @@ impl Subcontract for Type {
  )
  .into();
 
- let forall_contract = match kind {
- VarKind::RecordRows { .. } => internals::forall_record_tail(),
- VarKind::EnumRows { .. } => internals::forall_enum_tail(),
- _ => unreachable!(),
- };
-
- mk_app!(forall_contract, sealing_key.clone(), excluded_ncl)
+ mk_app!(
+ internals::forall_record_tail(),
+ sealing_key.clone(),
+ excluded_ncl
+ )
  }
  };
  vars.insert(var.ident(), contract);
@@ -1044,7 +1045,6 @@ impl Subcontract for EnumRows {
  );
 
  let case = mk_fun!(label_arg, value_arg, match_expr);
- // println!("Generated case: {case}");
  Ok(mk_app!(internals::enumeration(), case))
  }
 }

core/src/typecheck/error.rs

@@ -39,9 +39,9 @@ pub enum RowUnifError {
  /// The underlying unification error that caused the mismatch.
  cause: Option<Box<UnifError>>,
  },
- /// A [row constraint][super::RowConstr] was violated.
+ /// A [row constraint][super::RowConstrs] was violated.
  RecordRowConflict(UnifRecordRow),
- /// A [row constraint][super::RowConstr] was violated.
+ /// A [row constraint][super::RowConstrs] was violated.
  EnumRowConflict(UnifEnumRow),
  /// Tried to unify a type constant with another different type.
  WithConst {
@@ -202,7 +202,7 @@ pub enum UnifError {
  inferred: UnifType,
  },
  /// Tried to unify a unification variable with a row type violating the [row
- /// constraints][super::RowConstr] of the variable.
+ /// constraints][super::RowConstrs] of the variable.
  RecordRowConflict {
  /// The row that conflicts with an existing one.
  row: UnifRecordRow,
@@ -214,7 +214,7 @@ pub enum UnifError {
  inferred: UnifType,
  },
  /// Tried to unify a unification variable with a row type violating the [row
- /// constraints][super::RowConstr] of the variable.
+ /// constraints][super::RowConstrs] of the variable.
  EnumRowConflict {
  /// The row that conflicts with an existing one.
  row: UnifEnumRow,

core/src/typecheck/mod.rs

@@ -1345,7 +1345,7 @@ pub struct State<'a> {
  /// The unification table.
  table: &'a mut UnifTable,
  /// Row constraints.
- constr: &'a mut RowConstr,
+ constr: &'a mut RowConstrs,
  /// A mapping from unification variables or constants together with their
  /// kind to the name of the corresponding type variable which introduced it,
  /// if any.
@@ -1398,7 +1398,7 @@ where
  let mut state: State = State {
  resolver,
  table: &mut table,
- constr: &mut RowConstr::new(),
+ constr: &mut RowConstrs::new(),
  names: &mut names,
  wildcard_vars: &mut wildcard_vars,
  };

core/src/typecheck/unif.rs

@@ -1028,7 +1028,20 @@ impl UnifTable {
 /// identifiers that said row must NOT contain, to forbid ill-formed types with multiple
 /// declaration of the same id, for example `{ a: Number, a: String}` or `[| 'Foo String, 'Foo
 /// Number |]`.
-pub type RowConstr = HashMap<VarId, HashSet<Ident>>;
+///
+/// Note that because the syntax (and pattern matching likewise) distinguishes between `'Foo` and
+/// `'Foo some_arg`, the type `[| 'Foo, 'Foo SomeType |]` is unproblematic for typechecking. In
+/// some sense, enum tags and enum variants live in a different dimension. It looks like we should
+/// use separate sets of constraints for enum tag constraints and enum variants constraints. But a
+/// set just for enum tag constraints is useless, because enum tags can never conflict, as they
+/// don't have any argument: `'Foo` always "agrees with" another `'Foo` definition. In consequence,
+/// we simply record enum variants constraints and ignore enum tags.
+///
+/// Note that a `VarId` always refer to either a type unification variable, a record row
+/// unification variable or an enum row unification variable. Thus, we can use a single constraint
+/// set per variable id (which isn't used at all for type unification variables). Because we expect
+/// the map to be rather sparse, we use a `HashMap` instead of a `Vec`.
+pub type RowConstrs = HashMap<VarId, HashSet<Ident>>;
 
 trait PropagateConstrs {
  /// Check that unifying a variable with a type doesn't violate rows constraints, and update the
@@ -1047,13 +1060,18 @@ trait PropagateConstrs {
  /// don't constrain `u`, `u` could be unified later with a row type `{a : String}` which violates
  /// the original constraint on `p`. Thus, when unifying `p` with `u` or a row ending with `u`,
  /// `u` must inherit all the constraints of `p`.
- fn propagate_constrs(&self, constr: &mut RowConstr, var_id: VarId) -> Result<(), RowUnifError>;
+ fn propagate_constrs(&self, constr: &mut RowConstrs, var_id: VarId)
+ -> Result<(), RowUnifError>;
 }
 
 impl PropagateConstrs for UnifRecordRows {
- fn propagate_constrs(&self, constr: &mut RowConstr, var_id: VarId) -> Result<(), RowUnifError> {
+ fn propagate_constrs(
+ &self,
+ constr: &mut RowConstrs,
+ var_id: VarId,
+ ) -> Result<(), RowUnifError> {
  fn propagate(
- constr: &mut RowConstr,
+ constr: &mut RowConstrs,
  var_id: VarId,
  var_constr: HashSet<Ident>,
  rrows: &UnifRecordRows,
@@ -1091,16 +1109,30 @@ impl PropagateConstrs for UnifRecordRows {
 }
 
 impl PropagateConstrs for UnifEnumRows {
- fn propagate_constrs(&self, constr: &mut RowConstr, var_id: VarId) -> Result<(), RowUnifError> {
+ fn propagate_constrs(
+ &self,
+ constr: &mut RowConstrs,
+ var_id: VarId,
+ ) -> Result<(), RowUnifError> {
  fn propagate(
- constr: &mut RowConstr,
+ constr: &mut RowConstrs,
  var_id: VarId,
  var_constr: HashSet<Ident>,
  erows: &UnifEnumRows,
  ) -> Result<(), RowUnifError> {
  match erows {
  UnifEnumRows::Concrete {
- erows: EnumRowsF::Extend { row, .. },
+ // If the row is an enum tag (ie `typ` is `None`), it can't cause any conflict.
+ // See [RowConstrs] for more details.
+ erows:
+ EnumRowsF::Extend {
+ row:
+ row @ UnifEnumRow {
+ id: _,
+ typ: Some(_),
+ },
+ ..
+ },
  ..
  } if var_constr.contains(&row.id.ident()) => {
  Err(RowUnifError::EnumRowConflict(row.clone()))
@@ -1730,7 +1762,13 @@ impl RemoveRow for UnifEnumRows {
  row: next_row,
  tail,
  } => {
- if target.ident() == next_row.id.ident() {
+ // Enum variants and enum tags don't conflict, and can thus coexist in the same
+ // row type (for example, [| 'Foo Number, 'Foo |]). In some sense, they live
+ // inside different dimensions. Thus, when matching rows, we don't only compare
+ // the tag but also the nature of the enum row (tag vs variant)
+ if target.ident() == next_row.id.ident()
+ && target_content.is_some() == next_row.typ.is_some()
+ {
  Ok((
  RemoveRowResult::Extracted(next_row.typ.map(|typ| *typ)),
  *tail,
@@ -1751,9 +1789,12 @@ impl RemoveRow for UnifEnumRows {
  UnifEnumRows::UnifVar { id: var_id, .. } => {
  let tail_var_id = state.table.fresh_erows_var_id(var_level);
 
- state
- .constr
- .insert(tail_var_id, HashSet::from([target.ident()]));
+ // Enum tag are ignored for row conflict. See [RowConstrs]
+ if target_content.is_some() {
+ state
+ .constr
+ .insert(tail_var_id, HashSet::from([target.ident()]));
+ }
 
  let row_to_insert = UnifEnumRow {
  id: *target,

core/stdlib/internals.ncl

@@ -118,60 +118,33 @@
  else
  %blame% (%label_with_message% "expected an enum variant" label),
 
- "$forall_enum_tail" = fun sealing_key constr label value =>
- # We check for conflicts only when the polarity of the foralls matches the
- # current polarity ("negative" polarity relatively to the forall). In
- # positive (relative) polarity, a value lying in the tail either is sealed
- # and has thus already been checked for conflicts, or it is not sealed and
- # it will fail the `unseal` check anyway.
- let current_polarity = %polarity% label in
- let polarity = (%lookup_type_variable% sealing_key label).polarity in
- if polarity == current_polarity then
- # [^enum-no-sealing]: Theoretically, we should seal/unseal values that
- # are part of enum tail. However, we can't just do that, because then a
- # match expression that is entirely legit, for example
- #
- # ```
- # match { 'Foo => 1, _ => 2 } : forall r. [| 'Foo; r|] -> Number`
- # ```
- #
- # would fail on `'Bar`, if we just seal the latter naively. It looks like
- # we should allow matches to see through sealed enum, but accept only if
- # the catch-all case matches what's inside the saled enum.
- #
- # This doesn't look trivial for now, and would actually break the stdlib,
- # as parametricity hasn't been correctly enforced for enum types. One
- # example is `std.string.from_enum`, which has contract
- # `forall a. [|; a |] -> String` but actually violates parametricity (it
- # actually looks inside its argument).
- #
- # While this might be an issue to investigate in the longer term, or for
- # the next major version, we continue to just not enforce parametricity
- # for enum types for now.
- value
- else
- let value_tag = %to_str% (%enum_get_tag% value) in
- if std.array.elem value_tag constr then
- %blame%
- (
- %label_with_message%
- "shape mismatch for '%{value_tag}"
- (
- %label_with_notes%
- (
- %force%
- [
- "Found an enum with tag `'%{value_tag}` which is indeed part of the expected enum type",
- "However, their shape differs: one is an enum variant that carries an argument while the other is a bare enum tag"
- ]
- )
- label
- )
- )
- else
- # Same as [^enum-no-sealing] above. We should theoretically seal here,
- # but we don't for now.
- value,
+ "$forall_enum_tail" = fun label value =>
+ # Theoretically, we should seal/unseal values that are part of enum tail
+ # and `$forall_enum_tail` should be defined similarly to
+ # `$forall_record_tail`, as a function of `sealing_key` as well.
+ #
+ # However, we can't just do that, because then a match expression that is
+ # entirely legit, for example
+ #
+ # ```
+ # match { 'Foo => 1, _ => 2 } : forall r. [| 'Foo; r|] -> Number`
+ # ```
+ #
+ # would fail on `'Bar` because it's sealed. It looks like we should allow
+ # `match` to see through sealed enum, but proceed only if the final
+ # catch-all case matches what's inside the sealed enum, and not a more
+ # precise parametricity-breaking pattern.
+ #
+ # Unfortunately, that would break the current stdlib because parametricity
+ # hasn't never been enforced correctly for enum types in the past. For
+ # example, `std.string.from_enum` has contract
+ # `forall a. [|; a |] -> String` which does violate parametricity, as it
+ # looks inside its argument although it's part of a polymorphic tail.
+ #
+ # While this might be an issue to investigate in the longer term, or for
+ # the next major version, we continue to just not enforce parametricity
+ # for enum types for now to maintain backward-compatibility.
+ value,
 
  "$record" = fun field_contracts tail_contract label value =>
  if %typeof% value == 'Record then