open Internal.Utilities

open Internal.Utilities.Collections

open Microsoft.FSharp.Compiler.AbstractIL

open Microsoft.FSharp.Compiler.AbstractIL.Internal

open Microsoft.FSharp.Compiler.AbstractIL.Internal.Library

open Microsoft.FSharp.Compiler

open Microsoft.FSharp.Compiler.AbstractIL.Diagnostics

open Microsoft.FSharp.Compiler.Range

open Microsoft.FSharp.Compiler.Ast

open Microsoft.FSharp.Compiler.ErrorLogger

open Microsoft.FSharp.Compiler.Tast

open Microsoft.FSharp.Compiler.Tastops

open Microsoft.FSharp.Compiler.Tastops.DebugPrint

open Microsoft.FSharp.Compiler.Env

open Microsoft.FSharp.Compiler.Lib

open Microsoft.FSharp.Compiler.Infos

open Microsoft.FSharp.Compiler.Infos.AccessibilityLogic

open Microsoft.FSharp.Compiler.Infos.AttributeChecking

open Microsoft.FSharp.Compiler.Typrelns

open Microsoft.FSharp.Compiler.PrettyNaming

let compgen_id = mkSynId range0 unassignedTyparName

let NewCompGenTypar (kind,rigid,staticReq,dynamicReq,error) =

NewTypar(kind,rigid,Typar(compgen_id,staticReq,true),error,dynamicReq,[],false,false)

let anon_id m = mkSynId m unassignedTyparName

let NewAnonTypar (kind,m,rigid,var,dyn) =

NewTypar (kind,rigid,Typar(anon_id m,var,true),false,dyn,[],false,false)

let NewNamedInferenceMeasureVar (_m,rigid,var,id) =

NewTypar(TyparKind.Measure,rigid,Typar(id,var,false),false,TyparDynamicReq.No,[],false,false)

let NewInferenceMeasurePar () = NewCompGenTypar (TyparKind.Measure,TyparRigidity.Flexible,NoStaticReq,TyparDynamicReq.No,false)

let NewErrorTypar () = NewCompGenTypar (TyparKind.Type,TyparRigidity.Flexible,NoStaticReq,TyparDynamicReq.No,true)

let NewErrorMeasureVar () = NewCompGenTypar (TyparKind.Measure,TyparRigidity.Flexible,NoStaticReq,TyparDynamicReq.No,true)

let NewInferenceType () = mkTyparTy (NewTypar (TyparKind.Type,TyparRigidity.Flexible,Typar(compgen_id,NoStaticReq,true),false,TyparDynamicReq.No,[],false,false))

let NewErrorType () = mkTyparTy (NewErrorTypar ())

let NewErrorMeasure () = MeasureVar (NewErrorMeasureVar ())

let NewInferenceTypes l = l |> List.map (fun _ -> NewInferenceType ())

let FreshenAndFixupTypars 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 tps = tpsorig |> List.map copy_tyvar

let renaming,tinst = FixupNewTypars m fctps tinst tpsorig tps

tps,renaming,tinst

let FreshenTypeInst m tpsorig = FreshenAndFixupTypars m TyparRigidity.Flexible [] [] tpsorig

let FreshMethInst m fctps tinst tpsorig = FreshenAndFixupTypars m TyparRigidity.Flexible fctps tinst tpsorig

let FreshenTypars m tpsorig =

match tpsorig with

| [] -> []

| _ ->

let _,_,tptys = FreshenTypeInst m tpsorig

tptys

let FreshenMethInfo m (minfo:MethInfo) =

let _,_,tptys = FreshMethInst m (minfo.GetFormalTyparsOfDeclaringType m) minfo.DeclaringTypeInst minfo.FormalMethodTypars

tptys

exception ConstraintSolverTupleDiffLengths of DisplayEnv * TType list * TType list * range * range

exception ConstraintSolverInfiniteTypes of DisplayEnv * TType * TType * range * range

exception ConstraintSolverTypesNotInEqualityRelation of DisplayEnv * TType * TType * range * range

exception ConstraintSolverTypesNotInSubsumptionRelation of DisplayEnv * TType * TType * range * range

exception ConstraintSolverMissingConstraint of DisplayEnv * Tast.Typar * Tast.TyparConstraint * range * range

exception ConstraintSolverError of string * range * range

exception ConstraintSolverRelatedInformation of string option * range * exn

exception ErrorFromApplyingDefault of Env.TcGlobals * DisplayEnv * Tast.Typar * TType * exn * range

exception ErrorFromAddingTypeEquation of Env.TcGlobals * DisplayEnv * TType * TType * exn * range

exception ErrorsFromAddingSubsumptionConstraint of Env.TcGlobals * DisplayEnv * TType * TType * exn * range

exception ErrorFromAddingConstraint of DisplayEnv * exn * range

exception PossibleOverload of DisplayEnv * string * exn * range

exception UnresolvedOverloading of DisplayEnv * exn list * string * range

exception UnresolvedConversionOperator of DisplayEnv * TType * TType * range

let GetPossibleOverloads amap m denv (calledMethGroup: (CalledMeth<_> * exn) list) =

calledMethGroup |> List.map (fun (cmeth, e) -> PossibleOverload(denv,NicePrint.stringOfMethInfo amap m denv cmeth.Method, e, m))

type TcValF = (ValRef -> ValUseFlag -> TType list -> range -> Expr * TType)

type ConstraintSolverState =

{

g: Env.TcGlobals;

amap: Import.ImportMap;

InfoReader : InfoReader;

TcVal : TcValF

/// 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

/// each time a solution to an index variable is found.

mutable ExtraCxs: HashMultiMap<Stamp, (TraitConstraintInfo * range)>;

}

static member New(g,amap,infoReader, tcVal) =

{ g=g; amap=amap;

ExtraCxs= HashMultiMap(10, HashIdentity.Structural)

InfoReader=infoReader

TcVal = tcVal } ;

