Add scalars to TypeName

[MarkMcCaskey]

Part of #368 ; spun off of #371

[nikomatsakis]

Good start! I think we can remove the code around scalar values. What I think we will need though is

(1) to modify the parser so that it permits parsing tuples like (T1, ..., Tn) as types
(2) then either to modify the parser so that it recognizes bool, u8, etc as keywords or to modify the lowering code that maps type names to types so that it has hard-coded knowledge of bool and friends.

Modifying parser to accept tuples:

Just add "(" ... ")" into this entry, and extend Ty to include Ty::Tuple:

chalk/chalk-parse/src/parser.lalrpop

Lines 180 to 192 in 154020e

	TyWithoutFor: Ty = {
	<n:Id> => Ty::Id { name: n},
	"fn" "(" <t:Ty> ")" => Ty::ForAll {
	lifetime_names: vec![],
	ty: Box::new(t)
	},
	"dyn" <b:Plus<QuantifiedInlineBound>> => Ty::Dyn {
	bounds: b,
	},
	<n:Id> "<" <a:Comma<Parameter>> ">" => Ty::Apply { name: n, args: a },
	<a:AliasTy> => Ty::Alias { alias: a },
	"(" <Ty> ")",
	};

You'll have to modify the match here in lowering to include tuple too:

chalk/chalk-integration/src/lowering.rs

Line 977 in 154020e

match *self {

Modifying parser to know bools etc:

You could do the same for bools, integers, etc as you did for tuples, or you could modify lowering, as described next. I don't have a strong opinion about which is better -- this is just the chalk testing harness, after all -- I think I'd go for modifying the parser, it seems mildly easier to me.

Modifying lowering to hard-code bools etc:

Here is the lowering code that actually looks up a name:

chalk/chalk-integration/src/lowering.rs

Lines 79 to 96 in 154020e

	fn lookup_type(&self, name: Identifier) -> LowerResult<TypeLookup> {
	if let Some(k) = self
	.parameter_map
	.get(&chalk_ir::ParameterKind::Ty(name.str))
	{
	return Ok(TypeLookup::Parameter(*k));
	}
	if let Some(id) = self.struct_ids.get(&name.str) {
	return Ok(TypeLookup::Struct(*id));
	}
	if let Some(_) = self.trait_ids.get(&name.str) {
	return Err(RustIrError::NotStruct(name));
	}
	Err(RustIrError::InvalidTypeName(name))
	}

Right now it's hard-coded to type parameters or the names of structs. It could have some code at the end that's like "if this is the string bool, then return TypeLookup::Bool" etc. You would also have to modify this code that converts a type like foo into the chalk-ir type to understand those results:

chalk/chalk-integration/src/lowering.rs

Lines 978 to 996 in 154020e

	Ty::Id { name } => match env.lookup_type(name)? {
	TypeLookup::Struct(id) => {
	let k = env.struct_kind(id);
	if k.binders.len() > 0 {
	Err(RustIrError::IncorrectNumberOfTypeParameters {
	identifier: name,
	expected: k.binders.len(),
	actual: 0,
	})
	} else {
	Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
	name: chalk_ir::TypeName::Struct(id),
	substitution: chalk_ir::Substitution::empty(interner),
	})
	.intern(interner))
	}
	}
	TypeLookup::Parameter(d) => Ok(chalk_ir::TyData::BoundVar(d).intern(interner)),
	},

[MarkMcCaskey]

Thank you for the very helpful review!

Here's the status of the PR:

• chalk_solve::clauses::match_type_name does a no-op for scalars and tuples right now, this probably isn't what we want -- I didn't get around to adding tests that would cause this to fail yet but I imagine it won't be hard to do
• scalar type name and tuple parsing now works: it may be a bit sub-optimal in places because I expected (A, B,) to not parse, but I just tested it now and it works! Which means that my implementation, which special cases the single tuple case of (A,), may be overly complex. Also I used right-recursion for something when some of the existing parsing code was using left-recursion which is a red flag to me that I may have made a mistake. It's been a bit since I did BNF-style parsing and I don't remember the details -- I'll look into this tomorrow.
• I updated all the tests that were using names that collide with the new scalar values to use different names. The reason I chose different names instead of removing the declarations was to future-proof in case traits are automatically implemented for the scalar types and that interferes with the functioning of the tests. That said, I did notice that #[auto] on a trait did not apply to the scalar values -- another thing that should be tested!
• It's a lexing/regex error if the tests use something like struct i32 { } now which is probably not what we want. Ideally there'd be a more clear error message there.

So from my perspective there's 3 things left to do:

• Address feedback and fix anything I've missed here
• Add more interesting tests and improve the internals to make that work
• Resolve the merge conflict implementing Visit for scalars and tuples

I'll try to get those done tomorrow if I'm able to!

[nikomatsakis]

Looking real close! Left one suggestion around how to handle tuples (and a suggestion for cleaning up the parser)

[nikomatsakis]

Nice! A few comments.

[nikomatsakis]

Looking good! I think this is just about ready to land, modulo a rebase.

[nikomatsakis]

It was said on Zulip, but I think what you want to do is to modify the code that runs in this match arm

chalk/chalk-solve/src/clauses.rs

Lines 296 to 298 in f438d7e

	DomainGoal::WellFormed(WellFormed::Ty(ty))
	| DomainGoal::IsUpstream(ty)
	| DomainGoal::DownstreamType(ty) => match_ty(builder, environment, ty)?,

So presumably that function match_ty:

chalk/chalk-solve/src/clauses.rs

Lines 392 to 407 in f438d7e

	/// Examine `T` and push clauses that may be relevant to proving the
	/// following sorts of goals (and maybe others):
	///
	/// * `DomainGoal::WellFormed(T)`
	/// * `DomainGoal::IsUpstream(T)`
	/// * `DomainGoal::DownstreamType(T)`
	/// * `DomainGoal::IsFullyVisible(T)`
	/// * `DomainGoal::IsLocal(T)`
	///
	/// Note that the type `T` must not be an unbound inference variable;
	/// earlier parts of the logic should "flounder" in that case.
	fn match_ty<I: Interner>(
	builder: &mut ClauseBuilder<'_, I>,
	environment: &Environment<I>,
	ty: &Ty<I>,
	) -> Result<(), Floundered> {

It should, if ty is a built-in scalar type, just generate a clause that declare them to be well-formed. You can basically just add them to this existing arm that handles generic placeholders, which are also always assumed to be well-formed:

chalk/chalk-solve/src/clauses.rs

Lines 411 to 413 in f438d7e

	TyData::Placeholder(_) => {
	builder.push_clause(WellFormed::Ty(ty.clone()), Some(FromEnv::Ty(ty.clone())));
	}

[nikomatsakis]

Looks good! Just one nit and then let's land this.

[nikomatsakis]

I think this logic should move into match_type_name

[nikomatsakis]

i.e., right here

[nikomatsakis]

I think this is right, though it may change as we tweak our def'n of implied bounds

[MarkMcCaskey]

Thanks! I moved the logic but had to change the type signature of match_type_name to take an ApplicationTy and an Interner to be able to get a Ty to be able to add the fact. Let me know if there's a better way to do this! I wasn't able to find anything much better by looking through the docs.

A somewhat reasonable alternative is to pass Ty and an Interner instead: we can avoid the cost of interning the ApplicationTy again at the cost of having to handle a failure case (Ty's that are not Applications and have no TypeName) and do the branch on ty.data again.

[nikomatsakis]

It seems fine as is to me, thanks!