PostInferenceChecks.fs

// Copyright (c) Microsoft Corporation.  All Rights Reserved.  See License.txt in the project root for license information.

/// Implements a set of checks on the TAST for a file that can only be performed after type inference
/// is complete.
module internal FSharp.Compiler.PostTypeCheckSemanticChecks

open System
open System.Collections.Generic

open Internal.Utilities.Collections
open Internal.Utilities.Library
open Internal.Utilities.Library.Extras
open FSharp.Compiler
open FSharp.Compiler.AbstractIL.IL
open FSharp.Compiler.AccessibilityLogic
open FSharp.Compiler.DiagnosticsLogger
open FSharp.Compiler.Features
open FSharp.Compiler.Infos
open FSharp.Compiler.InfoReader
open FSharp.Compiler.Syntax
open FSharp.Compiler.Syntax.PrettyNaming
open FSharp.Compiler.TcGlobals
open FSharp.Compiler.Text
open FSharp.Compiler.Text.Range
open FSharp.Compiler.TypedTree
open FSharp.Compiler.TypedTreeBasics
open FSharp.Compiler.TypedTreeOps
open FSharp.Compiler.TypeHierarchy
open FSharp.Compiler.TypeRelations
open Import

//--------------------------------------------------------------------------
// NOTES: reraise safety checks
//--------------------------------------------------------------------------

// "rethrow may only occur with-in the body of a catch handler".
//   -- Section 4.23. Part III. CLI Instruction Set. ECMA Draft 2002.
//
//   1. reraise() calls are converted to TOp.Reraise in the type checker.
//   2. any remaining reraise val_refs will be first class uses. These are trapped.
//   3. The freevars track free TOp.Reraise (they are bound (cleared) at try-catch handlers).
//   4. An outermost expression is not contained in a try-catch handler.
//      These may not have unbound rethrows.
//      Outermost expressions occur at:
//      * module bindings.
//      * attribute arguments.
//      * Any more? What about fields of a static class?
//   5. A lambda body (from lambda-expression or method binding) will not occur under a try-catch handler.
//      These may not have unbound rethrows.
//   6. All other constructs are assumed to generate IL code sequences.
//      For correctness, this claim needs to be justified.
//
//   Informal justification:
//   If a reraise occurs, then it is minimally contained by either:
//     a) a try-catch - accepted.
//     b) a lambda expression - rejected.
//     c) none of the above - rejected as when checking outmost expressions.

//--------------------------------------------------------------------------
// check environment
//--------------------------------------------------------------------------

[<RequireQualifiedAccess>]
type Resumable =
      | None
      /// Indicates we are expecting resumable code (the body of a ResumableCode delegate or
      /// the body of the MoveNextMethod for a state machine)
      ///   -- allowed: are we inside the 'then' branch of an 'if __useResumableCode then ...'
      ///      for a ResumableCode delegate.
      | ResumableExpr of allowed: bool

type env =
    {
      /// The bound type parameter names in scope
      boundTyparNames: string list

      /// The bound type parameters in scope
      boundTypars: TyparMap<unit>

      /// The set of arguments to this method/function
      argVals: ValMap<unit>

      /// "module remap info", i.e. hiding information down the signature chain, used to compute what's hidden by a signature
      sigToImplRemapInfo: (Remap * SignatureHidingInfo) list

      /// Are we in a quotation?
      quote : bool

      /// Are we under [<ReflectedDefinition>]?
      reflect : bool

      /// Are we in an extern declaration?
      external : bool

      /// Current return scope of the expr.
      returnScope : int

      /// Are we in an app expression (Expr.App)?
      isInAppExpr: bool

      /// Are we expecting a  resumable code block etc
      resumableCode: Resumable
    }

    override _.ToString() = "<env>"

let BindTypar env (tp: Typar) =
    { env with
         boundTyparNames = tp.Name :: env.boundTyparNames
         boundTypars = env.boundTypars.Add (tp, ()) }

let BindTypars g env (tps: Typar list) =
    let tps = NormalizeDeclaredTyparsForEquiRecursiveInference g tps
    if isNil tps then env else
    // Here we mutate to provide better names for generalized type parameters
    let nms = PrettyTypes.PrettyTyparNames (fun _ -> true) env.boundTyparNames tps
    PrettyTypes.AssignPrettyTyparNames tps nms
    List.fold BindTypar env tps

/// Set the set of vals which are arguments in the active lambda. We are allowed to return
/// byref arguments as byref returns.
let BindArgVals env (vs: Val list) =
    { env with argVals = ValMap.OfList (List.map (fun v -> (v, ())) vs) }

[<AutoOpen>]
module Limit =

    [<Flags>]
    type LimitFlags =
        | None                          = 0b00000
        | ByRef                         = 0b00001
        | ByRefOfSpanLike               = 0b00011
        | ByRefOfStackReferringSpanLike = 0b00101
        | SpanLike                      = 0b01000
        | StackReferringSpanLike        = 0b10000

    [<Struct>]
    type Limit =
        {
            scope: int
            flags: LimitFlags
        }

        member this.IsLocal = this.scope >= 1

    /// Check if the limit has the target limit.
    let inline HasLimitFlag targetLimit (limit: Limit) =
        limit.flags &&& targetLimit = targetLimit

    let NoLimit = { scope = 0; flags = LimitFlags.None }

    let CombineTwoLimits limit1 limit2 =
        let isByRef1 = HasLimitFlag LimitFlags.ByRef limit1
        let isByRef2 = HasLimitFlag LimitFlags.ByRef limit2
        let isStackSpan1 = HasLimitFlag LimitFlags.StackReferringSpanLike limit1
        let isStackSpan2 = HasLimitFlag LimitFlags.StackReferringSpanLike limit2
        let isLimited1 = isByRef1 || isStackSpan1
        let isLimited2 = isByRef2 || isStackSpan2

        // A limit that has a stack referring span-like but not a by-ref,
        //   we force the scope to 1. This is to handle call sites
        //   that return a by-ref and have stack referring span-likes as arguments.
        //   This is to ensure we can only prevent out of scope at the method level rather than visibility.
        let limit1 =
            if isStackSpan1 && not isByRef1 then
                { limit1 with scope = 1 }
            else
                limit1

        let limit2 =
            if isStackSpan2 && not isByRef2 then
                { limit2 with scope = 1 }
            else
                limit2

        match isLimited1, isLimited2 with
        | false, false ->
            { scope = 0; flags = limit1.flags ||| limit2.flags }
        | true, true ->
            { scope = Math.Max(limit1.scope, limit2.scope); flags = limit1.flags ||| limit2.flags }
        | true, false ->
            { limit1 with flags = limit1.flags ||| limit2.flags }
        | false, true ->
            { limit2 with flags = limit1.flags ||| limit2.flags }

    let CombineLimits limits =
        (NoLimit, limits)
        ||> List.fold CombineTwoLimits