type ConstraintSolverEnv =

{

SolverState: ConstraintSolverState;

MatchingOnly : bool

m: range;

EquivEnv: TypeEquivEnv;

DisplayEnv : DisplayEnv

}

member csenv.InfoReader = csenv.SolverState.InfoReader

member csenv.g = csenv.SolverState.g

member csenv.amap = csenv.SolverState.amap

let MakeConstraintSolverEnv css m denv =

{ SolverState=css;

m=m;

// Indicates that when unifiying ty1 = ty2, only type variables in ty1 may be solved

MatchingOnly=false;

EquivEnv=TypeEquivEnv.Empty;

DisplayEnv = denv }

let rec occursCheck g un ty =

match stripTyEqns g ty with

| TType_ucase(_,l)

| TType_app (_,l)

| TType_tuple l -> List.exists (occursCheck g un) l

| TType_fun (d,r) -> occursCheck g un d || occursCheck g un r

| TType_var r -> typarEq un r

| TType_forall (_,tau) -> occursCheck g un tau

| _ -> false

let rec isNativeIntegerTy g ty =

typeEquivAux EraseMeasures g g.nativeint_ty ty ||

typeEquivAux EraseMeasures g g.unativeint_ty ty ||

(isEnumTy g ty && isNativeIntegerTy g (underlyingTypeOfEnumTy g ty))

let isSignedIntegerTy g ty =

typeEquivAux EraseMeasures g g.sbyte_ty ty ||

typeEquivAux EraseMeasures g g.int16_ty ty ||

typeEquivAux EraseMeasures g g.int32_ty ty ||

typeEquivAux EraseMeasures g g.nativeint_ty ty ||

typeEquivAux EraseMeasures g g.int64_ty ty

let isUnsignedIntegerTy g ty =

typeEquivAux EraseMeasures g g.byte_ty ty ||

typeEquivAux EraseMeasures g g.uint16_ty ty ||

typeEquivAux EraseMeasures g g.uint32_ty ty ||

typeEquivAux EraseMeasures g g.unativeint_ty ty ||

typeEquivAux EraseMeasures g g.uint64_ty ty

let rec isIntegerOrIntegerEnumTy g ty =

isSignedIntegerTy g ty ||

isUnsignedIntegerTy g ty ||

(isEnumTy g ty && isIntegerOrIntegerEnumTy g (underlyingTypeOfEnumTy g ty))

let rec isIntegerTy g ty =

isSignedIntegerTy g ty ||

isUnsignedIntegerTy g ty

let isStringTy g ty = typeEquiv g g.string_ty ty

let isCharTy g ty = typeEquiv g g.char_ty ty

let isFpTy g ty =

typeEquivAux EraseMeasures g g.float_ty ty ||

typeEquivAux EraseMeasures g g.float32_ty ty

let isDecimalTy g ty =

typeEquivAux EraseMeasures g g.decimal_ty ty

let IsNonDecimalNumericOrIntegralEnumType g ty = isIntegerOrIntegerEnumTy g ty || isFpTy g ty

let IsNumericOrIntegralEnumType g ty = IsNonDecimalNumericOrIntegralEnumType g ty || isDecimalTy g ty

let IsNonDecimalNumericType g ty = isIntegerTy g ty || isFpTy g ty

let IsNumericType g ty = IsNonDecimalNumericType g ty || isDecimalTy g ty

let GetMeasureOfType g ty =

match ty with

| AppTy g (tcref,[tyarg]) ->

match stripTyEqns g tyarg with

| TType_measure ms ->

if measureEquiv g ms MeasureOne then None else Some (tcref,ms)

| _ -> None

| _ -> None

type TraitConstraintSolution =

| TTraitUnsolved

| TTraitBuiltIn

| TTraitSolved of MethInfo * TypeInst

| TTraitSolvedRecdProp of RecdFieldInfo * bool

let BakedInTraitConstraintNames =

[ "op_Division" ; "op_Multiply"; "op_Addition"

"op_Subtraction"; "op_Modulus";

"get_Zero"; "get_One";

"DivideByInt";"get_Item"; "set_Item";

"op_BitwiseAnd"; "op_BitwiseOr"; "op_ExclusiveOr"; "op_LeftShift";

"op_RightShift"; "op_UnaryPlus"; "op_UnaryNegation"; "get_Sign"; "op_LogicalNot"

"op_OnesComplement"; "Abs"; "Sqrt"; "Sin"; "Cos"; "Tan";

"Sinh"; "Cosh"; "Tanh"; "Atan"; "Acos"; "Asin"; "Exp"; "Ceiling"; "Floor"; "Round"; "Log10"; "Log"; "Sqrt";

"Truncate"; "op_Explicit";

"Pow"; "Atan2" ]

type Trace =

| Trace of (unit -> unit) list ref

static member New () = Trace (ref [])

member t.Undo () = let (Trace trace) = t in List.iter (fun a -> a ()) !trace

type OptionalTrace =

| NoTrace

| WithTrace of Trace

member x.HasTrace = match x with NoTrace -> false | WithTrace _ -> true

let CollectThenUndo f =

let trace = Trace.New()

let res = f trace

trace.Undo();

res

let CheckThenUndo f = CollectThenUndo f |> CheckNoErrorsAndGetWarnings

let FilterEachThenUndo f meths =

meths |> List.choose (fun calledMeth ->

match CheckThenUndo (fun trace -> f trace calledMeth) with

| None -> None

| Some warns -> Some (calledMeth,warns.Length))

let ShowAccessDomain ad =

match ad with

| AccessibleFromEverywhere -> "public"

| AccessibleFrom(_,_) -> "accessible"

| AccessibleFromSomeFSharpCode -> "public, protected or internal"

| AccessibleFromSomewhere -> ""

