Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix 5580 and better encapsulate constraint solver #8294

Merged
merged 8 commits into from
Jan 22, 2020
Merged
Show file tree
Hide file tree
Changes from 6 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
244 changes: 181 additions & 63 deletions src/fsharp/ConstraintSolver.fs

Large diffs are not rendered by default.

127 changes: 72 additions & 55 deletions src/fsharp/ConstraintSolver.fsi
Original file line number Diff line number Diff line change
Expand Up @@ -17,32 +17,32 @@ open FSharp.Compiler.MethodCalls
open FSharp.Compiler.InfoReader

/// Create a type variable representing the use of a "_" in F# code
val NewAnonTypar : TyparKind * range * TyparRigidity * TyparStaticReq * TyparDynamicReq -> Typar
val NewAnonTypar: TyparKind * range * TyparRigidity * TyparStaticReq * TyparDynamicReq -> Typar

/// Create an inference type variable
val NewInferenceType : unit -> TType
val NewInferenceType: unit -> TType

/// Create an inference type variable for the kind of a byref pointer
val NewByRefKindInferenceType : TcGlobals -> range -> TType
val NewByRefKindInferenceType: TcGlobals -> range -> TType

/// Create an inference type variable representing an error condition when checking an expression
val NewErrorType : unit -> TType
val NewErrorType: unit -> TType

/// Create an inference type variable representing an error condition when checking a measure
val NewErrorMeasure : unit -> Measure
val NewErrorMeasure: unit -> Measure

/// Create a list of inference type variables, one for each element in the input list
val NewInferenceTypes : 'a list -> TType list
val NewInferenceTypes: 'a list -> TType list

/// Given a set of formal type parameters and their constraints, make new inference type variables for
/// each and ensure that the constraints on the new type variables are adjusted to refer to these.
val FreshenAndFixupTypars : range -> TyparRigidity -> Typars -> TType list -> Typars -> Typars * TyparInst * TType list
val FreshenAndFixupTypars: range -> TyparRigidity -> Typars -> TType list -> Typars -> Typars * TyparInst * TType list

val FreshenTypeInst : range -> Typars -> Typars * TyparInst * TType list
val FreshenTypeInst: range -> Typars -> Typars * TyparInst * TType list

val FreshenTypars : range -> Typars -> TType list
val FreshenTypars: range -> Typars -> TType list

val FreshenMethInfo : range -> MethInfo -> TType list
val FreshenMethInfo: range -> MethInfo -> TType list

[<RequireQualifiedAccess>]
/// Information about the context of a type equation.
Expand Down Expand Up @@ -114,53 +114,70 @@ type TcValF = (ValRef -> ValUseFlag -> TType list -> range -> Expr * TType)
type ConstraintSolverState =
static member New: TcGlobals * Import.ImportMap * InfoReader * TcValF -> ConstraintSolverState

type ConstraintSolverEnv

val BakedInTraitConstraintNames : Set<string>

val MakeConstraintSolverEnv : ContextInfo -> ConstraintSolverState -> range -> DisplayEnv -> ConstraintSolverEnv
val BakedInTraitConstraintNames: Set<string>

[<Sealed; NoEquality; NoComparison>]
type Trace

type OptionalTrace =
| NoTrace
| WithTrace of Trace

val SimplifyMeasuresInTypeScheme : TcGlobals -> bool -> Typars -> TType -> TyparConstraint list -> Typars
val SolveTyparEqualsType : ConstraintSolverEnv -> int -> range -> OptionalTrace -> TType -> TType -> OperationResult<unit>
val SolveTypeEqualsTypeKeepAbbrevs : ConstraintSolverEnv -> int -> range -> OptionalTrace -> TType -> TType -> OperationResult<unit>

/// Canonicalize constraints prior to generalization
val CanonicalizeRelevantMemberConstraints : ConstraintSolverEnv -> int -> OptionalTrace -> Typars -> OperationResult<unit>

