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

src/fsharp/ConstraintSolver.fs

@@ -245,6 +245,11 @@ type ConstraintSolverState =
       /// The function used to freshen values we encounter during trait constraint solving
       TcVal: TcValF
 
+      /// Indicates if the constraint solver is being run after type checking is complete,
+      /// e.g. during codegen to determine solutions and witnesses for trait constraints.
+      /// Suppresses the generation of certain errors such as missing constraint warnings.
+      codegen: bool
+
       /// This table stores all unsolved, ungeneralized trait constraints, indexed by free type variable.
       /// That is, there will be one entry in this table for each free type variable in 
       /// each outstanding, unsolved, ungeneralized trait constraint. Constraints are removed from the table and resolved 
@@ -257,6 +262,7 @@ type ConstraintSolverState =
           amap = amap 
           ExtraCxs = HashMultiMap(10, HashIdentity.Structural)
           InfoReader = infoReader
+          codegen = false
           TcVal = tcVal } 
 
 type ConstraintSolverEnv = 
@@ -1939,14 +1945,14 @@ and AddConstraint (csenv: ConstraintSolverEnv) ndeep m2 trace tp newConstraint
               | (TyparRigidity.Rigid | TyparRigidity.WillBeRigid), TyparConstraint.DefaultsTo _ -> true
               | _ -> false) then 
             ()
-        elif tp.Rigidity = TyparRigidity.Rigid then
+        elif tp.Rigidity = TyparRigidity.Rigid && not csenv.SolverState.codegen then
             return! ErrorD (ConstraintSolverMissingConstraint(denv, tp, newConstraint, m, m2)) 
         else
             // It is important that we give a warning if a constraint is missing from a 
             // will-be-made-rigid type variable. This is because the existence of these warnings
             // is relevant to the overload resolution rules (see 'candidateWarnCount' in the overload resolution
             // implementation).
-            if tp.Rigidity.WarnIfMissingConstraint then
+            if tp.Rigidity.WarnIfMissingConstraint  && not csenv.SolverState.codegen then
                 do! WarnD (ConstraintSolverMissingConstraint(denv, tp, newConstraint, m, m2))
 
             let newConstraints = 
@@ -3059,20 +3065,36 @@ let CreateCodegenState tcVal g amap =
       amap = amap
       TcVal = tcVal
       ExtraCxs = HashMultiMap(10, HashIdentity.Structural)
-      InfoReader = new InfoReader(g, amap) }
+      InfoReader = new InfoReader(g, amap)
+      codegen = true }
 
 /// Generate a witness expression if none is otherwise available, e.g. in legacy non-witness-passing code
-let CodegenWitnessForTraitConstraint tcVal g amap m (traitInfo: TraitConstraintInfo) argExprs = trackErrors {
+let CodegenWitnessForTraitConstraint tcVal g amap m (traitInfo:TraitConstraintInfo) argExprs = trackErrors {
     let css = CreateCodegenState tcVal g amap
-
     let csenv = MakeConstraintSolverEnv ContextInfo.NoContext css m (DisplayEnv.Empty g)
-
     let! _res = SolveMemberConstraint csenv true PermitWeakResolution.Yes 0 m NoTrace traitInfo
-
     let sln = GenWitnessExpr amap g m traitInfo argExprs
     return sln
   }
 
+/// Generate the lambda argument passed for a use of a generic construct that accepts trait witnesses
+let CodegenWitnessesForTyparInst tcVal g amap m typars tyargs = trackErrors {
+    let css = CreateCodegenState tcVal g amap
+    let csenv = MakeConstraintSolverEnv ContextInfo.NoContext css m (DisplayEnv.Empty g)
+    let ftps, _renaming, tinst = FreshenTypeInst m typars
+    let traitInfos = GetTraitConstraintInfosOfTypars g ftps 
+    do! SolveTypeEqualsTypeEqns csenv 0 m NoTrace None tinst tyargs
+    return MethodCalls.GenWitnessArgs amap g m traitInfos
+  }
+
+/// Generate the lambda argument passed for a use of a generic construct that accepts trait witnesses
+let CodegenWitnessesForTraitWitness tcVal g amap m traitInfo = trackErrors {
+    let css = CreateCodegenState tcVal g amap
+    let csenv = MakeConstraintSolverEnv ContextInfo.NoContext css m (DisplayEnv.Empty g)
+    let! _res = SolveMemberConstraint csenv true PermitWeakResolution.Yes 0 m NoTrace traitInfo
+    return MethodCalls.GenWitnessExprLambda amap g m traitInfo
+  }
+
 /// For some code like "let f() = ([] = [])", a free choice is made for a type parameter
 /// for an interior type variable.  This chooses a solution for a type parameter subject
 /// to its constraints and applies that solution by using a constraint.
@@ -3118,6 +3140,7 @@ let IsApplicableMethApprox g amap m (minfo: MethInfo) availObjTy =
               amap = amap
               TcVal = (fun _ -> failwith "should not be called")
               ExtraCxs = HashMultiMap(10, HashIdentity.Structural)
+              codegen = false
               InfoReader = new InfoReader(g, amap) }
         let csenv = MakeConstraintSolverEnv ContextInfo.NoContext css m (DisplayEnv.Empty g)
         let minst = FreshenMethInfo m minfo