type cenv =
    { boundVals: Dictionary<Stamp, int> // really a hash set

      limitVals: Dictionary<Stamp, Limit>

      mutable potentialUnboundUsesOfVals: StampMap<range>

      mutable anonRecdTypes: StampMap<AnonRecdTypeInfo>

      stackGuard: StackGuard

      g: TcGlobals

      amap: ImportMap

      /// For reading metadata
      infoReader: InfoReader

      internalsVisibleToPaths : CompilationPath list

      denv: DisplayEnv

      viewCcu : CcuThunk

      reportErrors: bool

      isLastCompiland : bool*bool

      isInternalTestSpanStackReferring: bool

      // outputs
      mutable usesQuotations: bool

      mutable entryPointGiven: bool

      /// Callback required for quotation generation
      tcVal: ConstraintSolver.TcValF }

    override x.ToString() = "<cenv>"

/// Check if the value is an argument of a function
let IsValArgument env (v: Val) =
    env.argVals.ContainsVal v

/// Check if the value is a local, not an argument of a function.
let IsValLocal env (v: Val) =
    v.ValReprInfo.IsNone && not (IsValArgument env v)

/// Get the limit of the val.
let GetLimitVal cenv env m (v: Val) =
    let limit =
        match cenv.limitVals.TryGetValue v.Stamp with
        | true, limit -> limit
        | _ ->
            if IsValLocal env v then
                { scope = 1; flags = LimitFlags.None }
            else
                NoLimit

    if isSpanLikeTy cenv.g m v.Type then
        // The value is a limited Span or might have become one through mutation
        let isMutable = v.IsMutable && cenv.isInternalTestSpanStackReferring
        let isLimited = HasLimitFlag LimitFlags.StackReferringSpanLike limit

        if isMutable || isLimited then
            { limit with flags = LimitFlags.StackReferringSpanLike }
        else
            { limit with flags = LimitFlags.SpanLike }

    elif isByrefTy cenv.g v.Type then
        let isByRefOfSpanLike = isSpanLikeTy cenv.g m (destByrefTy cenv.g v.Type)

        if isByRefOfSpanLike then
            if HasLimitFlag LimitFlags.ByRefOfStackReferringSpanLike limit then
                { limit with flags = LimitFlags.ByRefOfStackReferringSpanLike }
            else
                { limit with flags = LimitFlags.ByRefOfSpanLike }
        else
            { limit with flags = LimitFlags.ByRef }

    else
        { limit with flags = LimitFlags.None }

/// Get the limit of the val by reference.
let GetLimitValByRef cenv env m v =
    let limit = GetLimitVal cenv env m v

    let scope =
        // Getting the address of an argument will always be a scope of 1.
        if IsValArgument env v then 1
        else limit.scope

    let flags =
        if HasLimitFlag LimitFlags.StackReferringSpanLike limit then
            LimitFlags.ByRefOfStackReferringSpanLike
        elif HasLimitFlag LimitFlags.SpanLike limit then
            LimitFlags.ByRefOfSpanLike
        else
            LimitFlags.ByRef

    { scope = scope; flags = flags }

let LimitVal cenv (v: Val) limit =
    if not v.IgnoresByrefScope then
        cenv.limitVals[v.Stamp] <- limit

let BindVal cenv env (v: Val) =
    let alreadyDone = cenv.boundVals.ContainsKey v.Stamp
    cenv.boundVals[v.Stamp] <- 1

    let topLevelBindingHiddenBySignatureFile () =
        let parentHasSignatureFile () =
            match v.TryDeclaringEntity with
            | ParentNone -> false
            | Parent p ->
                match p.TryDeref with
                | ValueNone -> false
                | ValueSome e -> e.HasSignatureFile

        v.IsModuleBinding && not v.HasSignatureFile && parentHasSignatureFile ()

    if not env.external &&
       not alreadyDone &&
       cenv.reportErrors &&
       not v.HasBeenReferenced &&
       (not v.IsCompiledAsTopLevel || topLevelBindingHiddenBySignatureFile ()) &&
       not (v.DisplayName.StartsWithOrdinal("_")) &&
       not v.IsCompilerGenerated &&
       // Don't warn for variables with synthetic ranges - these are compiler-generated
       // rebinding patterns in query/CE translation. See https://github.com/dotnet/fsharp/issues/422
       not v.Range.IsSynthetic then

        if v.IsCtorThisVal then
            warning (Error(FSComp.SR.chkUnusedThisVariable v.DisplayName, v.Range))
        else
            warning (Error(FSComp.SR.chkUnusedValue v.DisplayName, v.Range))

let BindVals cenv env vs = List.iter (BindVal cenv env) vs