val ResolveOverloading : ConstraintSolverEnv -> OptionalTrace -> string -> ndeep: int -> TraitConstraintInfo option -> int * int -> AccessorDomain -> CalledMeth<Expr> list -> bool -> TType option -> CalledMeth<Expr> option * OperationResult<unit>
val UnifyUniqueOverloading : ConstraintSolverEnv -> int * int -> string -> AccessorDomain -> CalledMeth<SynExpr> list -> TType -> OperationResult<bool>
val EliminateConstraintsForGeneralizedTypars : ConstraintSolverEnv -> OptionalTrace -> Typars -> unit

val CheckDeclaredTypars : DisplayEnv -> ConstraintSolverState -> range -> Typars -> Typars -> unit

val AddConstraint : ConstraintSolverEnv -> int -> Range.range -> OptionalTrace -> Typar -> TyparConstraint -> OperationResult<unit>
val AddCxTypeEqualsType : ContextInfo -> DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> unit
val AddCxTypeEqualsTypeUndoIfFailed : DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool
val AddCxTypeEqualsTypeUndoIfFailedOrWarnings : DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool
val AddCxTypeEqualsTypeMatchingOnlyUndoIfFailed : DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool
val AddCxTypeMustSubsumeType : ContextInfo -> DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> TType -> unit
val AddCxTypeMustSubsumeTypeUndoIfFailed : DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool
val AddCxTypeMustSubsumeTypeMatchingOnlyUndoIfFailed : DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool
val AddCxMethodConstraint : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TraitConstraintInfo -> unit
val AddCxTypeMustSupportNull : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit
val AddCxTypeMustSupportComparison : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit
val AddCxTypeMustSupportEquality : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit
val AddCxTypeMustSupportDefaultCtor : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit
val AddCxTypeIsReferenceType : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit
val AddCxTypeIsValueType : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit
val AddCxTypeIsUnmanaged : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit
val AddCxTypeIsEnum : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> TType -> unit
val AddCxTypeIsDelegate : DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> TType -> TType -> unit

val CodegenWitnessThatTypeSupportsTraitConstraint : TcValF -> TcGlobals -> ImportMap -> range -> TraitConstraintInfo -> Expr list -> OperationResult<Expr option>

val ChooseTyparSolutionAndSolve : ConstraintSolverState -> DisplayEnv -> Typar -> unit

val IsApplicableMethApprox : TcGlobals -> ImportMap -> range -> MethInfo -> TType -> bool
| NoTrace
| WithTrace of Trace

val SimplifyMeasuresInTypeScheme: TcGlobals -> bool -> Typars -> TType -> TyparConstraint list -> Typars

val ResolveOverloadingForCall: DisplayEnv -> ConstraintSolverState -> range -> string -> ndeep: int -> TraitConstraintInfo option -> int * int -> AccessorDomain -> CalledMeth<Expr> list -> bool -> TType option -> CalledMeth<Expr> option * OperationResult<unit>

val UnifyUniqueOverloading: DisplayEnv -> ConstraintSolverState -> range -> int * int -> string -> AccessorDomain -> CalledMeth<SynExpr> list -> TType -> OperationResult<bool>

/// Remove the global constraints where these type variables appear in the support of the constraint
val EliminateConstraintsForGeneralizedTypars: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> Typars -> unit

val CheckDeclaredTypars: DisplayEnv -> ConstraintSolverState -> range -> Typars -> Typars -> unit

val AddCxTypeEqualsType: ContextInfo -> DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> unit

val AddCxTypeEqualsTypeUndoIfFailed: DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool

val AddCxTypeEqualsTypeUndoIfFailedOrWarnings: DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool

val AddCxTypeEqualsTypeMatchingOnlyUndoIfFailed: DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool

val AddCxTypeMustSubsumeType: ContextInfo -> DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> TType -> unit

val AddCxTypeMustSubsumeTypeUndoIfFailed: DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool

val AddCxTypeMustSubsumeTypeMatchingOnlyUndoIfFailed: DisplayEnv -> ConstraintSolverState -> range -> TType -> TType -> bool

val AddCxMethodConstraint: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TraitConstraintInfo -> unit

val AddCxTypeMustSupportNull: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit

val AddCxTypeMustSupportComparison: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit

val AddCxTypeMustSupportEquality: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit

val AddCxTypeMustSupportDefaultCtor: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit

val AddCxTypeIsReferenceType: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit

