Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove unit fields from enum variants #565

Merged
merged 1 commit into from
Jul 9, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion chalk-engine/src/simplify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
context.into_goal(domain_goal.clone()),
)));
}
GoalData::CannotProve(()) => {
GoalData::CannotProve => {
debug!("Marking Strand as ambiguous because of a `CannotProve` subgoal");
ex_clause.ambiguous = true;
}
Expand Down
4 changes: 2 additions & 2 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1055,11 +1055,11 @@ impl LowerDomainGoal for DomainGoal {
trait_ref.lower(env)?,
)]
}
DomainGoal::Compatible => vec![chalk_ir::DomainGoal::Compatible(())],
DomainGoal::Compatible => vec![chalk_ir::DomainGoal::Compatible],
DomainGoal::DownstreamType { ty } => {
vec![chalk_ir::DomainGoal::DownstreamType(ty.lower(env)?)]
}
DomainGoal::Reveal => vec![chalk_ir::DomainGoal::Reveal(())],
DomainGoal::Reveal => vec![chalk_ir::DomainGoal::Reveal],
DomainGoal::ObjectSafe { id } => {
vec![chalk_ir::DomainGoal::ObjectSafe(env.lookup_trait(id)?)]
}
Expand Down
6 changes: 3 additions & 3 deletions chalk-ir/src/debug.rs
Original file line number Diff line number Diff line change
Expand Up @@ -332,7 +332,7 @@ impl<I: Interner> Debug for GoalData<I> {
GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
GoalData::EqGoal(ref wc) => write!(fmt, "{:?}", wc),
GoalData::DomainGoal(ref wc) => write!(fmt, "{:?}", wc),
GoalData::CannotProve(()) => write!(fmt, r"¯\_(ツ)_/¯"),
GoalData::CannotProve => write!(fmt, r"¯\_(ツ)_/¯"),
}
}
}
Expand Down Expand Up @@ -717,9 +717,9 @@ impl<I: Interner> Debug for DomainGoal<I> {
DomainGoal::LocalImplAllowed(tr) => {
write!(fmt, "LocalImplAllowed({:?})", tr.with_colon(),)
}
DomainGoal::Compatible(_) => write!(fmt, "Compatible"),
DomainGoal::Compatible => write!(fmt, "Compatible"),
DomainGoal::DownstreamType(n) => write!(fmt, "DownstreamType({:?})", n),
DomainGoal::Reveal(_) => write!(fmt, "Reveal"),
DomainGoal::Reveal => write!(fmt, "Reveal"),
DomainGoal::ObjectSafe(n) => write!(fmt, "ObjectSafe({:?})", n),
}
}
Expand Down
12 changes: 4 additions & 8 deletions chalk-ir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1570,9 +1570,7 @@ pub enum DomainGoal<I: Interner> {
/// Used to activate the "compatible modality" rules. Rules that introduce predicates that have
/// to do with "all compatible universes" should depend on this clause so that they only apply
/// if this is present.
///
/// (HACK: Having `()` makes some of our macros work better.)
Compatible(()),
Compatible,

/// Used to indicate that a given type is in a downstream crate. Downstream crates contain the
/// current crate at some level of their dependencies.
Expand All @@ -1587,7 +1585,7 @@ pub enum DomainGoal<I: Interner> {

/// Used to activate the "reveal mode", in which opaque (`impl Trait`) types can be equated
/// to their actual type.
Reveal(()),
Reveal,

/// Used to indicate that a trait is object safe.
ObjectSafe(TraitId<I>),
Expand Down Expand Up @@ -2189,7 +2187,7 @@ impl<I: Interner> Goal<I> {
GoalData::Implies(
ProgramClauses::from_iter(
interner,
vec![DomainGoal::Compatible(()), DomainGoal::DownstreamType(ty)],
vec![DomainGoal::Compatible, DomainGoal::DownstreamType(ty)],
),
self.shifted_in(interner),
)
Expand Down Expand Up @@ -2273,9 +2271,7 @@ pub enum GoalData<I: Interner> {
/// X, Y where `X = Y` is not true. But we treat it as "cannot
/// prove" so that `forall<X,Y> { not { X = Y } }` also winds up
/// as cannot prove.
///
/// (TOTAL HACK: Having a unit result makes some of our macros work better.)
CannotProve(()),
CannotProve,
}

impl<I: Interner> Copy for GoalData<I>
Expand Down
2 changes: 1 addition & 1 deletion chalk-recursive/src/fulfill.rs
Original file line number Diff line number Diff line change
Expand Up @@ -318,7 +318,7 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
GoalData::EqGoal(EqGoal { a, b }) => {
self.unify(&environment, &a, &b)?;
}
GoalData::CannotProve(()) => {
GoalData::CannotProve => {
debug!("Pushed a CannotProve goal, setting cannot_prove = true");
self.cannot_prove = true;
}
Expand Down
6 changes: 3 additions & 3 deletions chalk-solve/src/clauses.rs
Original file line number Diff line number Diff line change
Expand Up @@ -414,7 +414,7 @@ fn program_clauses_that_could_match<I: Interner>(
}
AliasTy::Opaque(_) => (),
},
DomainGoal::Compatible(()) | DomainGoal::Reveal(()) => (),
DomainGoal::Compatible | DomainGoal::Reveal => (),
};

Ok(clauses)
Expand Down Expand Up @@ -460,7 +460,7 @@ fn push_clauses_for_compatible_normalize<I: Interner>(
.iter()
.cloned()
.casted(interner)
.chain(iter::once(DomainGoal::Compatible(()).cast(interner)))
.chain(iter::once(DomainGoal::Compatible.cast(interner)))
.chain(iter::once(
WhereClause::Implemented(trait_ref.clone()).cast(interner),
))
Expand All @@ -470,7 +470,7 @@ fn push_clauses_for_compatible_normalize<I: Interner>(
.chain(iter::once(
DomainGoal::DownstreamType(type_parameters[i].clone()).cast(interner),
))
.chain(iter::once(GoalData::CannotProve(()).intern(interner))),
.chain(iter::once(GoalData::CannotProve.intern(interner))),
);
}
});
Expand Down
10 changes: 5 additions & 5 deletions chalk-solve/src/clauses/program_clauses.rs
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,7 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
}
.cast(interner),
),
iter::once(DomainGoal::Reveal(())),
iter::once(DomainGoal::Reveal),
);