exception NonRigidTypar of DisplayEnv * string option * range * TType * TType * range

exception LocallyAbortOperationThatLosesAbbrevs

let localAbortD = ErrorD LocallyAbortOperationThatLosesAbbrevs

let PreferUnifyTypar (v1:Typar) (v2:Typar) =

match v1.Rigidity,v2.Rigidity with

// Rigid > all

| TyparRigidity.Rigid,_ -> false

// Prefer to unify away WillBeRigid in favour of Rigid

| TyparRigidity.WillBeRigid,TyparRigidity.Rigid -> true

| TyparRigidity.WillBeRigid,TyparRigidity.WillBeRigid -> true

| TyparRigidity.WillBeRigid,TyparRigidity.WarnIfNotRigid -> false

| TyparRigidity.WillBeRigid,TyparRigidity.Anon -> false

| TyparRigidity.WillBeRigid,TyparRigidity.Flexible -> false

// Prefer to unify away WarnIfNotRigid in favour of Rigid

| TyparRigidity.WarnIfNotRigid,TyparRigidity.Rigid -> true

| TyparRigidity.WarnIfNotRigid,TyparRigidity.WillBeRigid -> true

| TyparRigidity.WarnIfNotRigid,TyparRigidity.WarnIfNotRigid -> true

| TyparRigidity.WarnIfNotRigid,TyparRigidity.Anon -> false

| TyparRigidity.WarnIfNotRigid,TyparRigidity.Flexible -> false

// Prefer to unify away anonymous variables in favour of Rigid, WarnIfNotRigid

| TyparRigidity.Anon,TyparRigidity.Rigid -> true

| TyparRigidity.Anon,TyparRigidity.WillBeRigid -> true

| TyparRigidity.Anon,TyparRigidity.WarnIfNotRigid -> true

| TyparRigidity.Anon,TyparRigidity.Anon -> true

| TyparRigidity.Anon,TyparRigidity.Flexible -> false

// Prefer to unify away Flexible in favour of Rigid, WarnIfNotRigid or Anon

| TyparRigidity.Flexible,TyparRigidity.Rigid -> true

| TyparRigidity.Flexible,TyparRigidity.WillBeRigid -> true

| TyparRigidity.Flexible,TyparRigidity.WarnIfNotRigid -> true

| TyparRigidity.Flexible,TyparRigidity.Anon -> true

| TyparRigidity.Flexible,TyparRigidity.Flexible ->

// Prefer to unify away compiler generated type vars

match v1.IsCompilerGenerated, v2.IsCompilerGenerated with

| true,false -> true

| false,true -> false

| _ ->

// Prefer to unify away non-error vars - gives better error recovery since we keep

// error vars lying around, and can avoid giving errors about illegal polymorphism

// if they occur

match v1.IsFromError, v2.IsFromError with

| true,false -> false

| _ -> true

let FindMinimumMeasureExponent vs =

let rec findmin vs =

match vs with

| [] -> vs

| (v:Typar,e)::vs ->

match findmin vs with

| [] -> [(v,e)]

| (v',e')::vs' ->

if abs e < abs e' || (abs e = abs e' && PreferUnifyTypar v v')

then (v, e) :: vs

else (v',e') :: (v,e) :: vs'

findmin vs

let SubstMeasure (r:Typar) ms =

if r.Rigidity = TyparRigidity.Rigid then error(InternalError("SubstMeasure: rigid",r.Range));

if r.Kind = TyparKind.Type then error(InternalError("SubstMeasure: kind=type",r.Range));

let tp = r.Data

match tp.typar_solution with

| None -> tp.typar_solution <- Some (TType_measure ms)

| Some _ -> error(InternalError("already solved",r.Range));

let rec TransactStaticReq (csenv:ConstraintSolverEnv) trace (tpr:Typar) req =

let m = csenv.m

if (tpr.Rigidity.ErrorIfUnified && tpr.StaticReq <> req) then

ErrorD(ConstraintSolverError(FSComp.SR.csTypeCannotBeResolvedAtCompileTime(tpr.Name),m,m))

else

let orig = tpr.StaticReq

match trace with

| NoTrace -> ()

| WithTrace (Trace actions) -> actions := (fun () -> tpr.SetStaticReq orig) :: !actions

tpr.SetStaticReq req;

CompleteD

and SolveTypStaticReqTypar (csenv:ConstraintSolverEnv) trace req (tpr:Typar) =

let orig = tpr.StaticReq

let req2 = JoinTyparStaticReq req orig

if orig <> req2 then TransactStaticReq csenv trace tpr req2 else CompleteD

and SolveTypStaticReq (csenv:ConstraintSolverEnv) trace req ty =

match req with

| NoStaticReq -> CompleteD

| HeadTypeStaticReq ->

// requires that a type constructor be known at compile time

match stripTyparEqns ty with

| TType_measure ms ->

let vs = ListMeasureVarOccsWithNonZeroExponents ms

IterateD (fun ((tpr:Typar),_) -> SolveTypStaticReqTypar csenv trace req tpr) vs

| _ ->

if (isAnyParTy csenv.g ty) then

let tpr = destAnyParTy csenv.g ty

SolveTypStaticReqTypar csenv trace req tpr

else CompleteD

let rec TransactDynamicReq trace (tpr:Typar) req =

let orig = tpr.DynamicReq

match trace with

| NoTrace -> ()

| WithTrace (Trace actions) -> actions := (fun () -> tpr.SetDynamicReq orig) :: !actions

tpr.SetDynamicReq req;

CompleteD

and SolveTypDynamicReq (csenv:ConstraintSolverEnv) trace req ty =

match req with

| TyparDynamicReq.No -> CompleteD

| TyparDynamicReq.Yes ->

if (isAnyParTy csenv.g ty) then

let tpr = destAnyParTy csenv.g ty