src/fsharp/ConstraintSolver.fsi

@@ -192,12 +192,18 @@ val SolveTypeAsError: DisplayEnv -> ConstraintSolverState -> range -> TType -> u
 val ApplyTyparDefaultAtPriority: DisplayEnv -> ConstraintSolverState -> priority: int -> Typar -> unit
 
 /// Generate a witness expression if none is otherwise available, e.g. in legacy non-witness-passing code
-val CodegenWitnessForTraitConstraint: TcValF -> TcGlobals -> ImportMap -> range -> TraitConstraintInfo -> Expr list -> OperationResult<Expr option>
+val CodegenWitnessForTraitConstraint : TcValF -> TcGlobals -> ImportMap -> range -> TraitConstraintInfo -> Expr list -> OperationResult<Expr option>
+
+/// Generate the arguments passed when using a generic construct that accepts traits witnesses
+val CodegenWitnessesForTyparInst : TcValF -> TcGlobals -> ImportMap -> range -> Typars -> TType list -> OperationResult<Choice<TraitConstraintInfo, Expr> list>
+
+/// Generate the lambda argument passed for a use of a generic construct that accepts trait witnesses
+val CodegenWitnessesForTraitWitness : TcValF -> TcGlobals -> ImportMap -> range -> TraitConstraintInfo -> OperationResult<Choice<TraitConstraintInfo, Expr>>
 
 /// For some code like "let f() = ([] = [])", a free choice is made for a type parameter
 /// for an interior type variable.  This chooses a solution for a type parameter subject
 /// to its constraints and applies that solution by using a constraint.
-val ChooseTyparSolutionAndSolve: ConstraintSolverState -> DisplayEnv -> Typar -> unit
+val ChooseTyparSolutionAndSolve : ConstraintSolverState -> DisplayEnv -> Typar -> unit
 
 val IsApplicableMethApprox: TcGlobals -> ImportMap -> range -> MethInfo -> TType -> bool
 

src/fsharp/FSComp.txt

@@ -1512,3 +1512,4 @@ featureFixedIndexSlice3d4d,"fixed-index slice 3d/4d"
 featureAndBang,"applicative computation expressions"
 featureNullableOptionalInterop,"nullable optional interop"
 featureDefaultInterfaceMemberConsumption,"default interface member consumption"
+featureWitnessPassing,"witness passing"

src/fsharp/FSharp.Compiler.Private/FSharp.Compiler.Private.fsproj

@@ -406,10 +406,10 @@
       <Link>TypedTree\TypedTreeOps.fs</Link>
     </Compile>
     <Compile Include="..\TypedTreePickle.fsi">
-      <Link>TypedTree\.TypedTreePickle.fsi</Link>
+      <Link>TypedTree\TypedTreePickle.fsi</Link>
     </Compile>
     <Compile Include="..\TypedTreePickle.fs">
-      <Link>TypedTree\.TypedTreePickle.fs</Link>
+      <Link>TypedTree\TypedTreePickle.fs</Link>
     </Compile>
     <Compile Include="..\import.fsi">
       <Link>Logic\import.fsi</Link>

src/fsharp/FSharp.Core/Linq.fs

@@ -396,7 +396,7 @@ module LeafExpressionConverter =
             | NullableGreaterEqNullableQ _ -> transBinOp inp env false args false Expression.GreaterThanOrEqual
             | NullableLessNullableQ _ -> transBinOp inp env false args false Expression.LessThan
             | NullableLessEqNullableQ _ -> transBinOp inp env false args false Expression.LessThanOrEqual
-
+            
             // Detect the F# quotation encoding of decimal literals
             | MakeDecimalQ (_, _, [Int32 lo; Int32 med; Int32 hi; Bool isNegative; Byte scale]) ->
                 Expression.Constant (new System.Decimal(lo, med, hi, isNegative, scale)) |> asExpr
