squash unsolved variables arising from witness generation

Author: dsyme

src/fsharp/CompileOptions.fs

@@ -1055,7 +1055,7 @@ let internalFlags (tcConfigB:TcConfigBuilder) =
   [
     CompilerOption
        ("stamps", tagNone,
-        OptionUnit ignore,
+        OptionSet Tastops.DebugPrint.layoutStamps,
         Some(InternalCommandLineOption("--stamps", rangeCmdArgs)), None)
 
     CompilerOption

src/fsharp/ConstraintSolver.fs

@@ -106,13 +106,8 @@ let NewByRefKindInferenceType (g: TcGlobals) m =
 
 let NewInferenceTypes l = l |> List.map (fun _ -> NewInferenceType ()) 
 
-// QUERY: should 'rigid' ever really be 'true'? We set this when we know 
-// we are going to have to generalize a typar, e.g. when implementing a 
-// abstract generic method slot. But we later check the generalization 
-// condition anyway, so we could get away with a non-rigid typar. This 
-// would sort of be cleaner, though give errors later. 
 let FreshenAndFixupTypars (traitCtxt: ITraitContext option) m rigid fctps tinst tpsorig = 
-    let copy_tyvar (tp: Typar) =  NewCompGenTypar (tp.Kind, rigid, tp.StaticReq, (if rigid=TyparRigidity.Rigid then TyparDynamicReq.Yes else TyparDynamicReq.No), false)
+    let copy_tyvar (tp: Typar) = NewCompGenTypar (tp.Kind, rigid, tp.StaticReq, (if rigid=TyparRigidity.Rigid then TyparDynamicReq.Yes else TyparDynamicReq.No), false)
     let tps = tpsorig |> List.map copy_tyvar 
     let renaming, tinst = FixupNewTypars traitCtxt m fctps tinst tpsorig tps
     tps, renaming, tinst
@@ -322,13 +317,13 @@ let rec occursCheck g un ty =
 type PermitWeakResolution = 
 
     /// Represents the point where we are generalizing inline code
-    | YesAtInlineGeneralization
+    | LegacyYesAtInlineGeneralization
 
     /// Represents points where we are choosing a default solution to trait constraints
     | YesAtChooseSolution
 
-    /// Represents legacy invocations of the constraint solver during codegen
-    | YesAtCodeGen
+    /// Represents invocations of the constraint solver during codegen or inlining to determine witnesses
+    | LegacyYesAtCodeGen
 
     /// No weak resolution allowed
     | No
@@ -339,15 +334,15 @@ type PermitWeakResolution =
         if g.langVersion.SupportsFeature LanguageFeature.ExtensionConstraintSolutions then 
             match x with
             | YesAtChooseSolution -> true
-            | YesAtInlineGeneralization
-            | YesAtCodeGen
+            | LegacyYesAtCodeGen
+            | LegacyYesAtInlineGeneralization
             | No -> false
         else
             //legacy 
             match x with
-            | YesAtChooseSolution -> true
-            | YesAtCodeGen -> true
-            | YesAtInlineGeneralization -> true
+            | YesAtChooseSolution
+            | LegacyYesAtCodeGen
+            | LegacyYesAtInlineGeneralization -> true
             | No -> false
 
 
@@ -447,7 +442,7 @@ let IsBinaryOpArgTypePair p1 p2 permitWeakResolution minfos g ty1 ty2 =
 
     // During regular canonicalization (weak resolution) we don't do any check on the other type at all - we 
     // ignore the possibility that method overloads may resolve the constraint
-    | PermitWeakResolution.YesAtInlineGeneralization
+    | PermitWeakResolution.LegacyYesAtInlineGeneralization
     | PermitWeakResolution.YesAtChooseSolution -> 
         // weak resolution lets the other type be a variable type
         isTyparTy g ty2 || 
@@ -457,7 +452,7 @@ let IsBinaryOpArgTypePair p1 p2 permitWeakResolution minfos g ty1 ty2 =
         typeEquivAux EraseMeasures g ty1 ty2
 
     // During codegen we only apply a builtin resolution if both the types are correct
-    | PermitWeakResolution.YesAtCodeGen ->
+    | PermitWeakResolution.LegacyYesAtCodeGen ->
         p2 ty2 &&
         // All built-in rules only apply in cases where left and right operator types are equal (after
         // erasing units)
@@ -1853,7 +1848,7 @@ and SolveRelevantMemberConstraintsForTypar (csenv:ConstraintSolverEnv) ndeep (pe
         SolveMemberConstraint csenv true permitWeakResolution (ndeep+1) m2 trace traitInfo)
 
 and CanonicalizeRelevantMemberConstraints (csenv: ConstraintSolverEnv) ndeep trace tps isInline =
-    let permitWeakResolution = (if isInline then PermitWeakResolution.YesAtInlineGeneralization else PermitWeakResolution.YesAtChooseSolution)
+    let permitWeakResolution = (if isInline then PermitWeakResolution.LegacyYesAtInlineGeneralization else PermitWeakResolution.YesAtChooseSolution)
     SolveRelevantMemberConstraints csenv ndeep permitWeakResolution trace tps
 
 and AddMemberConstraint (csenv: ConstraintSolverEnv) ndeep m2 (trace: OptionalTrace) traitInfo support (frees: Typar list) =
@@ -3148,17 +3143,6 @@ let CreateCodegenState tcVal g amap =
       ExtraCxs = HashMultiMap(10, HashIdentity.Structural)
       InfoReader = new InfoReader(g, amap) }
 
