What meaning (both from user and typechecker perspective) does synthax "Set _" have ? If I understand correctly, it is instruction to infer level from context, but how it is done ?