@@ -414,33 +414,33 @@ module LeafExpressionConverter =
             | BitwiseOrQ _ -> transBinOp inp env false args false Expression.Or
             | BitwiseXorQ _ -> transBinOp inp env false args false Expression.ExclusiveOr
             | BitwiseNotQ (_, _, [x1]) -> Expression.Not(ConvExprToLinqInContext env x1) |> asExpr
-
-            | CheckedNeg (_, _, [x1]) -> Expression.NegateChecked(ConvExprToLinqInContext env x1) |> asExpr
+            
+            | CheckedNeg (_, _, [x1]) -> Expression.NegateChecked(ConvExprToLinqInContext env x1)                                |> asExpr
             | CheckedPlusQ _ -> transBinOp inp env false args false Expression.AddChecked
             | CheckedMinusQ _ -> transBinOp inp env false args false Expression.SubtractChecked
             | CheckedMultiplyQ _ -> transBinOp inp env false args false Expression.MultiplyChecked
-
+            
             | NullablePlusQ _ -> transBinOp inp env false args true Expression.Add
             | PlusNullableQ _ -> transBinOp inp env true args false Expression.Add
             | NullablePlusNullableQ _ -> transBinOp inp env false args false Expression.Add
-
+            
             | NullableMinusQ _ -> transBinOp inp env false args true Expression.Subtract
             | MinusNullableQ _ -> transBinOp inp env true args false Expression.Subtract
             | NullableMinusNullableQ _ -> transBinOp inp env false args false Expression.Subtract
-
+            
             | NullableMultiplyQ _ -> transBinOp inp env false args true Expression.Multiply
             | MultiplyNullableQ _ -> transBinOp inp env true args false Expression.Multiply
             | NullableMultiplyNullableQ _ -> transBinOp inp env false args false Expression.Multiply
-
+            
             | NullableDivideQ _ -> transBinOp inp env false args true Expression.Divide
             | DivideNullableQ _ -> transBinOp inp env true args false Expression.Divide
             | NullableDivideNullableQ _ -> transBinOp inp env false args false Expression.Divide
-
+            
             | NullableModuloQ _ -> transBinOp inp env false args true Expression.Modulo
             | ModuloNullableQ _ -> transBinOp inp env true args false Expression.Modulo
             | NullableModuloNullableQ _ -> transBinOp inp env false args false Expression.Modulo
 
-            | ConvNullableCharQ (_, _, [x1]) -> Expression.Convert(ConvExprToLinqInContext env x1, typeof<Nullable<char>>) |> asExpr
+            | ConvNullableCharQ    (_, _, [x1]) -> Expression.Convert(ConvExprToLinqInContext env x1, typeof<Nullable<char>>) |> asExpr
             | ConvNullableDecimalQ (_, _, [x1]) -> Expression.Convert(ConvExprToLinqInContext env x1, typeof<Nullable<decimal>>) |> asExpr
             | ConvNullableFloatQ (_, _, [x1]) -> Expression.Convert(ConvExprToLinqInContext env x1, typeof<Nullable<float>>) |> asExpr
             | ConvNullableDoubleQ (_, _, [x1]) -> Expression.Convert(ConvExprToLinqInContext env x1, typeof<Nullable<double>>) |> asExpr
@@ -496,10 +496,19 @@ module LeafExpressionConverter =
             // Throw away markers inserted to satisfy C#'s design where they pass an argument
             // or type T to an argument expecting Expression<T>.
             | ImplicitExpressionConversionHelperQ (_, [_], [x1]) -> ConvExprToLinqInContext env x1
-
-            | _ ->
-                let argsP = ConvExprsToLinq env args
-                Expression.Call(ConvObjArg env objOpt None, minfo, argsP) |> asExpr
+
+            /// Use witnesses if they are available
+            | CallWithWitnesses (objArgOpt, _, minfo2, witnessArgs, args) -> 
+                let fullArgs = witnessArgs @ args
+                let replacementExpr =
+                    match objArgOpt with
+                    | None -> Expr.Call(minfo2, fullArgs)
+                    | Some objArg -> Expr.Call(objArg, minfo2, fullArgs)
+                ConvExprToLinqInContext env replacementExpr
+
+            | _ -> 
+                let argsP = ConvExprsToLinq env args 
+                Expression.Call(ConvObjArg env objOpt None, minfo, argsP) |> asExpr  
 
 #if !NO_CURRIED_FUNCTION_OPTIMIZATIONS
         // f x1 x2 x3 x4 --> InvokeFast4