val AddCxTypeIsValueType: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit

val AddCxTypeIsUnmanaged: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> unit

val AddCxTypeIsEnum: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> TType -> unit

val AddCxTypeIsDelegate: DisplayEnv -> ConstraintSolverState -> range -> OptionalTrace -> TType -> TType -> TType -> unit

val AddCxTyparDefaultsTo: DisplayEnv -> ConstraintSolverState -> range -> ContextInfo -> Typar -> int -> TType -> unit

val SolveTypeAsError: DisplayEnv -> ConstraintSolverState -> range -> TType -> unit

val ApplyTyparDefaultAtPriority: DisplayEnv -> ConstraintSolverState -> priority: int -> Typar -> unit

val CodegenWitnessThatTypeSupportsTraitConstraint: TcValF -> TcGlobals -> ImportMap -> range -> TraitConstraintInfo -> Expr list -> OperationResult<Expr option>

val ChooseTyparSolutionAndSolve: ConstraintSolverState -> DisplayEnv -> Typar -> unit

val IsApplicableMethApprox: TcGlobals -> ImportMap -> range -> MethInfo -> TType -> bool

val CanonicalizePartialInferenceProblem: ConstraintSolverState -> DisplayEnv -> range -> Typars -> unit
58 changes: 15 additions & 43 deletions src/fsharp/TypeChecker.fs
Original file line number Diff line number Diff line change
Expand Up @@ -2284,13 +2284,6 @@ module GeneralizationHelpers =
ConstraintSolver.ChooseTyparSolutionAndSolve cenv.css denv tp)
generalizedTypars

let CanonicalizePartialInferenceProblem (cenv, denv, m) tps =
// Canonicalize constraints prior to generalization
let csenv = (MakeConstraintSolverEnv ContextInfo.NoContext cenv.css m denv)
TryD (fun () -> ConstraintSolver.CanonicalizeRelevantMemberConstraints csenv 0 NoTrace tps)
(fun res -> ErrorD (ErrorFromAddingConstraint(denv, res, m)))
|> RaiseOperationResult

let ComputeAndGeneralizeGenericTypars (cenv,
denv: DisplayEnv,
m,
Expand Down Expand Up @@ -2333,8 +2326,7 @@ module GeneralizationHelpers =
generalizedTypars |> List.iter (SetTyparRigid cenv.g denv m)

// Generalization removes constraints related to generalized type variables
let csenv = MakeConstraintSolverEnv ContextInfo.NoContext cenv.css m denv
EliminateConstraintsForGeneralizedTypars csenv NoTrace generalizedTypars
EliminateConstraintsForGeneralizedTypars denv cenv.css m NoTrace generalizedTypars

generalizedTypars

Expand Down Expand Up @@ -4333,8 +4325,7 @@ let rec TcTyparConstraint ridx cenv newOk checkCxs occ (env: TcEnv) tpenv c =
| WhereTyparDefaultsToType(tp, ty, m) ->
let ty', tpenv = TcTypeAndRecover cenv newOk checkCxs occ env tpenv ty
let tp', tpenv = TcTypar cenv env newOk tpenv tp
let csenv = MakeConstraintSolverEnv env.eContextInfo cenv.css m env.DisplayEnv
AddConstraint csenv 0 m NoTrace tp' (TyparConstraint.DefaultsTo(ridx, ty', m)) |> CommitOperationResult
AddCxTyparDefaultsTo env.DisplayEnv cenv.css m env.eContextInfo tp' ridx ty'
tpenv

| WhereTyparSubtypeOfType(tp, ty, m) ->
Expand Down Expand Up @@ -5595,11 +5586,7 @@ and TcPatterns warnOnUpper cenv env vFlags s argTys args =
assert (List.length args = List.length argTys)
List.mapFold (fun s (ty, pat) -> TcPat warnOnUpper cenv env None vFlags s ty pat) s (List.zip argTys args)


and solveTypAsError cenv denv m ty =
let ty2 = NewErrorType ()
assert((destTyparTy cenv.g ty2).IsFromError)
SolveTypeEqualsTypeKeepAbbrevs (MakeConstraintSolverEnv ContextInfo.NoContext cenv.css m denv) 0 m NoTrace ty ty2 |> ignore
and solveTypAsError cenv denv m ty = ConstraintSolver.SolveTypeAsError denv cenv.css m ty

