Type mismatch error when using domain subtraction on function variable

I have this formal specification and the error seems to be simple to fix. However, I have spent a decent amount of time and still cannot figure out. The error is related to domain subtraction. The snippets of the context and machine are below:

CONTEXT
    Drone_Ctx
SETS
    DRONES
    TARGETS
CONTSTANTS
    assigned
AXIOMS
    axm1: assigned : DRONES ↔ TARGETS
END

MACHINE
    AV_0
SEES
    Drone_Ctx
VARIABLES
    loc
    reached
INVARIANTS
    inv1: loc : DRONES → TARGETS
    inv2: reached ⊆ DRONES
EVENTS
    INITIALISATION
    THEN
        act1: loc := ∅
        act2: reached := ∅
    END

    Abort_Mission:
    ANY
        dr
    WHERE
        grd1: dr ∈ DRONES
        grd2: dr ∈ dom(loc)
        grd3: dr ∉ reached
    THEN
        act1: loc := loc ⩤ {dr}
    END
END

The error message thrown because of this statement: loc := loc ⩤ {dr} despite correct typing is:

Multiple markers at this line

• Types DRONES×TARGETS and DRONES do not match
• Types DRONES and '1×'2 do not match

Please advise!

I tried initializing loc ∈ DRONES → TARGETS using loc ≔ ∅, ∅ ▷ assigned, and assigned ⩤ DRONES, expecting Rodin to infer the correct function type. But I still get type mismatch errors like the following when using loc ⩤ {dr}:

Types DRONES×TARGETS and DRONES do not match .

The error is in the order of the operator's arguments, the domain subtraction expects the set as left argument, the relation as right argument

loc := loc ⩤ {dr}

should be

loc := {dr} ⩤ loc