let RecordAnonRecdInfo cenv (anonInfo: AnonRecdTypeInfo) =
    if not (cenv.anonRecdTypes.ContainsKey anonInfo.Stamp) then
         cenv.anonRecdTypes <- cenv.anonRecdTypes.Add(anonInfo.Stamp, anonInfo)

//--------------------------------------------------------------------------
// approx walk of type
//--------------------------------------------------------------------------

/// Represents the container for nester type instantions, carrying information about the parent (generic type) and data about corresponding generic typar definition.
/// For current use, IlGenericParameterDef was enough. For other future use cases, conversion into F# Typar might be needed.
type TypeInstCtx =
    | NoInfo
    | IlGenericInst of parent:TyconRef * genericArg:ILGenericParameterDef
    | TyparInst of parent:TyconRef
    | TopLevelAllowingByRef

    with member x.TyparAllowsRefStruct() =
                        match x with
                        | IlGenericInst(_,ilTypar) -> ilTypar.HasAllowsRefStruct
                        | _ -> false

let rec CheckTypeDeep (cenv: cenv) (visitTy, visitTyconRefOpt, visitAppTyOpt, visitTraitSolutionOpt, visitTyparOpt as f) (g: TcGlobals) env (typeInstParentOpt:TypeInstCtx) ty =
    // We iterate the _solved_ constraints as well, to pick up any record of trait constraint solutions
    // This means we walk _all_ the constraints _everywhere_ in a type, including
    // those attached to _solved_ type variables. This is used by PostTypeCheckSemanticChecks to detect uses of
    // values as solutions to trait constraints and determine if inference has caused the value to escape its scope.
    // The only record of these solutions is in the _solved_ constraints of types.
    // In an ideal world we would, instead, record the solutions to these constraints as "witness variables" in expressions,
    // rather than solely in types.
    match ty with
    | TType_var (tp, _) when tp.Solution.IsSome ->
        for cx in tp.Constraints do
            match cx with
            | TyparConstraint.MayResolveMember(TTrait(solution=soln), _) ->
                 match visitTraitSolutionOpt, soln.Value with
                 | Some visitTraitSolution, Some sln -> visitTraitSolution sln
                 | _ -> ()
            | _ -> ()
    | _ -> ()

    let ty =
        if g.compilingFSharpCore then
            match stripTyparEqns ty with
            // When compiling FSharp.Core, do not strip type equations at this point if we can't dereference a tycon.
            | TType_app (tcref, _, _) when not tcref.CanDeref -> ty
            | _ -> stripTyEqns g ty
        else
            stripTyEqns g ty
    visitTy ty

    match ty with
    | TType_forall (tps, body) ->
        let env = BindTypars g env tps
        CheckTypeDeep cenv f g env typeInstParentOpt body
        tps |> List.iter (fun tp -> tp.Constraints |> List.iter (CheckTypeConstraintDeep cenv f g env))

    | TType_measure _ -> ()

    | TType_app (tcref, tinst, _) ->
        match visitTyconRefOpt with
        | Some visitTyconRef -> visitTyconRef typeInstParentOpt tcref
        | None -> ()

        // If it's a 'byref<'T>', don't check 'T as an inner. This allows byref<Span<'T>>.
        // 'byref<byref<'T>>' is invalid and gets checked in visitAppTy.
        //if isByrefTyconRef g tcref then
        //    CheckTypesDeepNoInner cenv f g env tinst

        if tcref.CanDeref && tcref.IsILTycon && tinst.Length = tcref.ILTyconRawMetadata.GenericParams.Length then
            (tinst,tcref.ILTyconRawMetadata.GenericParams)
            ||> List.iter2 (fun ty ilGenericParam ->
                let typeInstParent = IlGenericInst(tcref, ilGenericParam)
                CheckTypeDeep cenv f g env typeInstParent ty)
        else
            let parentRef = TyparInst(tcref)
            for ty in tinst do
                CheckTypeDeep cenv f g env parentRef ty

        match visitAppTyOpt with
        | Some visitAppTy -> visitAppTy (tcref, tinst)
        | None -> ()

    | TType_anon (anonInfo, tys) ->
        RecordAnonRecdInfo cenv anonInfo
        CheckTypesDeep cenv f g env tys

    | TType_ucase (_, tinst) ->
        CheckTypesDeep cenv f g env tinst

    | TType_tuple (_, tys) ->
        CheckTypesDeep cenv f g env tys

    | TType_fun (s, t, _) ->
        CheckTypeDeep cenv f g env NoInfo s
        CheckTypeDeep cenv f g env NoInfo t

    | TType_var (tp, _) ->
          if not tp.IsSolved then
              match visitTyparOpt with
              | None -> ()
              | Some visitTyar ->
                    visitTyar (env, tp)

and CheckTypesDeep cenv f g env tys =
    for ty in tys do
        CheckTypeDeep cenv f g env NoInfo ty

and CheckTypeConstraintDeep cenv f g env x =
     match x with
     | TyparConstraint.CoercesTo(ty, _) -> CheckTypeDeep cenv f g env NoInfo ty
     | TyparConstraint.MayResolveMember(traitInfo, _) -> CheckTraitInfoDeep cenv f g env traitInfo
     | TyparConstraint.DefaultsTo(_, ty, _) -> CheckTypeDeep cenv f g env NoInfo ty
     | TyparConstraint.SimpleChoice(tys, _) -> CheckTypesDeep cenv f g env tys
     | TyparConstraint.IsEnum(underlyingTy, _) -> CheckTypeDeep cenv f g env NoInfo underlyingTy
     | TyparConstraint.IsDelegate(argTys, retTy, _) -> CheckTypeDeep cenv f g env NoInfo argTys; CheckTypeDeep cenv f g env NoInfo retTy
     | TyparConstraint.SupportsComparison _
     | TyparConstraint.SupportsEquality _
     | TyparConstraint.SupportsNull _
     | TyparConstraint.NotSupportsNull _
     | TyparConstraint.IsNonNullableStruct _
     | TyparConstraint.IsUnmanaged _
     | TyparConstraint.AllowsRefStruct _
     | TyparConstraint.IsReferenceType _
     | TyparConstraint.RequiresDefaultConstructor _ -> ()