// AliasEq(T<..> = !T<..>).
Expand Down Expand Up @@ -610,7 +610,7 @@ impl<I: Interner> ToProgramClauses<I> for TraitDatum<I> {
.iter()
.cloned()
.casted(interner)
.chain(iter::once(DomainGoal::Compatible(()).cast(interner)))
.chain(iter::once(DomainGoal::Compatible.cast(interner)))
.chain((0..i).map(|j| {
DomainGoal::IsFullyVisible(type_parameters[j].clone())
.cast(interner)
Expand All @@ -619,7 +619,7 @@ impl<I: Interner> ToProgramClauses<I> for TraitDatum<I> {
DomainGoal::DownstreamType(type_parameters[i].clone())
.cast(interner),
))
.chain(iter::once(GoalData::CannotProve(()).intern(interner))),
.chain(iter::once(GoalData::CannotProve.intern(interner))),
);
}
}
Expand Down Expand Up @@ -649,13 +649,13 @@ impl<I: Interner> ToProgramClauses<I> for TraitDatum<I> {
.iter()
.cloned()
.casted(interner)
.chain(iter::once(DomainGoal::Compatible(()).cast(interner)))
.chain(iter::once(DomainGoal::Compatible.cast(interner)))
.chain(
trait_ref
.type_parameters(interner)
.map(|ty| DomainGoal::IsUpstream(ty).cast(interner)),
)
.chain(iter::once(GoalData::CannotProve(()).intern(interner))),
.chain(iter::once(GoalData::CannotProve.intern(interner))),
);
}

Expand Down
8 changes: 4 additions & 4 deletions chalk-solve/src/wf.rs
Original file line number Diff line number Diff line change
Expand Up @@ -527,7 +527,7 @@ impl WfWellKnownGoals {
| WellKnownTrait::FnOnce
| WellKnownTrait::FnMut
| WellKnownTrait::Fn
| WellKnownTrait::Unsize => Some(GoalData::CannotProve(()).intern(interner)),
| WellKnownTrait::Unsize => Some(GoalData::CannotProve.intern(interner)),
}
}

Expand Down Expand Up @@ -585,10 +585,10 @@ impl WfWellKnownGoals {
| TypeName::Ref(Mutability::Not)
| TypeName::Never => return None,
TypeName::Adt(adt_id) => (*adt_id, substitution),
_ => return Some(GoalData::CannotProve(()).intern(interner)),
_ => return Some(GoalData::CannotProve.intern(interner)),
},

_ => return Some(GoalData::CannotProve(()).intern(interner)),
_ => return Some(GoalData::CannotProve.intern(interner)),
};

// not { Implemented(ImplSelfTy: Drop) }
Expand Down Expand Up @@ -668,7 +668,7 @@ impl WfWellKnownGoals {
let adt_id = match impl_datum.self_type_adt_id(interner) {
Some(id) => id,
// Drop can only be implemented on a nominal type
None => return Some(GoalData::CannotProve(()).intern(interner)),
None => return Some(GoalData::CannotProve.intern(interner)),
};

let mut gb = GoalBuilder::new(db);
Expand Down