microsoft / qsharp

Azure Quantum Development Kit, including the Q# programming language, resource estimator, and Quantum Katas
https://microsoft.github.io/qsharp/
MIT License
439 stars 89 forks source link

Type inference should have appropriate errors for ambiguous types #152

Closed swernli closed 1 year ago

swernli commented 1 year ago

In circumstances where generics don't have enough information to resolve to a concrete type, type inference should have an error about ambiguous types. For example:

let x = Length([]);

The type of the array is not known, so the generic on Length cannot be made concrete. This does not interfere with the evaluator, which does not care about generics, but could become a problem for code generation.

swernli commented 1 year ago

It's possible this would be less of an issue with the idea to skip monomorphization in favor of untyped pointers in code generation. We should avoid introducing new errors for this until it we have a better understanding of what the actual error cases are.

bamarsha commented 1 year ago

I disagree - we should still treat ambiguous types as an error. For one, we can't rule out wanting monomorphization in the future.

Other than codegen, ambiguous types also create issues for type classes and bounded polymorphism, which we probably want to add to Q# in the future. If a bounded type parameter is instantiated ambiguously, then there is no way to know which type class instance to use. Since the choice can change the behavior of the program, it means that the program has no meaning, which means the type system has failed.

Ambiguous type errors also aren't "new errors" - the old Q# compiler disallowed ambiguous types, too. And although the two potential problems above are both future problems only, relaxing the restrictions now and then adding them back later is a lot harder (in terms of breaking changes) than just keeping the errors in.