and CheckTraitInfoDeep cenv (_, _, _, visitTraitSolutionOpt, _ as f) g env traitInfo =
    CheckTypesDeep cenv f g env traitInfo.SupportTypes
    CheckTypesDeep cenv f g env traitInfo.CompiledObjectAndArgumentTypes
    Option.iter (CheckTypeDeep cenv f g env NoInfo ) traitInfo.CompiledReturnType
    match visitTraitSolutionOpt, traitInfo.Solution with
    | Some visitTraitSolution, Some sln -> visitTraitSolution sln
    | _ -> ()

/// Check for byref-like types
let CheckForByrefLikeType cenv env m ty check =
    CheckTypeDeep cenv (ignore, Some (fun ctx tcref -> if (isByrefLikeTyconRef cenv.g m tcref && not(ctx.TyparAllowsRefStruct())) then check()),  None, None, None) cenv.g env NoInfo ty

/// Check for byref types
let CheckForByrefType cenv env ty check =
    CheckTypeDeep cenv (ignore, Some (fun _ctx tcref -> if isByrefTyconRef cenv.g tcref then check()),  None, None, None) cenv.g env NoInfo ty

/// check captures under lambdas
///
/// This is the definition of what can/can't be free in a lambda expression. This is checked at lambdas OR TBind(v, e) nodes OR TObjExprMethod nodes.
/// For TBind(v, e) nodes we may know an 'arity' which gives as a larger set of legitimate syntactic arguments for a lambda.
/// For TObjExprMethod(v, e) nodes we always know the legitimate syntactic arguments.
let CheckEscapes cenv allowProtected m syntacticArgs body = (* m is a range suited to error reporting *)
    if cenv.reportErrors then
        let cantBeFree (v: Val) =
           // If v is a syntactic argument, then it can be free since it was passed in.
           // The following cannot be free:
           //   a) BaseVal can never escape.
           //   b) Byref typed values can never escape.
           // Note that: Local mutables can be free, as they will be boxed later.

           // These checks must correspond to the tests governing the error messages below.
           (v.IsBaseVal || isByrefLikeTy cenv.g m v.Type) &&
           not (ListSet.contains valEq v syntacticArgs)

        let frees = freeInExpr (CollectLocalsWithStackGuard()) body
        let fvs   = frees.FreeLocals

        if not allowProtected && frees.UsesMethodLocalConstructs  then
            errorR(Error(FSComp.SR.chkProtectedOrBaseCalled(), m))
        elif Zset.exists cantBeFree fvs then
            let v =  List.find cantBeFree (Zset.elements fvs)

            // byref error before mutable error (byrefs are mutable...).
            if (isByrefLikeTy cenv.g m v.Type) then
                // Inner functions are not guaranteed to compile to method with a predictable arity (number of arguments).
                // As such, partial applications involving byref arguments could lead to closures containing byrefs.
                // For safety, such functions are assumed to have no known arity, and so cannot accept byrefs.
                errorR(Error(FSComp.SR.chkByrefUsedInInvalidWay(v.DisplayName), m))

            elif v.IsBaseVal then
                errorR(Error(FSComp.SR.chkBaseUsedInInvalidWay(), m))

            else
                // Should be dead code, unless governing tests change
                errorR(InternalError(FSComp.SR.chkVariableUsedInInvalidWay(v.DisplayName), m))
        Some frees
    else
        None


/// Check type access
let AccessInternalsVisibleToAsInternal thisCompPath internalsVisibleToPaths access =
    // Each internalsVisibleToPath is a compPath for the internals of some assembly.
    // Replace those by the compPath for the internals of this assembly.
    // This makes those internals visible here, but still internal. Bug://3737
    (access, internalsVisibleToPaths) ||> List.fold (fun access internalsVisibleToPath ->
        accessSubstPaths (thisCompPath, internalsVisibleToPath) access)


let CheckTypeForAccess (cenv: cenv) env objName valAcc m ty =
    if cenv.reportErrors then

        let visitType ty =
            // We deliberately only check the fully stripped type for accessibility,
            // because references to private type abbreviations are permitted
            match tryTcrefOfAppTy cenv.g ty with
            | ValueNone -> ()
            | ValueSome tcref ->
                let thisCompPath = compPathOfCcu cenv.viewCcu
                let tyconAcc = tcref.Accessibility |> AccessInternalsVisibleToAsInternal thisCompPath cenv.internalsVisibleToPaths
                if isLessAccessible tyconAcc valAcc then
                    errorR(Error(FSComp.SR.chkTypeLessAccessibleThanType(tcref.DisplayName, objName()), m))

        CheckTypeDeep cenv (visitType, None, None, None, None) cenv.g env NoInfo ty

let WarnOnWrongTypeForAccess (cenv: cenv) env objName valAcc m ty =
    if cenv.reportErrors then

        let visitType ty =
            // We deliberately only check the fully stripped type for accessibility,
            // because references to private type abbreviations are permitted
            match tryTcrefOfAppTy cenv.g ty with
            | ValueNone -> ()
            | ValueSome tcref ->
                let thisCompPath = compPathOfCcu cenv.viewCcu
                let tyconAcc = tcref.Accessibility |> AccessInternalsVisibleToAsInternal thisCompPath cenv.internalsVisibleToPaths
                if isLessAccessible tyconAcc valAcc then
                    let errorText = FSComp.SR.chkTypeLessAccessibleThanType(tcref.DisplayName, objName()) |> snd
                    let warningText = errorText + Environment.NewLine + FSComp.SR.tcTypeAbbreviationsCheckedAtCompileTime()
                    warning(ObsoleteDiagnostic(false, None, Some warningText, None, m))

        CheckTypeDeep cenv (visitType, None, None, None, None) cenv.g env NoInfo ty