if tpr.DynamicReq <> TyparDynamicReq.Yes then TransactDynamicReq trace tpr TyparDynamicReq.Yes else CompleteD

else CompleteD

let SubstMeasureWarnIfRigid (csenv:ConstraintSolverEnv) trace (v:Typar) ms =

if v.Rigidity.WarnIfUnified && not (isAnyParTy csenv.g (TType_measure ms)) then

// NOTE: we grab the name eagerly to make sure the type variable prints as a type variable

let tpnmOpt = if v.IsCompilerGenerated then None else Some v.Name

SolveTypStaticReq csenv trace v.StaticReq (TType_measure ms) ++ (fun () ->

SubstMeasure v ms;

WarnD(NonRigidTypar(csenv.DisplayEnv,tpnmOpt,v.Range,TType_measure (MeasureVar v), TType_measure ms,csenv.m)))

else

// Propagate static requirements from 'tp' to 'ty'

SolveTypStaticReq csenv trace v.StaticReq (TType_measure ms) ++ (fun () ->

SubstMeasure v ms;

if v.Rigidity = TyparRigidity.Anon && measureEquiv csenv.g ms MeasureOne then

WarnD(Error(FSComp.SR.csCodeLessGeneric(),v.Range))

else CompleteD)

let DivRoundDown x y =

let signx=if x<0 then -1 else 1

let signy=if y<0 then -1 else 1

if signx=signy then x / y

else (x-y+signy) / y

let rec UnifyMeasureWithOne (csenv:ConstraintSolverEnv) trace ms =

let (rigidVars,nonRigidVars) = (ListMeasureVarOccsWithNonZeroExponents ms) |> List.partition (fun (v,_) -> v.Rigidity = TyparRigidity.Rigid)

let expandedCons = ListMeasureConOccsWithNonZeroExponents csenv.g true ms

let unexpandedCons = ListMeasureConOccsWithNonZeroExponents csenv.g false ms

match FindMinimumMeasureExponent nonRigidVars, rigidVars, expandedCons, unexpandedCons with

| [], [], [], _ -> CompleteD

| [], _, _, _ -> localAbortD

| (v,e)::vs, rigidVars, _, _ ->

// don't break up abbreviations if we can help it!

if unexpandedCons |> List.forall (fun (_,e') -> e' % e = 0) && (vs@rigidVars) |> List.forall (fun (_,e') -> e' % e = 0)

then

let newms = ProdMeasures (List.map (fun (c,e') -> MeasurePower (MeasureCon c) (- (DivRoundDown e' e))) unexpandedCons

@ List.map (fun (v,e') -> MeasurePower (MeasureVar v) (- (DivRoundDown e' e))) (vs @ rigidVars))

SubstMeasureWarnIfRigid csenv trace v newms

else

let newms = ProdMeasures (List.map (fun (c,e') -> MeasurePower (MeasureCon c) (- (DivRoundDown e' e))) expandedCons

@ List.map (fun (v,e') -> MeasurePower (MeasureVar v) (- (DivRoundDown e' e))) (vs @ rigidVars))