-let CodegenWitnessThatTypeSupportsTraitConstraint 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.YesAtCodeGen 0 m NoTrace traitInfo
-
-    let sln = GenWitnessExpr amap g m traitInfo argExprs
-    return sln
-  }
-
 let ChooseTyparSolutionAndSolve css denv tp =
     let g = css.g
     let amap = css.amap
@@ -3169,6 +3153,25 @@ let ChooseTyparSolutionAndSolve css denv tp =
         (fun err -> ErrorD(ErrorFromApplyingDefault(g, denv, tp, max, err, m)))
     |> RaiseOperationResult
 
+let CodegenWitnessThatTypeSupportsTraitConstraint tcVal g amap m (traitInfo: TraitConstraintInfo) argExprs = trackErrors {
+    let css = CreateCodegenState tcVal g amap
+    let denv = DisplayEnv.Empty g
+
+    let csenv = MakeConstraintSolverEnv ContextInfo.NoContext css m denv
+
+    let! _res = SolveMemberConstraint csenv true PermitWeakResolution.LegacyYesAtCodeGen 0 m NoTrace traitInfo
+    let sln = GenWitnessExpr amap g m traitInfo argExprs
+
+    sln |> Option.iter (fun slnExpr -> 
+        let unsolved = FSharp.Compiler.FindUnsolved.UnsolvedTyparsOfExpr g amap denv slnExpr
+
+        unsolved |> List.iter (fun tp -> 
+                if (tp.Rigidity <> TyparRigidity.Rigid) && not tp.IsSolved then 
+                    ChooseTyparSolutionAndSolve css denv tp))
+
+    return sln
+  }
+
 let CheckDeclaredTypars denv css m typars1 typars2 = 
     let csenv = MakeConstraintSolverEnv ContextInfo.NoContext css m denv
     TryD_IgnoreAbortForFailedOverloadResolution

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

@@ -446,6 +446,12 @@
     <Compile Include="..\PatternMatchCompilation.fs">
       <Link>Logic\PatternMatchCompilation.fs</Link>
     </Compile>
+    <Compile Include="..\FindUnsolved.fsi">
+      <Link>Logic\FindUnsolved.fsi</Link>
+    </Compile>
+    <Compile Include="..\FindUnsolved.fs">
+      <Link>Logic\FindUnsolved.fs</Link>
+    </Compile>
     <Compile Include="..\ConstraintSolver.fsi">
       <Link>Logic\ConstraintSolver.fsi</Link>
     </Compile>
@@ -458,12 +464,6 @@
     <Compile Include="..\CheckFormatStrings.fs">
       <Link>Logic\CheckFormatStrings.fs</Link>
     </Compile>
-    <Compile Include="..\FindUnsolved.fsi">
-      <Link>Logic\FindUnsolved.fsi</Link>
-    </Compile>
-    <Compile Include="..\FindUnsolved.fs">
-      <Link>Logic\FindUnsolved.fs</Link>
-    </Compile>
     <Compile Include="..\QuotationTranslator.fsi">
       <Link>Logic\QuotationTranslator.fsi</Link>
     </Compile>

src/fsharp/FindUnsolved.fs

@@ -276,4 +276,13 @@ let UnsolvedTyparsOfModuleDef g amap denv (mdef, extraAttribs) =
    accAttribs cenv Nix extraAttribs
    List.rev cenv.unsolved
 
+let UnsolvedTyparsOfExpr g amap denv expr =
+   let cenv = 
+      { g =g  
+        amap=amap 
+        denv=denv 
+        unsolved = [] }
+   accExpr cenv Nix expr
+   List.rev cenv.unsolved
+
 

src/fsharp/FindUnsolved.fsi