@@ -650,12 +659,11 @@ module LeafExpressionConverter =
             let convType = lambdaTy.MakeGenericType tyargs
             let convDelegate = Expression.Lambda(convType, bodyP, [| vP |]) |> asExpr
             Expression.Call(typeof<FuncConvert>, "ToFSharpFunc", tyargs, [| convDelegate |]) |> asExpr
-
         | _ ->
             failConvert inp
 
     and failConvert inp =
-        raise (new NotSupportedException(Printf.sprintf "Could not convert the following F# Quotation to a LINQ Expression Tree\n--------\n%A\n-------------\n" inp))
+            raise (new NotSupportedException(Printf.sprintf "Could not convert the following F# Quotation to a LINQ Expression Tree\n--------\n%A\n-------------\n" inp))
 
     and transBinOp inp env addConvertLeft args addConvertRight (exprErasedConstructor : _ * _ -> _) =
         match args with 

src/fsharp/FSharp.Core/nativeptr.fsi

@@ -12,31 +12,27 @@ namespace Microsoft.FSharp.NativeInterop
     module NativePtr =
 
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("OfNativeIntInlined")>]
         /// <summary>Returns a typed native pointer for a given machine address.</summary>
         /// <param name="address">The pointer address.</param>
         /// <returns>A typed pointer.</returns>
         val inline ofNativeInt : address:nativeint -> nativeptr<'T>
 
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("ToVoidPtrInlined")>]
         /// <summary>Returns an untyped native pointer for a given typed pointer.</summary>
         /// <param name="address">The pointer address.</param>
         /// <returns>A typed pointer.</returns>
         val inline toVoidPtr : address:nativeptr<'T> -> voidptr
 
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("OfVoidPtrInlined")>]
         /// <summary>Returns a typed native pointer for a untyped native pointer.</summary>
         /// <param name="address">The untyped pointer.</param>
         /// <returns>A typed pointer.</returns>
         val inline ofVoidPtr : voidptr -> nativeptr<'T>
 
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("ToNativeIntInlined")>]
         /// <summary>Returns a machine address for a given typed native pointer.</summary>
         /// <param name="address">The input pointer.</param>
@@ -45,7 +41,6 @@ namespace Microsoft.FSharp.NativeInterop
 
 
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("AddPointerInlined")>]
         /// <summary>Returns a typed native pointer by adding index * sizeof&lt;'T&gt; to the 
         /// given input pointer.</summary>
@@ -55,7 +50,6 @@ namespace Microsoft.FSharp.NativeInterop
         val inline add : address:nativeptr<'T> -> index:int -> nativeptr<'T>
 
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("GetPointerInlined")>]
         /// <summary>Dereferences the typed native pointer computed by adding index * sizeof&lt;'T&gt; to the 
         /// given input pointer.</summary>
@@ -65,23 +59,20 @@ namespace Microsoft.FSharp.NativeInterop
         val inline get : address:nativeptr<'T> -> index:int -> 'T
 
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("ReadPointerInlined")>]
         /// <summary>Dereferences the given typed native pointer.</summary>
         /// <param name="address">The input pointer.</param>
         /// <returns>The value at the pointer address.</returns>
         val inline read : address:nativeptr<'T> -> 'T
 
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("WritePointerInlined")>]
         /// <summary>Assigns the <c>value</c> into the memory location referenced by the given typed native pointer.</summary>
         /// <param name="address">The input pointer.</param>
         /// <param name="value">The value to assign.</param>
         val inline write : address:nativeptr<'T> -> value:'T -> unit
 
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("SetPointerInlined")>]
         /// <summary>Assigns the <c>value</c> into the memory location referenced by the typed native 
         /// pointer computed by adding index * sizeof&lt;'T&gt; to the given input pointer.</summary>
@@ -94,14 +85,12 @@ namespace Microsoft.FSharp.NativeInterop
         /// <param name="count">The number of objects of type T to allocate.</param>
         /// <returns>A typed pointer to the allocated memory.</returns>
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("StackAllocate")>]
         val inline stackalloc : count:int -> nativeptr<'T>
 
         /// <summary>Converts a given typed native pointer to a managed pointer.</summary>
         /// <param name="address">The input pointer.</param>
         /// <returns>The managed pointer.</returns>
         [<Unverifiable>]
-        [<NoDynamicInvocation>]
         [<CompiledName("ToByRefInlined")>]
         val inline toByRef : nativeptr<'T> -> byref<'T>