/// Indicates whether a byref or byref-like type is permitted at a particular location
[<RequireQualifiedAccess>]
type PermitByRefType =
    /// Don't permit any byref or byref-like types
    | None

    /// Don't permit any byref or byref-like types on inner types.
    | NoInnerByRefLike

    /// Permit only a Span or IsByRefLike type
    | SpanLike

    /// Permit all byref and byref-like types
    | All


/// Indicates whether an address-of operation is permitted at a particular location
[<RequireQualifiedAccess>]
type PermitByRefExpr =
    /// Permit a tuple of arguments where elements can be byrefs
    | YesTupleOfArgs of int

    /// Context allows for byref typed expr.
    | Yes

    /// Context allows for byref typed expr, but the byref must be returnable
    | YesReturnable

    /// Context allows for byref typed expr, but the byref must be returnable and a non-local
    | YesReturnableNonLocal

    /// General (address-of expr and byref values not allowed)
    | No

    member ctxt.Disallow =
        match ctxt with
        | PermitByRefExpr.Yes
        | PermitByRefExpr.YesReturnable
        | PermitByRefExpr.YesReturnableNonLocal -> false
        | _ -> true

    member ctxt.PermitOnlyReturnable =
        match ctxt with
        | PermitByRefExpr.YesReturnable
        | PermitByRefExpr.YesReturnableNonLocal -> true
        | _ -> false

    member ctxt.PermitOnlyReturnableNonLocal =
        match ctxt with
        | PermitByRefExpr.YesReturnableNonLocal -> true
        | _ -> false

let inline IsLimitEscapingScope env (ctxt: PermitByRefExpr) limit =
    (limit.scope >= env.returnScope || (limit.IsLocal && ctxt.PermitOnlyReturnableNonLocal))

let mkArgsPermit n =
    if n=1 then PermitByRefExpr.Yes
    else PermitByRefExpr.YesTupleOfArgs n

/// Work out what byref-values are allowed at input positions to named F# functions or members
let mkArgsForAppliedVal isBaseCall (vref: ValRef) argsl =
    match vref.ValReprInfo with
    | Some valReprInfo ->
        let argArities = valReprInfo.AritiesOfArgs
        let argArities = if isBaseCall && argArities.Length >= 1 then List.tail argArities else argArities
        // Check for partial applications: arguments to partial applications don't get to use byrefs
        if List.length argsl >= argArities.Length then
            List.map mkArgsPermit argArities
        else
            []
    | None -> []

/// Work out what byref-values are allowed at input positions to functions
let rec mkArgsForAppliedExpr isBaseCall argsl x =
    match stripDebugPoints (stripExpr x) with
    // recognise val
    | Expr.Val (vref, _, _) -> mkArgsForAppliedVal isBaseCall vref argsl
    // step through instantiations
    | Expr.App (f, _fty, _tyargs, [], _) -> mkArgsForAppliedExpr isBaseCall argsl f
    // step through subsumption coercions
    | Expr.Op (TOp.Coerce, _, [f], _) -> mkArgsForAppliedExpr isBaseCall argsl f
    | _  -> []

/// Check if a type argument is an interface with unimplemented static abstract members
/// when used with a type parameter that has interface constraints.
/// See: https://github.com/dotnet/fsharp/issues/19184
let CheckInterfaceTypeArgForUnimplementedStaticAbstractMembers (cenv: cenv) m (typar: Typar) (typeArg: TType) =
    if cenv.reportErrors then
        // Only check if the type parameter has interface constraints
        let hasInterfaceConstraint =
            typar.Constraints |> List.exists (function
                | TyparConstraint.CoercesTo(constraintTy, _) -> isInterfaceTy cenv.g constraintTy
                | _ -> false)

        if hasInterfaceConstraint && isInterfaceTy cenv.g typeArg then
            match cenv.infoReader.TryFindUnimplementedStaticAbstractMemberOfType m typeArg with
            | Some memberName ->
                let interfaceTypeName = NicePrint.minimalStringOfType cenv.denv typeArg
                errorR(Error(FSComp.SR.chkInterfaceWithUnimplementedStaticAbstractMemberUsedAsTypeArgument(interfaceTypeName, memberName), m))
            | None -> ()

