Bug 176707 – WSL IntLiteralType should become int32 if unified with a type variable

• Component: WebGPU
• Status: RESOLVED FIXED

[Filip Pizlo]

This requires two changes:

- TypeVariable in parameter position needs to be happy about being unified with an IntLiteralType.  It probably already is.
- IntLiteralType in argument position needs to be happy with being unified with a TypeVariable or with itself.  In either case, it needs to just become an int32.

Tricky case: if IntLiteralType is unified with a TypeVariable, it needs to check that this type variable is in parameter position.  Otherwise it means this:

void foo<U>(U, U);
void bar<T>(T x) { foo(42, x); } 

Here, 42 will get unified with T.  This is invalid.  If T is the root of the equivalence set then we need to rely on 42's argument position validation to observe that it got unified with a TypeVariable in argument position, which means constraint failure.

[Filip Pizlo]

An even easier approach is to teach UnificationContext that during verification, it should ask all literals to select a more specific type.  They don't have to do it if they don't want to.

This has to be done in two phases.  First all of the literals that were involved in unification have to be given an opportunity to observe that they are unified with a literal or type variable.  If they are, then they can sign up to be part of a pre-verification pass.

Once all literals have been given a chance to sign up, then we run the pre-verification pass, where they all try to unify themselves with a more specific type of their choosing.  This could fail, if two literals are involved in a unifying call:

void foo<T>(T, T);

foo(0, 0.);

We'll almost certainly want 0. to be a floatLiteralType that can unify with a variety of different types.  Maybe we want 0u to behave like that also.  So, what could happen here is that both intLiteralType and floatLiteralType observe that they are unified with T, and then they will both want to select their more specific types.  At this point, unless we do a two-phase approach, we could have undecidability: depending on whether intLiteralType or floatLiteralType is picked first, that one could determine the type that T becomes.  This means that the program will either type check and use T=double (if floatLiteralType runs first), or it will not type check because intLiteralType ran first, unified with int32, and then floatLiteralType's pre-verification would say "oh, OK, I'm unified with something that isn't a floatLiteralType or TypeVariable so I have nothing to do". Then during actual verification, floatLiteralType would observe that it got unified with int32, which is wrong.

The two-phase approach ensures that both intLiteralType and floatLiteralType sign up for unifying, and then it's guaranteed that they will detect the type error no matter what order they run in.

[Filip Pizlo]

Created attachment 320788 [details]
the patch

[Filip Pizlo]

Comment on attachment 320788 [details]
the patch

View in context: https://bugs.webkit.org/attachment.cgi?id=320788&action=review

> Tools/WebGPUShadingLanguageRI/Type.js:41
> +    // This query assumes that the receiver type is to be used as a substitution for a type variable that was
> +    // declared to inherit this protocol. So, if upon unification with a type variable, the receiver type would
> +    // have chosen a subtype of itself, then it should handle this query by delegating it to that subtype. One
> +    // example is how intLiteralType becomes int32 (a subtype) when it is substituted for a TypeVariable. This
> +    // is not to say that the language supports subtyping everywhere, since declared types never experience
> +    // subtyping. Subtyping only emerges for literal types like nullType and intLiteralType.

I will revert.  This comment is wrong; I wrote it as I was exploring an alternate approach.

[Filip Pizlo]

Created attachment 320791 [details]
the patch

[Filip Pizlo]

Landed in https://trac.webkit.org/changeset/222038/webkit

[Keith Miller]

Comment on attachment 320791 [details]
the patch

seems reasonable. r=me.

[Radar WebKit Bug Importer]

<rdar://problem/34694485>

[Myles C. Maxfield]

Migrated to https://github.com/gpuweb/WHLSL/issues/140