and RecordNameAndTypeResolutions_IdeallyWithoutHavingOtherEffects cenv env tpenv expr =
// This function is motivated by cases like
Expand Down Expand Up @@ -6782,7 +6769,7 @@ and TcObjectExprBinding cenv (env: TcEnv) implty tpenv (absSlotInfo, bind) =
| _ ->
declaredTypars
// Canonicalize constraints prior to generalization
GeneralizationHelpers.CanonicalizePartialInferenceProblem (cenv, denv, m) declaredTypars
ConstraintSolver.CanonicalizePartialInferenceProblem cenv.css denv m declaredTypars

let freeInEnv = GeneralizationHelpers.ComputeUngeneralizableTypars env

Expand Down Expand Up @@ -9638,7 +9625,7 @@ and TcLookupThen cenv overallTy env tpenv mObjExpr objExpr objExprTy longId dela

// Canonicalize inference problem prior to '.' lookup on variable types
if isTyparTy cenv.g objExprTy then
GeneralizationHelpers.CanonicalizePartialInferenceProblem (cenv, env.DisplayEnv, mExprAndLongId) (freeInTypeLeftToRight cenv.g false objExprTy)
ConstraintSolver.CanonicalizePartialInferenceProblem cenv.css env.DisplayEnv mExprAndLongId (freeInTypeLeftToRight cenv.g false objExprTy)

let item, mItem, rest, afterResolution = ResolveExprDotLongIdentAndComputeRange cenv.tcSink cenv.nameResolver mExprAndLongId ad env.NameEnv objExprTy longId findFlag false
let mExprAndItem = unionRanges mObjExpr mItem
Expand Down Expand Up @@ -10089,8 +10076,7 @@ and TcMethodApplication
yield makeOneCalledMeth (minfo, pinfoOpt, false) ]

let uniquelyResolved =
let csenv = MakeConstraintSolverEnv ContextInfo.NoContext cenv.css mMethExpr denv
UnifyUniqueOverloading csenv callerArgCounts methodName ad preArgumentTypeCheckingCalledMethGroup returnTy
UnifyUniqueOverloading denv cenv.css mMethExpr callerArgCounts methodName ad preArgumentTypeCheckingCalledMethGroup returnTy

uniquelyResolved, preArgumentTypeCheckingCalledMethGroup

Expand Down Expand Up @@ -10182,17 +10168,15 @@ and TcMethodApplication
CalledMeth<Expr>(cenv.infoReader, Some(env.NameEnv), isCheckingAttributeCall, FreshenMethInfo, mMethExpr, ad, minfo, minst, callerTyArgs, pinfoOpt, callerObjArgTys, callerArgs, usesParamArrayConversion, true, objTyOpt))

let callerArgCounts = (unnamedCurriedCallerArgs.Length, namedCurriedCallerArgs.Length)
let csenv = MakeConstraintSolverEnv ContextInfo.NoContext cenv.css mMethExpr denv

// Commit unassociated constraints prior to member overload resolution where there is ambiguity
// about the possible target of the call.
if not uniquelyResolved then
GeneralizationHelpers.CanonicalizePartialInferenceProblem (cenv, denv, mItem)
ConstraintSolver.CanonicalizePartialInferenceProblem cenv.css denv mItem
(//freeInTypeLeftToRight cenv.g false returnTy @
(unnamedCurriedCallerArgs |> List.collectSquared (fun callerArg -> freeInTypeLeftToRight cenv.g false callerArg.Type)))

let result, errors =
ResolveOverloading csenv NoTrace methodName 0 None callerArgCounts ad postArgumentTypeCheckingCalledMethGroup true (Some returnTy)
let result, errors = ResolveOverloadingForCall denv cenv.css mMethExpr methodName 0 None callerArgCounts ad postArgumentTypeCheckingCalledMethGroup true (Some returnTy)