/// Check types occurring in the TAST.
let CheckTypeAux permitByRefLike (cenv: cenv) env m ty onInnerByrefError =
    if cenv.reportErrors then
        let visitTyar (env, tp) =
          if not (env.boundTypars.ContainsKey tp) then
             if tp.IsCompilerGenerated then
               errorR (Error(FSComp.SR.checkNotSufficientlyGenericBecauseOfScopeAnon(), m))
             else
               errorR (Error(FSComp.SR.checkNotSufficientlyGenericBecauseOfScope(tp.DisplayName), m))

        let visitTyconRef (ctx:TypeInstCtx) tcref =
            let checkInner() =
                match ctx with
                | TopLevelAllowingByRef -> false
                | TyparInst(parentTcRef)
                | IlGenericInst(parentTcRef,_) when isByrefTyconRef cenv.g parentTcRef -> false
                | _ -> true

            let isInnerByRefLike() = checkInner() && isByrefLikeTyconRef cenv.g m tcref

            let permitByRefLike =
                if ctx.TyparAllowsRefStruct() then PermitByRefType.All else permitByRefLike


            match permitByRefLike with
            | PermitByRefType.None when isByrefLikeTyconRef cenv.g m tcref ->
                errorR(Error(FSComp.SR.chkErrorUseOfByref(), m))
            | PermitByRefType.NoInnerByRefLike when isInnerByRefLike() ->
                onInnerByrefError ()
            | PermitByRefType.SpanLike when isByrefTyconRef cenv.g tcref || isInnerByRefLike() ->
                onInnerByrefError ()
            | _ -> ()

            if tyconRefEq cenv.g cenv.g.system_Void_tcref tcref then
                errorR(Error(FSComp.SR.chkSystemVoidOnlyInTypeof(), m))

        // check if T contains byref types in case of byref<T>
        let visitAppTy (tcref, tinst) =
            if isByrefLikeTyconRef cenv.g m tcref then
                let visitType ty0 =
                    match tryTcrefOfAppTy cenv.g ty0 with
                    | ValueNone -> ()
                    | ValueSome tcref2 ->
                        if isByrefTyconRef cenv.g tcref2 then
                            errorR(Error(FSComp.SR.chkNoByrefsOfByrefs(NicePrint.minimalStringOfType cenv.denv ty), m))
                CheckTypesDeep cenv (visitType, None, None, None, None) cenv.g env tinst
            
            // Check for interfaces with unimplemented static abstract members used as type arguments
            // This only applies when the type parameter has an interface constraint - using interfaces
            // with unconstrained generics (like List<ITest> or Dictionary<K, ITest>) is fine.
            // See: https://github.com/dotnet/fsharp/issues/19184
            if tcref.CanDeref then
                let typars = tcref.Typars m
                if typars.Length = tinst.Length then
                    (typars, tinst) ||> List.iter2 (CheckInterfaceTypeArgForUnimplementedStaticAbstractMembers cenv m)

        let visitTraitSolution info =
            match info with
            | FSMethSln(_, vref, _, _) ->
               //printfn "considering %s..." vref.DisplayName
               if valRefInThisAssembly cenv.g.compilingFSharpCore vref && not (cenv.boundVals.ContainsKey(vref.Stamp)) then
                   //printfn "recording %s..." vref.DisplayName
                   cenv.potentialUnboundUsesOfVals <- cenv.potentialUnboundUsesOfVals.Add(vref.Stamp, m)
            | _ -> ()

        let initialCtx =
            match permitByRefLike with
            | PermitByRefType.SpanLike
            | PermitByRefType.NoInnerByRefLike -> TopLevelAllowingByRef
            | _ -> NoInfo

        CheckTypeDeep cenv (ignore, Some visitTyconRef, Some visitAppTy, Some visitTraitSolution, Some visitTyar) cenv.g env initialCtx ty

let CheckType permitByRefLike cenv env m ty =
    CheckTypeAux permitByRefLike cenv env m ty (fun () -> errorR(Error(FSComp.SR.chkErrorUseOfByref(), m)))

/// Check types occurring in TAST (like CheckType) and additionally reject any byrefs.
/// The additional byref checks are to catch "byref instantiations" - one place were byref are not permitted.
let CheckTypeNoByrefs (cenv: cenv) env m ty = CheckType PermitByRefType.None cenv env m ty

/// Check types occurring in TAST but allow a Span or similar
let CheckTypePermitSpanLike (cenv: cenv) env m ty = CheckType PermitByRefType.SpanLike cenv env m ty

/// Check types occurring in TAST but allow all byrefs.  Only used on internally-generated types
let CheckTypePermitAllByrefs (cenv: cenv) env m ty = CheckType PermitByRefType.All cenv env m ty

/// Check types occurring in TAST but disallow inner types to be byref or byref-like types.
let CheckTypeNoInnerByrefs cenv env m ty = CheckType PermitByRefType.NoInnerByRefLike cenv env m ty

let CheckTypeInstNoByrefs cenv env m tyargs =
    tyargs |> List.iter (CheckTypeNoByrefs cenv env m)

let CheckTypeInstNoInnerByrefs cenv env m tyargs =
    tyargs |> List.iter (CheckTypeNoInnerByrefs cenv env m)

/// Applied functions get wrapped in coerce nodes for subsumption coercions
let (|OptionalCoerce|) expr =
    match stripDebugPoints expr with
    | Expr.Op (TOp.Coerce, _, [DebugPoints(Expr.App (f, _, _, [], _), _)], _) -> f
    | _ -> expr

/// Check an expression doesn't contain a 'reraise'
let CheckNoReraise cenv freesOpt (body: Expr) =
    if cenv.reportErrors then
        // Avoid recomputing the free variables
        let fvs = match freesOpt with None -> freeInExpr CollectLocals body | Some fvs -> fvs
        if fvs.UsesUnboundRethrow then
            errorR(Error(FSComp.SR.chkErrorContainsCallToRethrow(), body.Range))

/// Examples:
/// I<int> & I<int> => ExactlyEqual.
/// I<int> & I<string> => NotEqual.
/// I<int> & I<'T> => FeasiblyEqual.
/// with '[<Measure>] type kg': I< int<kg> > & I<int> => FeasiblyEqual.
/// with 'type MyInt = int': I<MyInt> & I<int> => FeasiblyEqual.
///
/// The differences could also be nested, example:
/// I<List<int*string>> vs I<List<int*'T>> => FeasiblyEqual.
type TTypeEquality =
    | ExactlyEqual
    | FeasiblyEqual
    | NotEqual

let compareTypesWithRegardToTypeVariablesAndMeasures g amap m ty1 ty2 =

    if (typeEquiv g ty1 ty2) then
        ExactlyEqual
    else
        if (typeEquiv g ty1 ty2 || TypesFeasiblyEquivStripMeasures g amap m ty1 ty2) then
            FeasiblyEqual
        else
            NotEqual

let keyTyByStamp g ty =
    assert isAppTy g ty
    (tcrefOfAppTy g ty).Stamp