if expandedCons |> List.forall (fun (_,e') -> e' % e = 0) && (vs@rigidVars) |> List.forall (fun (_,e') -> e' % e = 0)

then SubstMeasureWarnIfRigid csenv trace v newms

elif isNil vs

then localAbortD

else

// New variable v' must inherit WarnIfNotRigid from v

let v' = NewAnonTypar (TyparKind.Measure,v.Range,v.Rigidity,v.StaticReq,v.DynamicReq)

SubstMeasure v (MeasureProd(MeasureVar v', newms));

UnifyMeasureWithOne csenv trace ms

let UnifyMeasures (csenv:ConstraintSolverEnv) trace ms1 ms2 =

UnifyMeasureWithOne csenv trace (MeasureProd(ms1,MeasureInv ms2))

let SimplifyMeasure g vars ms =

let rec simp vars =

match FindMinimumMeasureExponent (List.filter (fun (_,e) -> e<>0) (List.map (fun v -> (v, MeasureVarExponent v ms)) vars)) with

| [] ->

(vars, None)

| (v,e)::vs ->

if e < 0 then

let v' = NewAnonTypar (TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)

let vars' = v' :: ListSet.remove typarEq v vars

SubstMeasure v (MeasureInv (MeasureVar v'));

simp vars'

else

let newv = if v.IsCompilerGenerated then NewAnonTypar (TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)

else NewNamedInferenceMeasureVar (v.Range,TyparRigidity.Flexible,v.StaticReq,v.Id)

let remainingvars = ListSet.remove typarEq v vars

let newms = (ProdMeasures (List.map (fun (c,e') -> MeasurePower (MeasureCon c) (- (DivRoundDown e' e))) (ListMeasureConOccsWithNonZeroExponents g false ms)

@ List.map (fun (v',e') -> if typarEq v v' then MeasureVar newv else MeasurePower (MeasureVar v') (- (DivRoundDown e' e))) (ListMeasureVarOccsWithNonZeroExponents ms)));

SubstMeasure v newms;

match vs with

| [] -> (remainingvars, Some newv)

| _ -> simp (newv::remainingvars)

simp vars

let rec SimplifyMeasuresInType g resultFirst ((generalizable, generalized) as param) ty =

match stripTyparEqns ty with

| TType_ucase(_,l)

| TType_app (_,l)

| TType_tuple l -> SimplifyMeasuresInTypes g param l

| TType_fun (d,r) -> if resultFirst then SimplifyMeasuresInTypes g param [r;d] else SimplifyMeasuresInTypes g param [d;r]

| TType_var _ -> param

| TType_forall (_,tau) -> SimplifyMeasuresInType g resultFirst param tau

| TType_measure unt ->

let (generalizable', newlygeneralized) = SimplifyMeasure g generalizable unt

match newlygeneralized with

| None -> (generalizable', generalized)

| Some v -> (generalizable', v::generalized)

and SimplifyMeasuresInTypes g param tys =

match tys with

| [] -> param

| ty::tys ->

let param' = SimplifyMeasuresInType g false param ty

SimplifyMeasuresInTypes g param' tys

let SimplifyMeasuresInConstraint g param c =

match c with

| TyparConstraint.DefaultsTo (_,ty,_) | TyparConstraint.CoercesTo(ty,_) -> SimplifyMeasuresInType g false param ty

| TyparConstraint.SimpleChoice (tys,_) -> SimplifyMeasuresInTypes g param tys

| TyparConstraint.IsDelegate (ty1,ty2,_) -> SimplifyMeasuresInTypes g param [ty1;ty2]

| _ -> param

let rec SimplifyMeasuresInConstraints g param cs =

match cs with

| [] -> param

| c::cs ->

let param' = SimplifyMeasuresInConstraint g param c

SimplifyMeasuresInConstraints g param' cs

let SimplifyMeasuresInTypeScheme g resultFirst (generalizable:Typar list) ty constraints =

// Only bother if we're generalizing over at least one unit-of-measure variable

let uvars, vars =

generalizable |> List.partition (fun v -> v.Kind = TyparKind.Measure && v.Rigidity <> TyparRigidity.Rigid)

match uvars with

| [] -> generalizable

| _::_ ->

let (untouched, generalized) = SimplifyMeasuresInType g resultFirst (SimplifyMeasuresInConstraints g (uvars, []) constraints) ty

vars @ List.rev generalized @ untouched

let freshMeasure () = MeasureVar (NewInferenceMeasurePar ())

let CheckWarnIfRigid (csenv:ConstraintSolverEnv) ty1 (r:Typar) ty =

let g = csenv.g

let denv = csenv.DisplayEnv

if r.Rigidity.WarnIfUnified &&

(not (isAnyParTy g ty) ||

(let tp2 = destAnyParTy g ty

not tp2.IsCompilerGenerated &&

(r.IsCompilerGenerated ||

// exclude this warning for two identically named user-specified type parameters, e.g. from different mutually recursive functions or types

r.DisplayName <> tp2.DisplayName ))) then

// NOTE: we grab the name eagerly to make sure the type variable prints as a type variable

let tpnmOpt = if r.IsCompilerGenerated then None else Some r.Name

WarnD(NonRigidTypar(denv,tpnmOpt,r.Range,ty1,ty,csenv.m ))

else

CompleteD

let rec SolveTyparEqualsTyp (csenv:ConstraintSolverEnv) ndeep m2 trace ty1 ty =

let m = csenv.m

let denv = csenv.DisplayEnv

DepthCheck ndeep m ++ (fun () ->

match ty1 with

| TType_var r | TType_measure (MeasureVar r) ->

// The types may still be equivalent due to abbreviations, which we are trying not to eliminate

if typeEquiv csenv.g ty1 ty then CompleteD else

// The famous 'occursCheck' check to catch things like 'a = list<'a>

if occursCheck csenv.g r ty then ErrorD (ConstraintSolverInfiniteTypes(denv,ty1,ty,m,m2)) else

// Note: warn _and_ continue!

CheckWarnIfRigid csenv ty1 r ty ++ (fun () ->

// Record the solution before we solve the constraints, since

// We may need to make use of the equation when solving the constraints.

// Record a entry in the undo trace if one is provided

let tpdata = r.Data

match trace with

| NoTrace -> ()

| WithTrace (Trace actions) -> actions := (fun () -> tpdata.typar_solution <- None) :: !actions

tpdata.typar_solution <- Some ty;

(* dprintf "setting typar %d to type %s at %a\n" r.Stamp ((DebugPrint.showType ty)) outputRange m; *)

// Only solve constraints if this is not an error var

if r.IsFromError then CompleteD else

// Check to see if this type variable is relevant to any trait constraints.

// If so, re-solve the relevant constraints.

(if csenv.SolverState.ExtraCxs.ContainsKey r.Stamp then

RepeatWhileD ndeep (fun ndeep -> SolveRelevantMemberConstraintsForTypar csenv ndeep false trace r)

else

CompleteD) ++ (fun _ ->

// Re-solve the other constraints associated with this type variable

solveTypMeetsTyparConstraints csenv ndeep m2 trace ty (r.DynamicReq,r.StaticReq,r.Constraints)))

| _ -> failwith "SolveTyparEqualsTyp")

and solveTypMeetsTyparConstraints (csenv:ConstraintSolverEnv) ndeep m2 trace ty (dreq,sreq,cs) =

let g = csenv.g

// Propagate dynamic requirements from 'tp' to 'ty'

SolveTypDynamicReq csenv trace dreq ty ++ (fun () ->

// Propagate static requirements from 'tp' to 'ty'

SolveTypStaticReq csenv trace sreq ty ++ (fun () ->

// Solve constraints on 'tp' w.r.t. 'ty'

cs |> IterateD (function

| TyparConstraint.DefaultsTo (priority,dty,m) ->

if not (isTyparTy g ty) || typeEquiv g ty dty then CompleteD else

AddConstraint csenv ndeep m2 trace (destTyparTy g ty) (TyparConstraint.DefaultsTo(priority,dty,m))

| TyparConstraint.SupportsNull m2 -> SolveTypSupportsNull csenv ndeep m2 trace ty

| TyparConstraint.IsEnum(underlying, m2) -> SolveTypIsEnum csenv ndeep m2 trace ty underlying

| TyparConstraint.SupportsComparison(m2) -> SolveTypeSupportsComparison csenv ndeep m2 trace ty

| TyparConstraint.SupportsEquality(m2) -> SolveTypSupportsEquality csenv ndeep m2 trace ty

| TyparConstraint.IsDelegate(aty,bty, m2) -> SolveTypIsDelegate csenv ndeep m2 trace ty aty bty

| TyparConstraint.IsNonNullableStruct m2 -> SolveTypIsNonNullableValueType csenv ndeep m2 trace ty

| TyparConstraint.IsUnmanaged m2 -> SolveTypIsUnmanaged csenv ndeep m2 trace ty

| TyparConstraint.IsReferenceType m2 -> SolveTypIsReferenceType csenv ndeep m2 trace ty

| TyparConstraint.RequiresDefaultConstructor m2 -> SolveTypRequiresDefaultConstructor csenv ndeep m2 trace ty

| TyparConstraint.SimpleChoice(tys,m2) -> SolveTypChoice csenv ndeep m2 trace ty tys

| TyparConstraint.CoercesTo(ty2,m2) -> SolveTypSubsumesTypKeepAbbrevs csenv ndeep m2 trace ty2 ty

| TyparConstraint.MayResolveMember(traitInfo,m2) ->

SolveMemberConstraint csenv false ndeep m2 trace traitInfo ++ (fun _ -> CompleteD)

)))

and SolveTypEqualsTyp (csenv:ConstraintSolverEnv) ndeep m2 (trace: OptionalTrace) ty1 ty2 =

let ndeep = ndeep + 1

let aenv = csenv.EquivEnv

let g = csenv.g

if ty1 === ty2 then CompleteD else

let canShortcut = not trace.HasTrace

let sty1 = stripTyEqnsA csenv.g canShortcut ty1

let sty2 = stripTyEqnsA csenv.g canShortcut ty2

match sty1, sty2 with

// type vars inside forall-types may be alpha-equivalent

| TType_var tp1, TType_var tp2 when typarEq tp1 tp2 || (aenv.EquivTypars.ContainsKey tp1 && typeEquiv g aenv.EquivTypars.[tp1] ty2) -> CompleteD

| TType_var tp1, TType_var tp2 when PreferUnifyTypar tp1 tp2 -> SolveTyparEqualsTyp csenv ndeep m2 trace sty1 ty2

| TType_var tp1, TType_var tp2 when PreferUnifyTypar tp2 tp1 && not csenv.MatchingOnly -> SolveTyparEqualsTyp csenv ndeep m2 trace sty2 ty1

| TType_var r, _ when (r.Rigidity <> TyparRigidity.Rigid) -> SolveTyparEqualsTyp csenv ndeep m2 trace sty1 ty2

| _, TType_var r when (r.Rigidity <> TyparRigidity.Rigid) && not csenv.MatchingOnly -> SolveTyparEqualsTyp csenv ndeep m2 trace sty2 ty1

// Catch float<_>=float<1>, float32<_>=float32<1> and decimal<_>=decimal<1>

| (_, TType_app (tc2,[ms])) when (tc2.IsMeasureableReprTycon && typeEquiv csenv.g sty1 (reduceTyconRefMeasureableOrProvided csenv.g tc2 [ms]))

-> SolveTypEqualsTyp csenv ndeep m2 trace ms (TType_measure MeasureOne)

| (TType_app (tc2,[ms]), _) when (tc2.IsMeasureableReprTycon && typeEquiv csenv.g sty2 (reduceTyconRefMeasureableOrProvided csenv.g tc2 [ms]))

-> SolveTypEqualsTyp csenv ndeep m2 trace ms (TType_measure MeasureOne)

| TType_app (tc1,l1) ,TType_app (tc2,l2) when tyconRefEq g tc1 tc2 -> SolveTypEqualsTypEqns csenv ndeep m2 trace l1 l2

| TType_app (_,_) ,TType_app (_,_) -> localAbortD

| TType_tuple l1 ,TType_tuple l2 -> SolveTypEqualsTypEqns csenv ndeep m2 trace l1 l2

| TType_fun (d1,r1) ,TType_fun (d2,r2) -> SolveFunTypEqn csenv ndeep m2 trace d1 d2 r1 r2

| TType_measure ms1 ,TType_measure ms2 -> UnifyMeasures csenv trace ms1 ms2

| TType_forall(tps1,rty1), TType_forall(tps2,rty2) ->

if tps1.Length <> tps2.Length then localAbortD else

let aenv = aenv.BindEquivTypars tps1 tps2

let csenv = {csenv with EquivEnv = aenv }

if not (typarsAEquiv g aenv tps1 tps2) then localAbortD else

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace rty1 rty2

| TType_ucase (uc1,l1) ,TType_ucase (uc2,l2) when g.unionCaseRefEq uc1 uc2 -> SolveTypEqualsTypEqns csenv ndeep m2 trace l1 l2

| _ -> localAbortD

and SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace ty1 ty2 =

let denv = csenv.DisplayEnv

// Back out of expansions of type abbreviations to give improved error messages.

// Note: any "normalization" of equations on type variables must respect the trace parameter

TryD (fun () -> SolveTypEqualsTyp csenv ndeep m2 trace ty1 ty2)

(function LocallyAbortOperationThatLosesAbbrevs -> ErrorD(ConstraintSolverTypesNotInEqualityRelation(denv,ty1,ty2,csenv.m,m2))

| err -> ErrorD err)

and SolveTypEqualsTypEqns csenv ndeep m2 trace origl1 origl2 =

match origl1,origl2 with

| [],[] -> CompleteD

| _ ->

// We unwind Iterate2D by hand here for performance reasons.

let rec loop l1 l2 =

match l1,l2 with

| [],[] -> CompleteD

| h1::t1, h2::t2 ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace h1 h2 ++ (fun () -> loop t1 t2)

| _ ->

ErrorD(ConstraintSolverTupleDiffLengths(csenv.DisplayEnv,origl1,origl2,csenv.m,m2))

loop origl1 origl2

and SolveFunTypEqn csenv ndeep m2 trace d1 d2 r1 r2 =

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace d1 d2 ++ (fun () ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace r1 r2)

and SolveTypSubsumesTyp (csenv:ConstraintSolverEnv) ndeep m2 (trace: OptionalTrace) ty1 ty2 =

// 'a :> obj ---> <solved>

let ndeep = ndeep + 1

let g = csenv.g

let amap = csenv.amap

let aenv = csenv.EquivEnv

let denv = csenv.DisplayEnv

let m = csenv.m

if isObjTy g ty1 then CompleteD else

let canShortcut = not trace.HasTrace

let sty1 = stripTyEqnsA csenv.g canShortcut ty1

let sty2 = stripTyEqnsA csenv.g canShortcut ty2

match sty1, sty2 with

| TType_var tp1, _ when aenv.EquivTypars.ContainsKey tp1 ->

SolveTypSubsumesTyp csenv ndeep m2 trace aenv.EquivTypars.[tp1] ty2

| TType_var r1, TType_var r2 when typarEq r1 r2 -> CompleteD

| _, TType_var r when not csenv.MatchingOnly -> SolveTyparSubtypeOfType csenv ndeep m2 trace r ty1

| TType_var _ , _ -> SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace ty1 ty2

| TType_tuple l1 ,TType_tuple l2 -> SolveTypEqualsTypEqns csenv ndeep m2 trace l1 l2 (* nb. can unify since no variance *)

| TType_fun (d1,r1) ,TType_fun (d2,r2) -> SolveFunTypEqn csenv ndeep m2 trace d1 d2 r1 r2 (* nb. can unify since no variance *)

| TType_measure ms1, TType_measure ms2 -> UnifyMeasures csenv trace ms1 ms2

// Enforce the identities float=float<1>, float32=float32<1> and decimal=decimal<1>

| (_, TType_app (tc2,[ms])) when (tc2.IsMeasureableReprTycon && typeEquiv csenv.g sty1 (reduceTyconRefMeasureableOrProvided csenv.g tc2 [ms]))

-> SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace ms (TType_measure MeasureOne)

| (TType_app (tc2,[ms]), _) when (tc2.IsMeasureableReprTycon && typeEquiv csenv.g sty2 (reduceTyconRefMeasureableOrProvided csenv.g tc2 [ms]))

-> SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace ms (TType_measure MeasureOne)

| TType_app (tc1,l1) ,TType_app (tc2,l2) when tyconRefEq g tc1 tc2 ->

SolveTypEqualsTypEqns csenv ndeep m2 trace l1 l2

| TType_ucase (uc1,l1) ,TType_ucase (uc2,l2) when g.unionCaseRefEq uc1 uc2 ->

SolveTypEqualsTypEqns csenv ndeep m2 trace l1 l2

| _ ->

// By now we know the type is not a variable type

// C :> obj ---> <solved>

if isObjTy g ty1 then CompleteD else

// 'a[] :> IList<'b> ---> 'a = 'b

// 'a[] :> ICollection<'b> ---> 'a = 'b

// 'a[] :> IEnumerable<'b> ---> 'a = 'b

// 'a[] :> IReadOnlyList<'b> ---> 'a = 'b

// 'a[] :> IReadOnlyCollection<'b> ---> 'a = 'b

// Note we don't support co-variance on array types nor

// the special .NET conversions for these types

if

(isArray1DTy g ty2 &&

isAppTy g ty1 &&

(let tcr1 = tcrefOfAppTy g ty1

tyconRefEq g tcr1 g.tcref_System_Collections_Generic_IList ||

tyconRefEq g tcr1 g.tcref_System_Collections_Generic_ICollection ||

tyconRefEq g tcr1 g.tcref_System_Collections_Generic_IReadOnlyList ||

tyconRefEq g tcr1 g.tcref_System_Collections_Generic_IReadOnlyCollection ||

tyconRefEq g tcr1 g.tcref_System_Collections_Generic_IEnumerable)) then

let _,tinst = destAppTy g ty1

match tinst with

| [ty1arg] ->

let ty2arg = destArrayTy g ty2

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace ty1arg ty2arg

| _ -> error(InternalError("destArrayTy",m));

// D<inst> :> Head<_> --> C<inst'> :> Head<_> for the

// first interface or super-class C supported by D which

// may feasibly convert to Head.

else

match (FindUniqueFeasibleSupertype g amap m ty1 ty2) with

| None -> ErrorD(ConstraintSolverTypesNotInSubsumptionRelation(denv,ty1,ty2,m,m2))

| Some t -> SolveTypSubsumesTyp csenv ndeep m2 trace ty1 t

and SolveTypSubsumesTypKeepAbbrevs csenv ndeep m2 trace ty1 ty2 =

let denv = csenv.DisplayEnv

TryD (fun () -> SolveTypSubsumesTyp csenv ndeep m2 trace ty1 ty2)

(function LocallyAbortOperationThatLosesAbbrevs -> ErrorD(ConstraintSolverTypesNotInSubsumptionRelation(denv,ty1,ty2,csenv.m,m2))

| err -> ErrorD err)

and SolveTyparSubtypeOfType (csenv:ConstraintSolverEnv) ndeep m2 trace tp ty1 =

let g = csenv.g

let m = csenv.m

if isObjTy g ty1 then CompleteD

elif typeEquiv g ty1 (mkTyparTy tp) then CompleteD

elif isSealedTy g ty1 then

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace (mkTyparTy tp) ty1

else

AddConstraint csenv ndeep m2 trace tp (TyparConstraint.CoercesTo(ty1,m))

and DepthCheck ndeep m =

if ndeep > 300 then error(Error(FSComp.SR.csTypeInferenceMaxDepth(),m)) else CompleteD

and SolveDimensionlessNumericType (csenv:ConstraintSolverEnv) ndeep m2 trace ty =

match GetMeasureOfType csenv.g ty with

| Some (tcref, _) ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace ty (mkAppTy tcref [TType_measure MeasureOne])

| None ->

CompleteD

and SolveMemberConstraint (csenv:ConstraintSolverEnv) permitWeakResolution ndeep m2 trace (TTrait(tys,nm,memFlags,argtys,rty,sln)) : OperationResult<bool> =

// Do not re-solve if already solved

if sln.Value.IsSome then ResultD true else

let g = csenv.g

let m = csenv.m

let amap = csenv.amap

let aenv = csenv.EquivEnv

let denv = csenv.DisplayEnv

let ndeep = ndeep + 1

DepthCheck ndeep m ++ (fun () ->

// Remove duplicates from the set of types in the support

let tys = ListSet.setify (typeAEquiv g aenv) tys

// Rebuild the trait info after removing duplicates

let traitInfo = TTrait(tys,nm,memFlags,argtys,rty,sln)

let rty = GetFSharpViewOfReturnType g rty

// Assert the object type if the constraint is for an instance member

begin

if memFlags.IsInstance then

match tys, argtys with

| [ty], (h :: _) -> SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace h ty

| _ -> ErrorD (ConstraintSolverError(FSComp.SR.csExpectedArguments(), m,m2))

else CompleteD

end ++ (fun () ->

// Trait calls are only supported on pseudo type (variables)

tys |> IterateD (SolveTypStaticReq csenv trace HeadTypeStaticReq)) ++ (fun () ->

let argtys = if memFlags.IsInstance then List.tail argtys else argtys

let minfos = GetRelevantMethodsForTrait csenv permitWeakResolution nm traitInfo

match minfos,tys,memFlags.IsInstance,nm,argtys with

| _,_,false,("op_Division" | "op_Multiply"),[argty1;argty2]

when

// This simulates the existence of

// float * float -> float

// float32 * float32 -> float32

// float<'u> * float<'v> -> float<'u 'v>

// float32<'u> * float32<'v> -> float32<'u 'v>

// decimal<'u> * decimal<'v> -> decimal<'u 'v>

// decimal<'u> * decimal -> decimal<'u>

// float32<'u> * float32<'v> -> float32<'u 'v>

// int * int -> int

// int64 * int64 -> int64

//

// The rule is triggered by these sorts of inputs when permitWeakResolution=false

// float * float

// float * float32 // will give error

// decimal<m> * decimal<m>

// decimal<m> * decimal <-- Note this one triggers even though "decimal" has some possibly-relevant methods

// float * Matrix // the rule doesn't trigger for this one since Matrix has overloads we can use and we prefer those instead

// float * Matrix // the rule doesn't trigger for this one since Matrix has overloads we can use and we prefer those instead

//

// The rule is triggered by these sorts of inputs when permitWeakResolution=true

// float * 'a

// 'a * float

// decimal<'u> * 'a <---

(let checkRuleAppliesInPreferenceToMethods argty1 argty2 =

// Check that at least one of the argument types is numeric

(IsNumericOrIntegralEnumType g argty1) &&

// Check that the support of type variables is empty. That is,

// if we're canonicalizing, then having one of the types nominal is sufficient.

// If not, then both must be nominal (i.e. not a type variable).

(permitWeakResolution || not (isTyparTy g argty2)) &&

// This next condition checks that either

// - Neither type contributes any methods OR

// - We have the special case "decimal<_> * decimal". In this case we have some

// possibly-relevant methods from "decimal" but we ignore them in this case.

(isNil minfos || (isSome (GetMeasureOfType g argty1) && isDecimalTy g argty2)) in

checkRuleAppliesInPreferenceToMethods argty1 argty2 ||

checkRuleAppliesInPreferenceToMethods argty2 argty1) ->

match GetMeasureOfType g argty1 with

| Some (tcref,ms1) ->

let ms2 = freshMeasure ()

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace argty2 (mkAppTy tcref [TType_measure ms2]) ++ (fun () ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace rty (mkAppTy tcref [TType_measure (MeasureProd(ms1,if nm = "op_Multiply" then ms2 else MeasureInv ms2))]) ++ (fun () ->

ResultD TTraitBuiltIn))

| _ ->

match GetMeasureOfType g argty2 with

| Some (tcref,ms2) ->

let ms1 = freshMeasure ()

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace argty1 (mkAppTy tcref [TType_measure ms1]) ++ (fun () ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace rty (mkAppTy tcref [TType_measure (MeasureProd(ms1, if nm = "op_Multiply" then ms2 else MeasureInv ms2))]) ++ (fun () ->

ResultD TTraitBuiltIn))

| _ ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace argty2 argty1 ++ (fun () ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace rty argty1 ++ (fun () ->

ResultD TTraitBuiltIn))

| _,_,false,("op_Addition" | "op_Subtraction" | "op_Modulus"),[argty1;argty2]

when // Ignore any explicit +/- overloads from any basic integral types

(minfos |> List.forall (fun minfo -> isIntegerTy g minfo.EnclosingType ) &&

( (IsNumericOrIntegralEnumType g argty1 || (nm = "op_Addition" && (isCharTy g argty1 || isStringTy g argty1))) && (permitWeakResolution || not (isTyparTy g argty2))

|| (IsNumericOrIntegralEnumType g argty2 || (nm = "op_Addition" && (isCharTy g argty2 || isStringTy g argty2))) && (permitWeakResolution || not (isTyparTy g argty1)))) ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace argty2 argty1 ++ (fun () ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace rty argty1 ++ (fun () ->

ResultD TTraitBuiltIn))

// We pretend for uniformity that the numeric types have a static property called Zero and One

// As with constants, only zero is polymorphic in its units

| [],[ty],false,"get_Zero",[]

when IsNumericType g ty ->

SolveTypEqualsTypKeepAbbrevs csenv ndeep m2 trace rty ty ++ (fun () ->

ResultD TTraitBuiltIn)

| [],[ty],false,"get_One",[]