@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.

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

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)