March 18, 2019
1:26 p.m.
Totally agree re: allowing Literals to interact normally with the type system as much as possible. I think option 1 (not allowing Literals in "implicit" type variables) is unfortunately a violation of that principle and could get confusing. I agree that option 2 (never naturally inferring Literal, even in arguments) would be super annoying and so is probably not good. Deploying Literals internally, allowing it in type variables (which is helpful for some tensor typing work we're doing) didn't have much backwards compatibility issues (but there were some), which seems to suggest that saying that this is best-effort is the best road to take.