let CheckMultipleInterfaceInstantiations cenv (ty:TType) (interfaces:TType list) isObjectExpression m =
    let groups = interfaces |> List.groupBy (keyTyByStamp cenv.g)
    let errors = seq {
        for _, items in groups do
            for i1 in 0 .. items.Length - 1 do
                for i2 in i1 + 1 .. items.Length - 1 do
                    let ty1 = items[i1]
                    let ty2 = items[i2]
                    let tcRef1 = tcrefOfAppTy cenv.g ty1
                    match compareTypesWithRegardToTypeVariablesAndMeasures cenv.g cenv.amap m ty1 ty2 with
                    | ExactlyEqual -> ()
                    | FeasiblyEqual ->
                        match tryLanguageFeatureErrorOption cenv.g.langVersion LanguageFeature.InterfacesWithMultipleGenericInstantiation m with
                        | None -> ()
                        | Some exn -> exn

                        let typ1Str = NicePrint.minimalStringOfType cenv.denv ty1
                        let typ2Str = NicePrint.minimalStringOfType cenv.denv ty2
                        if isObjectExpression then
                            Error(FSComp.SR.typrelInterfaceWithConcreteAndVariableObjectExpression(tcRef1.DisplayNameWithStaticParametersAndUnderscoreTypars, typ1Str, typ2Str),m)
                        else
                            let typStr = NicePrint.minimalStringOfType cenv.denv ty
                            Error(FSComp.SR.typrelInterfaceWithConcreteAndVariable(typStr, tcRef1.DisplayNameWithStaticParametersAndUnderscoreTypars, typ1Str, typ2Str),m)

                    | NotEqual ->
                        match tryLanguageFeatureErrorOption cenv.g.langVersion LanguageFeature.InterfacesWithMultipleGenericInstantiation m with
                        | None -> ()
                        | Some exn -> exn
    }
    match Seq.tryHead errors with
    | None -> ()
    | Some e -> errorR(e)

/// Check an expression, where the expression is in a position where byrefs can be generated
let rec CheckExprNoByrefs cenv env expr =
    CheckExpr cenv env expr PermitByRefExpr.No |> ignore

/// Check a value
and CheckValRef (cenv: cenv) (env: env) v m (ctxt: PermitByRefExpr) =

    if cenv.reportErrors then
        if cenv.g.isSpliceOperator v && not env.quote then errorR(Error(FSComp.SR.chkSplicingOnlyInQuotations(), m))
        if cenv.g.isSpliceOperator v then errorR(Error(FSComp.SR.chkNoFirstClassSplicing(), m))
        if valRefEq cenv.g v cenv.g.addrof_vref  then errorR(Error(FSComp.SR.chkNoFirstClassAddressOf(), m))
        if valRefEq cenv.g v cenv.g.reraise_vref then errorR(Error(FSComp.SR.chkNoFirstClassRethrow(), m))
        if valRefEq cenv.g v cenv.g.nameof_vref then errorR(Error(FSComp.SR.chkNoFirstClassNameOf(), m))
        if cenv.g.langVersion.SupportsFeature LanguageFeature.RefCellNotationInformationals then
            if valRefEq cenv.g v cenv.g.refcell_deref_vref then informationalWarning(Error(FSComp.SR.chkInfoRefcellDeref(), m))
            if valRefEq cenv.g v cenv.g.refcell_assign_vref then informationalWarning(Error(FSComp.SR.chkInfoRefcellAssign(), m))
            if valRefEq cenv.g v cenv.g.refcell_incr_vref then informationalWarning(Error(FSComp.SR.chkInfoRefcellIncr(), m))
            if valRefEq cenv.g v cenv.g.refcell_decr_vref then informationalWarning(Error(FSComp.SR.chkInfoRefcellDecr(), m))

        // ByRefLike-typed values can only occur in permitting ctxts
        if ctxt.Disallow && isByrefLikeTy cenv.g m v.Type then
            errorR(Error(FSComp.SR.chkNoByrefAtThisPoint(v.DisplayName), m))

    if env.isInAppExpr then
        CheckTypePermitAllByrefs cenv env m v.Type // we do checks for byrefs elsewhere
    else
        CheckTypeNoInnerByrefs cenv env m v.Type

/// Check a use of a value
and CheckValUse (cenv: cenv) (env: env) (vref: ValRef, vFlags, m) (ctxt: PermitByRefExpr) =

    let g = cenv.g

    let limit = GetLimitVal cenv env m vref.Deref

    if cenv.reportErrors then

        if vref.IsBaseVal then
            errorR(Error(FSComp.SR.chkLimitationsOfBaseKeyword(), m))

        let isCallOfConstructorOfAbstractType =
            (match vFlags with NormalValUse -> true | _ -> false) &&
            vref.IsConstructor &&
            (match vref.TryDeclaringEntity with Parent tcref -> isAbstractTycon tcref.Deref | _ -> false)

        if isCallOfConstructorOfAbstractType then
            errorR(Error(FSComp.SR.tcAbstractTypeCannotBeInstantiated(), m))

        // This is used to handle this case:
        //     let x = 1
        //     let y = &x
        //     &y
        let isReturnExprBuiltUsingStackReferringByRefLike =
            ctxt.PermitOnlyReturnable &&
            ((HasLimitFlag LimitFlags.ByRef limit && IsLimitEscapingScope env ctxt limit) ||
             HasLimitFlag LimitFlags.StackReferringSpanLike limit)

        if isReturnExprBuiltUsingStackReferringByRefLike then
            let isSpanLike = isSpanLikeTy g m vref.Type
            let isCompGen = vref.IsCompilerGenerated
            match isSpanLike, isCompGen with
            | true, true -> errorR(Error(FSComp.SR.chkNoSpanLikeValueFromExpression(), m))
            | true, false -> errorR(Error(FSComp.SR.chkNoSpanLikeVariable(vref.DisplayName), m))
            | false, true -> errorR(Error(FSComp.SR.chkNoByrefAddressOfValueFromExpression(), m))
            | false, false -> errorR(Error(FSComp.SR.chkNoByrefAddressOfLocal(vref.DisplayName), m))

        let isReturnOfStructThis =
            ctxt.PermitOnlyReturnable &&
            isByrefTy g vref.Type &&
            vref.IsMemberThisVal

        if isReturnOfStructThis then
            errorR(Error(FSComp.SR.chkStructsMayNotReturnAddressesOfContents(), m))

    CheckValRef cenv env vref m ctxt

    limit

