Type Solver fails to discriminate tagged unions if the 'tag' property isn't directly used within type refinements

Bug Reports Engine Bugs
,
1

Type refinement doesn’t occur if the discriminating property is localized

--!strict

type Circle = {
	Radius	: number,
	Type	: 'C'
}
type Rectangle = {
	Size	: vector,
	Type	: 'R'
}
type Object = Circle | Rectangle

local object = {} :: Object
local objectType = object.Type

if objectType == 'C' then
	math.floor(object.Radius)	--Type Error: Key 'Radius' is missing from 'Rectangle' in the type 'Circle | Rectangle'
elseif objectType == 'R' then
	vector.floor(object.Size)	--Type Error: Key 'Size' is missing from 'Circle' in the type 'Circle | Rectangle'
end

Only works if said property directly used for refinement

local object = {} :: Object

if object.Type == 'C' then
	math.floor(object.Radius)	--No Error
elseif object.Type == 'R' then
	vector.floor(object.Size)	--No Error
end

This could be fixed by forcibly type casting on each access to ‘object’, but in cases where the tagged union has many types could lead to messy and seemingly convoluted code.

1 Like
2

Hi there, thanks for the report! While we recognize that this limitation might be frustrating, it’s not a bug, and is intended behavior. In general, it is impossible for any programming language to be able to make a judgment about what the precise type of a binding will be at runtime through arbitrary control flow in a program. This was proven to be true in the 1950s as Rice’s Theorem.

As a result, we have to make a set of tradeoffs intrinsically in how refinements will work. It’d be possible, in principle, to allow trivial cases like when you bind typeof(foo) to a local variable and then branch on it later, but small variations of that program where you made things a little bit more complicated would suddenly stop working. In order to provide a good developer experience, we need the rules for when refinements do or don’t fire to be predictable (that way you can know, as you’re writing the code, whether or not you can expect it to pass the type checker). Our feeling right now is that refinements are already sufficiently complex in their current form, and we’re not interested in changes like this that would make forming a mental model of when they apply substantially more difficult.

1 Like