From d823d7f084294f2432cd433af3ffdc396f6fb61c Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Tue, 5 Mar 2024 11:43:23 +0000 Subject: [PATCH] Relax enum row conflict (#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 => ..}` --- .../errors/enum_contract_shape_mismatch.ncl | 3 - .../enum_contract_shape_mismatch_rev.ncl | 3 - ...derr_enum_contract_shape_mismatch.ncl.snap | 29 ------- ..._enum_contract_shape_mismatch_rev.ncl.snap | 29 ------- core/src/error/mod.rs | 2 +- core/src/parser/uniterm.rs | 11 +-- core/src/typ.rs | 20 ++--- core/src/typecheck/error.rs | 8 +- core/src/typecheck/mod.rs | 4 +- core/src/typecheck/unif.rs | 63 ++++++++++++--- core/stdlib/internals.ncl | 81 +++++++------------ ...ata-types.ncl => algebraic_data_types.ncl} | 0 .../typecheck/enum_row_conflict_extend.ncl | 14 ++++ .../typecheck/enum_row_conflict_poly.ncl | 16 ++++ .../typecheck/enum_row_conflict_remove.ncl | 14 ++++ .../typecheck/enum_row_tags_dont_conflict.ncl | 14 ++++ ...end.ncl => record_row_conflict_extend.ncl} | 0 ...=> record_row_conflict_poly_shuffled1.ncl} | 0 ...=> record_row_conflict_poly_shuffled2.ncl} | 0 ...=> record_row_conflict_poly_shuffled3.ncl} | 0 ...ove.ncl => record_row_conflict_remove.ncl} | 0 21 files changed, 160 insertions(+), 151 deletions(-) delete mode 100644 cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch.ncl delete mode 100644 cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch_rev.ncl delete mode 100644 cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch.ncl.snap delete mode 100644 cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch_rev.ncl.snap rename core/tests/integration/inputs/typecheck/{algebraic-data-types.ncl => algebraic_data_types.ncl} (100%) create mode 100644 core/tests/integration/inputs/typecheck/enum_row_conflict_extend.ncl create mode 100644 core/tests/integration/inputs/typecheck/enum_row_conflict_poly.ncl create mode 100644 core/tests/integration/inputs/typecheck/enum_row_conflict_remove.ncl create mode 100644 core/tests/integration/inputs/typecheck/enum_row_tags_dont_conflict.ncl rename core/tests/integration/inputs/typecheck/{row_conflict_extend.ncl => record_row_conflict_extend.ncl} (100%) rename core/tests/integration/inputs/typecheck/{row_conflict_poly_shuffled1.ncl => record_row_conflict_poly_shuffled1.ncl} (100%) rename core/tests/integration/inputs/typecheck/{row_conflict_poly_shuffled2.ncl => record_row_conflict_poly_shuffled2.ncl} (100%) rename core/tests/integration/inputs/typecheck/{row_conflict_poly_shuffled3.ncl => record_row_conflict_poly_shuffled3.ncl} (100%) rename core/tests/integration/inputs/typecheck/{row_conflict_remove.ncl => record_row_conflict_remove.ncl} (100%) diff --git a/cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch.ncl b/cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch.ncl deleted file mode 100644 index 1a1883894a..0000000000 --- a/cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch.ncl +++ /dev/null @@ -1,3 +0,0 @@ -# capture = 'stderr' -# command = ['eval'] -(std.function.id | forall r. [| 'Foo Number, 'Bar String, 'Qux; r |] -> [| 'Foo Number, 'Bar String, 'Qux; r |]) 'Foo diff --git a/cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch_rev.ncl b/cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch_rev.ncl deleted file mode 100644 index fd3fe34e1a..0000000000 --- a/cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch_rev.ncl +++ /dev/null @@ -1,3 +0,0 @@ -# capture = 'stderr' -# command = ['eval'] -(std.function.id | forall r. [| 'Foo, 'Bar String, 'Qux Dyn; r |] -> [| 'Foo, 'Bar String, 'Qux Dyn; r |]) ('Foo 5) diff --git a/cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch.ncl.snap b/cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch.ncl.snap deleted file mode 100644 index 2ccdaaed26..0000000000 --- a/cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch.ncl.snap +++ /dev/null @@ -1,29 +0,0 @@ ---- -source: cli/tests/snapshot/main.rs -expression: err ---- -error: contract broken by the caller - shape mismatch for 'Foo - ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch.ncl:3:30 - │ -3 │ (std.function.id | forall r. [| 'Foo Number, 'Bar String, 'Qux; r |] -> [| 'Foo Number, 'Bar String, 'Qux; r |]) 'Foo - │ --------------------------------------- ---- evaluated to this expression - │ │ - │ expected type of the argument provided by the caller - │ - = Found an enum with tag `'Foo` 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 - -note: - ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch.ncl:3:1 - │ -3 │ (std.function.id | forall r. [| 'Foo Number, 'Bar String, 'Qux; r |] -> [| 'Foo Number, 'Bar String, 'Qux; r |]) 'Foo - │ --------------------------------------------------------------------------------------------------------------------- (1) calling - -note: - ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch.ncl:3:2 - │ -3 │ (std.function.id | forall r. [| 'Foo Number, 'Bar String, 'Qux; r |] -> [| 'Foo Number, 'Bar String, 'Qux; r |]) 'Foo - │ --------------- (2) calling - - diff --git a/cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch_rev.ncl.snap b/cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch_rev.ncl.snap deleted file mode 100644 index 95a4f2615a..0000000000 --- a/cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch_rev.ncl.snap +++ /dev/null @@ -1,29 +0,0 @@ ---- -source: cli/tests/snapshot/main.rs -expression: err ---- -error: contract broken by the caller - shape mismatch for 'Foo - ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch_rev.ncl:3:30 - │ -3 │ (std.function.id | forall r. [| 'Foo, 'Bar String, 'Qux Dyn; r |] -> [| 'Foo, 'Bar String, 'Qux Dyn; r |]) ('Foo 5) - │ ------------------------------------ -------- evaluated to this expression - │ │ - │ expected type of the argument provided by the caller - │ - = Found an enum with tag `'Foo` 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 - -note: - ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch_rev.ncl:3:1 - │ -3 │ (std.function.id | forall r. [| 'Foo, 'Bar String, 'Qux Dyn; r |] -> [| 'Foo, 'Bar String, 'Qux Dyn; r |]) ('Foo 5) - │ ------------------------------------------------------------------------------------------------------------------- (1) calling - -note: - ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch_rev.ncl:3:2 - │ -3 │ (std.function.id | forall r. [| 'Foo, 'Bar String, 'Qux Dyn; r |] -> [| 'Foo, 'Bar String, 'Qux Dyn; r |]) ('Foo 5) - │ --------------- (2) calling - - diff --git a/core/src/error/mod.rs b/core/src/error/mod.rs index 3dff15a86b..6ed3bc1bd5 100644 --- a/core/src/error/mod.rs +++ b/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], diff --git a/core/src/parser/uniterm.rs b/core/src/parser/uniterm.rs index d3c4dc5335..715a051971 100644 --- a/core/src/parser/uniterm.rs +++ b/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()) } } diff --git a/core/src/typ.rs b/core/src/typ.rs index 4c5a1433ed..f573b7d079 100644 --- a/core/src/typ.rs +++ b/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)) } } diff --git a/core/src/typecheck/error.rs b/core/src/typecheck/error.rs index de0891d0cf..30db92355f 100644 --- a/core/src/typecheck/error.rs +++ b/core/src/typecheck/error.rs @@ -39,9 +39,9 @@ pub enum RowUnifError { /// The underlying unification error that caused the mismatch. cause: Option>, }, - /// 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, diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs index 67e775cff0..34450f7054 100644 --- a/core/src/typecheck/mod.rs +++ b/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, }; diff --git a/core/src/typecheck/unif.rs b/core/src/typecheck/unif.rs index b11c968ea5..2ec4cb6f4e 100644 --- a/core/src/typecheck/unif.rs +++ b/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>; +/// +/// 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>; 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, 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, 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, diff --git a/core/stdlib/internals.ncl b/core/stdlib/internals.ncl index 3ff75f6120..22539fba33 100644 --- a/core/stdlib/internals.ncl +++ b/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 diff --git a/core/tests/integration/inputs/typecheck/algebraic-data-types.ncl b/core/tests/integration/inputs/typecheck/algebraic_data_types.ncl similarity index 100% rename from core/tests/integration/inputs/typecheck/algebraic-data-types.ncl rename to core/tests/integration/inputs/typecheck/algebraic_data_types.ncl diff --git a/core/tests/integration/inputs/typecheck/enum_row_conflict_extend.ncl b/core/tests/integration/inputs/typecheck/enum_row_conflict_extend.ncl new file mode 100644 index 0000000000..c6296d3750 --- /dev/null +++ b/core/tests/integration/inputs/typecheck/enum_row_conflict_extend.ncl @@ -0,0 +1,14 @@ +# test.type = 'error' +# eval = 'typecheck' +# +# [test.metadata] +# error = 'TypecheckError::EnumRowConflict' +# +# [test.metadata.expectation] +# row = 'Foo' + +# Regression test following [#144](https://github.com/tweag/nickel/issues/144). Check that +# polymorphic type variables appearing inside a row type are correctly constrained at +# instantiation. +let extend | forall c. [| ; c |] -> [| 'Foo String ; c |] = null +in (let bad = extend ('Foo "a") in 0) : Number diff --git a/core/tests/integration/inputs/typecheck/enum_row_conflict_poly.ncl b/core/tests/integration/inputs/typecheck/enum_row_conflict_poly.ncl new file mode 100644 index 0000000000..64ec46d486 --- /dev/null +++ b/core/tests/integration/inputs/typecheck/enum_row_conflict_poly.ncl @@ -0,0 +1,16 @@ +# test.type = 'error' +# eval = 'typecheck' +# +# [test.metadata] +# error = 'TypecheckError::EnumRowConflict' +# +# [test.metadata.expectation] +# row = 'Foo' +let f + | forall r. [| ; r |] -> [| 'Foo Number, 'Bar Number ; r |] + # the implementation doesn't matter, we care about types + = fun r => null + in +let g = fun x => 'a in +g ((f ('Foo "a")) : _) + diff --git a/core/tests/integration/inputs/typecheck/enum_row_conflict_remove.ncl b/core/tests/integration/inputs/typecheck/enum_row_conflict_remove.ncl new file mode 100644 index 0000000000..08136c0802 --- /dev/null +++ b/core/tests/integration/inputs/typecheck/enum_row_conflict_remove.ncl @@ -0,0 +1,14 @@ +# test.type = 'error' +# eval = 'typecheck' +# +# [test.metadata] +# error = 'TypecheckError::EnumRowConflict' +# +# [test.metadata.expectation] +# row = 'Foo' + +# Regression test following [#144](https://github.com/tweag/nickel/issues/144). Check that +# polymorphic type variables appearing inside a row type are correctly constrained at +# instantiation. +let remove | forall c. [| 'Foo String; c |] -> [| ; c |] = null +in (let bad = remove (remove ('Foo "a")) in 0) : Number diff --git a/core/tests/integration/inputs/typecheck/enum_row_tags_dont_conflict.ncl b/core/tests/integration/inputs/typecheck/enum_row_tags_dont_conflict.ncl new file mode 100644 index 0000000000..46370cc2c8 --- /dev/null +++ b/core/tests/integration/inputs/typecheck/enum_row_tags_dont_conflict.ncl @@ -0,0 +1,14 @@ +# test.type = 'pass' +( + let f : forall r. [| 'Foo Number; r |] -> Bool = match { + 'Foo x => false, + _ => true, + } in + + let g : forall r. [| 'Foo Number, 'Foo |] -> Bool = match { + 'Foo x => false, + 'Foo => true, + } in + + f 'Foo && g 'Foo +) : Bool diff --git a/core/tests/integration/inputs/typecheck/row_conflict_extend.ncl b/core/tests/integration/inputs/typecheck/record_row_conflict_extend.ncl similarity index 100% rename from core/tests/integration/inputs/typecheck/row_conflict_extend.ncl rename to core/tests/integration/inputs/typecheck/record_row_conflict_extend.ncl diff --git a/core/tests/integration/inputs/typecheck/row_conflict_poly_shuffled1.ncl b/core/tests/integration/inputs/typecheck/record_row_conflict_poly_shuffled1.ncl similarity index 100% rename from core/tests/integration/inputs/typecheck/row_conflict_poly_shuffled1.ncl rename to core/tests/integration/inputs/typecheck/record_row_conflict_poly_shuffled1.ncl diff --git a/core/tests/integration/inputs/typecheck/row_conflict_poly_shuffled2.ncl b/core/tests/integration/inputs/typecheck/record_row_conflict_poly_shuffled2.ncl similarity index 100% rename from core/tests/integration/inputs/typecheck/row_conflict_poly_shuffled2.ncl rename to core/tests/integration/inputs/typecheck/record_row_conflict_poly_shuffled2.ncl diff --git a/core/tests/integration/inputs/typecheck/row_conflict_poly_shuffled3.ncl b/core/tests/integration/inputs/typecheck/record_row_conflict_poly_shuffled3.ncl similarity index 100% rename from core/tests/integration/inputs/typecheck/row_conflict_poly_shuffled3.ncl rename to core/tests/integration/inputs/typecheck/record_row_conflict_poly_shuffled3.ncl diff --git a/core/tests/integration/inputs/typecheck/row_conflict_remove.ncl b/core/tests/integration/inputs/typecheck/record_row_conflict_remove.ncl similarity index 100% rename from core/tests/integration/inputs/typecheck/row_conflict_remove.ncl rename to core/tests/integration/inputs/typecheck/record_row_conflict_remove.ncl