/// Check an expression, given information about the position of the expression
and CheckForOverAppliedExceptionRaisingPrimitive (cenv: cenv) expr =
    let g = cenv.g
    let expr = stripExpr expr
    let expr = stripDebugPoints expr

    // Some things are more easily checked prior to NormalizeAndAdjustPossibleSubsumptionExprs
    match expr with
    | Expr.App (f, _fty, _tyargs, argsl, _m) ->

        if cenv.reportErrors then

            // Special diagnostics for `raise`, `failwith`, `failwithf`, `nullArg`, `invalidOp` library intrinsics commonly used to raise exceptions
            // to warn on over-application.
            match f with
            | OptionalCoerce(Expr.Val (v, _, funcRange))
                when (valRefEq g v g.raise_vref || valRefEq g v g.failwith_vref || valRefEq g v g.null_arg_vref || valRefEq g v g.invalid_op_vref) ->
                match argsl with
                | [] | [_] -> ()
                | _ :: _ :: _ ->
                    warning(Error(FSComp.SR.checkRaiseFamilyFunctionArgumentCount(v.DisplayName, 1, argsl.Length), funcRange))

            | OptionalCoerce(Expr.Val (v, _, funcRange)) when valRefEq g v g.invalid_arg_vref ->
                match argsl with
                | [] | [_] | [_; _] -> ()
                | _ :: _ :: _ :: _ ->
                    warning(Error(FSComp.SR.checkRaiseFamilyFunctionArgumentCount(v.DisplayName, 2, argsl.Length), funcRange))

            | OptionalCoerce(Expr.Val (failwithfFunc, _, funcRange)) when valRefEq g failwithfFunc g.failwithf_vref  ->
                match argsl with
                | Expr.App (Expr.Val (newFormat, _, _), _, [_; typB; typC; _; _], [Expr.Const (Const.String formatString, formatRange, _)], _) :: xs when valRefEq g newFormat g.new_format_vref ->
                    match CheckFormatStrings.TryCountFormatStringArguments formatRange g false formatString typB typC with
                    | Some n ->
                        let expected = n + 1
                        let actual = List.length xs + 1
                        if expected < actual then
                            warning(Error(FSComp.SR.checkRaiseFamilyFunctionArgumentCount(failwithfFunc.DisplayName, expected, actual), funcRange))
                    | None -> ()
                | _ -> ()
            | _ -> ()
        | _ -> ()

and CheckCallLimitArgs cenv env m returnTy limitArgs (ctxt: PermitByRefExpr) =
    let isReturnByref = isByrefTy cenv.g returnTy
    let isReturnSpanLike = isSpanLikeTy cenv.g m returnTy

    // If return is a byref, and being used as a return, then a single argument cannot be a local-byref or a stack referring span-like.
    let isReturnLimitedByRef =
        isReturnByref &&
        (HasLimitFlag LimitFlags.ByRef limitArgs ||
         HasLimitFlag LimitFlags.StackReferringSpanLike limitArgs)

    // If return is a byref, and being used as a return, then a single argument cannot be a stack referring span-like or a local-byref of a stack referring span-like.
    let isReturnLimitedSpanLike =
        isReturnSpanLike &&
        (HasLimitFlag LimitFlags.StackReferringSpanLike limitArgs ||
         HasLimitFlag LimitFlags.ByRefOfStackReferringSpanLike limitArgs)

    if cenv.reportErrors then
        if ctxt.PermitOnlyReturnable && ((isReturnLimitedByRef && IsLimitEscapingScope env ctxt limitArgs) || isReturnLimitedSpanLike) then
            if isReturnLimitedSpanLike then
                errorR(Error(FSComp.SR.chkNoSpanLikeValueFromExpression(), m))
            else
                errorR(Error(FSComp.SR.chkNoByrefAddressOfValueFromExpression(), m))

        // You cannot call a function that takes a byref of a span-like (not stack referring) and
        //     either a stack referring span-like or a local-byref of a stack referring span-like.
        let isCallLimited =
            HasLimitFlag LimitFlags.ByRefOfSpanLike limitArgs &&
            (HasLimitFlag LimitFlags.StackReferringSpanLike limitArgs ||
             HasLimitFlag LimitFlags.ByRefOfStackReferringSpanLike limitArgs)

        if isCallLimited then
            errorR(Error(FSComp.SR.chkNoByrefLikeFunctionCall(), m))

    if isReturnLimitedByRef then
        if isSpanLikeTy cenv.g m (destByrefTy cenv.g returnTy) then
            let isStackReferring =
                HasLimitFlag LimitFlags.StackReferringSpanLike limitArgs ||
                HasLimitFlag LimitFlags.ByRefOfStackReferringSpanLike limitArgs
            if isStackReferring then
                { limitArgs with flags = LimitFlags.ByRefOfStackReferringSpanLike }
            else
                { limitArgs with flags = LimitFlags.ByRefOfSpanLike }
        else
            { limitArgs with flags = LimitFlags.ByRef }

    elif isReturnLimitedSpanLike then
        { scope = 1; flags = LimitFlags.StackReferringSpanLike }

    elif isReturnByref then
        if isSpanLikeTy cenv.g m (destByrefTy cenv.g returnTy) then
            { limitArgs with flags = LimitFlags.ByRefOfSpanLike }
        else
            { limitArgs with flags = LimitFlags.ByRef }