@@ -10,3 +10,6 @@ open FSharp.Compiler.Import
 
 /// Find all unsolved inference variables after type inference for an entire file
 val UnsolvedTyparsOfModuleDef: g: TcGlobals -> amap: ImportMap -> denv: DisplayEnv -> mdef : ModuleOrNamespaceExpr * extraAttribs: Attrib list -> Typar list
+
+/// Find all unsolved inference variables after adhoc generation of witness
+val UnsolvedTyparsOfExpr: g: TcGlobals -> amap: ImportMap -> denv: DisplayEnv -> expr: Expr -> Typar list

src/fsharp/IlxGen.fs

@@ -389,7 +389,7 @@ let ComputeTypeAccess (tref: ILTypeRef) hidden =
 type TypeReprEnv(reprs: Map<Stamp, uint16>, count: int) =
 
     /// Lookup a type parameter
-    member __.Item (tp: Typar, m: range) =
+    member __.LookupTyparRepr (tp: Typar, m: range) =
         try reprs.[tp.Stamp]
         with :? KeyNotFoundException ->
           errorR(InternalError("Undefined or unsolved type variable: " + showL(typarL tp), m))
@@ -540,7 +540,7 @@ and GenTypeAux amap m (tyenv: TypeReprEnv) voidOK ptrsOK ty =
         if tps.IsEmpty then GenTypeAux amap m tyenv VoidNotOK ptrsOK tau
         else EraseClosures.mkILTyFuncTy g.ilxPubCloEnv
 
-    | TType_var tp -> mkILTyvarTy tyenv.[tp, m]
+    | TType_var tp -> mkILTyvarTy (tyenv.LookupTyparRepr(tp, m))
 
     | TType_measure _ -> g.ilg.typ_Int32
 
@@ -4361,7 +4361,7 @@ and GenGenericParams cenv eenv tps =
     tps |> DropErasedTypars |> List.map (GenGenericParam cenv eenv)
 
 and GenGenericArgs m (tyenv: TypeReprEnv) tps =
-    tps |> DropErasedTypars |> List.map (fun c -> (mkILTyvarTy tyenv.[c, m]))
+    tps |> DropErasedTypars |> List.map (fun c -> mkILTyvarTy (tyenv.LookupTyparRepr(c, m)))
 
 /// Generate the closure class for a function
 and GenLambdaClosure cenv (cgbuf: CodeGenBuffer) eenv isLocalTypeFunc selfv expr =

src/fsharp/TastOps.fs

@@ -2743,7 +2743,7 @@ type DisplayEnv =
         maxMembers = None
         showObsoleteMembers = false
         showHiddenMembers = false
-        showTyparBinding = false
+        showTyparBinding = true
         showImperativeTyparAnnotations = false
         suppressInlineKeyword = false
         suppressMutableKeyword = false
@@ -3383,8 +3383,9 @@ module DebugPrint =
             else stat
         stat
 
-    let stampL _n w = 
-        w
+    let layoutStamps = ref false
+    let stampL (n: int64) w = 
+        if layoutStamps.Value then w ++ (wordL (tagText ("#" + string n))) else w
 
     let layoutTyconRef (tc: TyconRef) = 
         wordL (tagText tc.DisplayNameWithStaticParameters) |> stampL tc.Stamp
@@ -3901,7 +3902,7 @@ module DebugPrint =
                 wordL(tagText "bytes++")
             | Expr.Op (TOp.UInt16s _, _, _, _) -> wordL(tagText "uint16++")
             | Expr.Op (TOp.RefAddrGet _, _tyargs, _args, _) -> wordL(tagText "GetRefLVal...")
-            | Expr.Op (TOp.TraitCall _, _tyargs, _args, _) -> wordL(tagText "traitcall...")
+            | Expr.Op (TOp.TraitCall traitInfo, _tyargs, _args, _) -> wordL(tagText "traitcall") ^^ auxTraitL SimplifyTypes.typeSimplificationInfo0 traitInfo
             | Expr.Op (TOp.ExnFieldGet _, _tyargs, _args, _) -> wordL(tagText "TOp.ExnFieldGet...")
             | Expr.Op (TOp.ExnFieldSet _, _tyargs, _args, _) -> wordL(tagText "TOp.ExnFieldSet...")
             | Expr.Op (TOp.TryFinally _, _tyargs, _args, _) -> wordL(tagText "TOp.TryFinally...")