match afterResolution, result with
| AfterResolution.DoNothing, _ -> ()
Expand Down Expand Up @@ -11150,7 +11134,7 @@ and TcLetBinding cenv isUse env containerInfo declKind tpenv (synBinds, synBinds

// Canonicalize constraints prior to generalization
let denv = env.DisplayEnv
GeneralizationHelpers.CanonicalizePartialInferenceProblem (cenv, denv, synBindsRange)
ConstraintSolver.CanonicalizePartialInferenceProblem cenv.css denv synBindsRange
(checkedBinds |> List.collect (fun tbinfo ->
let (CheckedBindingInfo(_, _, _, _, flex, _, _, _, tauTy, _, _, _, _, _)) = tbinfo
let (ExplicitTyparInfo(_, declaredTypars, _)) = flex
Expand Down Expand Up @@ -12025,7 +12009,7 @@ and TcIncrementalLetRecGeneralization cenv scopem
else

let supportForBindings = newGeneralizableBindings |> List.collect (TcLetrecComputeSupportForBinding cenv)
GeneralizationHelpers.CanonicalizePartialInferenceProblem (cenv, denv, scopem) supportForBindings
ConstraintSolver.CanonicalizePartialInferenceProblem cenv.css denv scopem supportForBindings

let generalizedTyparsL = newGeneralizableBindings |> List.map (TcLetrecComputeAndGeneralizeGenericTyparsForBinding cenv denv freeInEnv)

Expand Down Expand Up @@ -17530,27 +17514,15 @@ let ApplyDefaults cenv g denvAtEnd m mexpr extraAttribs =
try
let unsolved = FSharp.Compiler.FindUnsolved.UnsolvedTyparsOfModuleDef g cenv.amap denvAtEnd (mexpr, extraAttribs)

GeneralizationHelpers.CanonicalizePartialInferenceProblem (cenv, denvAtEnd, m) unsolved
ConstraintSolver.CanonicalizePartialInferenceProblem cenv.css denvAtEnd m unsolved

let applyDefaults priority =
unsolved |> List.iter (fun tp ->
// The priority order comes from the order of declaration of the defaults in FSharp.Core.
for priority = 10 downto 0 do
unsolved |> List.iter (fun tp ->
if not tp.IsSolved then
// Apply the first default. If we're defaulting one type variable to another then
// the defaults will be propagated to the new type variable.
tp.Constraints |> List.iter (fun tpc ->
match tpc with
| TyparConstraint.DefaultsTo(priority2, ty2, m) when priority2 = priority ->
let ty1 = mkTyparTy tp
if not tp.IsSolved && not (typeEquiv cenv.g ty1 ty2) then
let csenv = MakeConstraintSolverEnv ContextInfo.NoContext cenv.css m denvAtEnd
TryD (fun () -> ConstraintSolver.SolveTyparEqualsType csenv 0 m NoTrace ty1 ty2)
(fun e -> solveTypAsError cenv denvAtEnd m ty1
ErrorD(ErrorFromApplyingDefault(g, denvAtEnd, tp, ty2, e, m)))
|> RaiseOperationResult
| _ -> ()))

for priority = 10 downto 0 do
applyDefaults priority
ConstraintSolver.ApplyTyparDefaultAtPriority denvAtEnd cenv.css priority tp)

// OK, now apply defaults for any unsolved HeadTypeStaticReq
unsolved |> List.iter (fun tp ->
Expand Down
12 changes: 12 additions & 0 deletions tests/fsharp/tests.fs
Original file line number Diff line number Diff line change
Expand Up @@ -2660,6 +2660,18 @@ module TypecheckTests =
[<Test>]
let ``type check neg115`` () = singleNegTest (testConfig "typecheck/sigs") "neg115"

[<Test>]
let ``type check neg116`` () = singleNegTest (testConfig "typecheck/sigs") "neg116"

[<Test>]
let ``type check neg117`` () = singleNegTest (testConfig "typecheck/sigs") "neg117"

[<Test>]
let ``type check neg118`` () = singleNegTest (testConfig "typecheck/sigs") "neg118"

[<Test>]
let ``type check neg119`` () = singleNegTest (testConfig "typecheck/sigs") "neg119"

[<Test>]
let ``type check neg_anon_1`` () = singleNegTest (testConfig "typecheck/sigs") "neg_anon_1"

Expand Down
Loading