[RFC FS-1071] Witnesses passing for trait-constraints w.r.t. quotations

[dsyme]

Implementation for RFC FS-1071 - Witness passing for quotations using SRTP-constrained functions and methods

F# quotations of code using SRTP constraint trait calls don't contain sufficient information to represent the semantic intent of the code. Specifically the quotations are missing any record of the resolution of SRTP constraints or how to execute constraint calls.

This RFC addresses this problem by incorporating the necessary information into both quotations and the code laid down for dynamic interpretation of quotations.

TODO

• Allow ReflectedDefiniton on let inline functions that utilise witnesses (currently no witness arguments are bound in the generated lambda and there is no representation for the utilization of the witness. Needs new LambdaWithWitnesses to detect the witnesses)
• This example causes a failure Members using overloaded operators defined over member's containing type require unsatisfiable constraint #968

[dsyme]

@cartermp @KevinRansom @TIHan One specific motivation for fixing this core problem with quotations is the need to use quotations more heavily in any future evolution of the "F# for AI models" prototype I've been involved in.

[TIHan]

What does the term "witness" mean in this case?

[dsyme]

What does the term "witness" mean in this case?

A witness is the lambda term that represents the solution to an SRTP constraint. For example, if you use + in generic inline math code, then there will be an extra hidden parameter in the compiled form of that generic code. You will a type-specialized lambda passed as that argument at callsites where the generic function is called at a non-generic, specific type, e.g.

• You will see (fun (a: double) (b: double) -> a + b) passed in at the place where the code is specialized at type double.

• You will see (fun (a: TimeSpan) (b: TimeSpan) -> TimeSpan.op_Addition(a,b)) passed in at the place where the code is specialized at type TimeSpan.

Because this is only about quotations, you only actually see these witnesses by matching on the quotation using the new CallWithWitnesses active pattern when processing the quotation.

Each witness effectively records the resolution/implementation of a trait constraint in quotations and/or compiled code.

(note passing implicit witnesses is the standard technique for implementing Haskell type classes)

[dsyme]

Closed in favour of #6810 from feature branch