@@ -7499,7 +7500,7 @@ let AdjustPossibleSubsumptionExpr g (expr: Expr) (suppliedArgs: Expr list) : (Ex
 
             let curriedInputTys, _ = stripFunTy g inputTy
 
-            assert (curriedActualArgTys.Length = curriedInputTys.Length)
+            if curriedActualArgTys.Length <> curriedInputTys.Length then None else
 
             let argTys = (curriedInputTys, curriedActualArgTys) ||> List.mapi2 (fun i x y -> (i, x, y))
 

src/fsharp/TastOps.fsi

@@ -1303,6 +1303,9 @@ module DebugPrint =
     /// A global flag indicating whether debug output should include ranges
     val layoutRanges : bool ref
 
+    /// A global flag indicating whether debug output should include stamps
+    val layoutStamps : bool ref
+
     /// Convert a type to a string for debugging purposes
     val showType : TType -> string
 

src/fsharp/TypeChecker.fs

@@ -11481,7 +11481,7 @@ and TcLetBinding cenv isUse env containerInfo declKind tpenv (synBinds, synBinds
         let (ExplicitTyparInfo(_, declaredTypars, canInferTypars)) = flex
         let allDeclaredTypars = enclosingDeclaredTypars @ declaredTypars
         let generalizedTypars, prelimValSchemes2 = 
-            let canInferTypars = GeneralizationHelpers. ComputeCanInferExtraGeneralizableTypars (containerInfo.ParentRef, canInferTypars, None)
+            let canInferTypars = GeneralizationHelpers.ComputeCanInferExtraGeneralizableTypars (containerInfo.ParentRef, canInferTypars, None)
 
             let maxInferredTypars = freeInTypeLeftToRight cenv.g false tauTy
 
@@ -11494,6 +11494,10 @@ and TcLetBinding cenv isUse env containerInfo declKind tpenv (synBinds, synBinds
                    GeneralizationHelpers.ComputeAndGeneralizeGenericTypars
                        (cenv, denv, m, freeInEnv, canInferTypars, canConstrain, inlineFlag, Some rhsExpr, allDeclaredTypars, maxInferredTypars, tauTy, false)
 
+            //printfn "Generalizing 'let' at %A" m
+            //printfn "  generalizedTypars = %s" (Layout.showL (DebugPrint.typarsL generalizedTypars))
+            //printfn "  rhsExpr = %s" (Layout.showL (DebugPrint.exprL cenv.g rhsExpr))
+
             let prelimValSchemes2 = GeneralizeVals cenv denv enclosingDeclaredTypars generalizedTypars nameToPrelimValSchemeMap
 
             generalizedTypars, prelimValSchemes2
@@ -12394,6 +12398,10 @@ and TcLetrecComputeAndGeneralizeGenericTyparsForBinding cenv denv freeInEnv (pgr
 
     let canGeneralizeConstrained = GeneralizationHelpers.CanGeneralizeConstrainedTyparsForDecl rbinfo.DeclKind
     let generalizedTypars = GeneralizationHelpers.ComputeAndGeneralizeGenericTypars (cenv, denv, m, freeInEnv, canInferTypars, canGeneralizeConstrained, inlineFlag, Some expr, allDeclaredTypars, maxInferredTypars, tau, isCtor)
+
+    printfn "Generalizing 'member/let-rec' at %A" m
+    printfn "  generalizedTypars = %s" (Layout.showL (DebugPrint.typarsL generalizedTypars))
+    printfn "  rhsExpr = %s" (Layout.showL (DebugPrint.exprL cenv.g expr))
     generalizedTypars
 
 /// Compute the type variables which may have member constraints that need to be canonicalized prior to generalization 

src/fsharp/tast.fs

@@ -5714,17 +5714,20 @@ let MakeRecdFieldsTable ucs: TyconRecdFields =
     { FieldsByIndex = Array.ofList ucs 
       FieldsByName = ucs |> NameMap.ofKeyedList (fun rfld -> rfld.Name) }
 
-
 let MakeUnionCases ucs: TyconUnionData = 
     { CasesTable=MakeUnionCasesTable ucs 
       CompiledRepresentation=newCache() }
 
 let MakeUnionRepr ucs = TUnionRepr (MakeUnionCases ucs)
 
 let NewTypar (kind, rigid, Typar(id, staticReq, isCompGen), isFromError, dynamicReq, attribs, eqDep, compDep) = 
+    let stamp = newStamp()
+    //printfn "stamp = %d" stamp
+    //if stamp = 16193L then 
+    //    assert false
     Typar.New
       { typar_id = id 
-        typar_stamp = newStamp() 
+        typar_stamp = stamp 
         typar_flags= TyparFlags(kind, rigid, isFromError, isCompGen, staticReq, dynamicReq, eqDep, compDep) 
         typar_solution = None
         typar_astype = Unchecked.defaultof<_>