Rust, 60 bytes

Takes a list of integers in [0..14) as input, with each element x representing a 0-based index into the sequence [&a, &b, ..., &g, &mut a, &mut b, ..., &mut g]. This way, x%7 gives the variable name and x/7 gives the mutability (0 for immutable, 1 for mutable). Returns true if mutable aliasing is present and false if it is absent.

|a:&[_]|a.iter().map(|x|x/7*6+1<<x%7*6).sum::<u64>()&!0/18>0

Attempt This Online!

Explanation

We take advantage of the restriction that input lists have a maximum length of 7. The fundamental idea here is that we assign a per-variable weight to references -- 1 for immutable references and 7 for mutable references -- and then check whether any variable has a total weight greater than 7. (If a variable has up to 7 immutable references or a single mutable reference, then the weight will be at most 7, but one mutable reference + one other reference will push the weight above 7.) In code:

def has_mutable_aliasing(arr):
    weights = {'a': 0, 'b': 0, 'c': 0, 'd': 0, 'e': 0, 'f': 0, 'g': 0}
    for name, mutable in arr:
        weights[name] += 7 if mutable else 1
    return any(weight > 7 for weight in weights.values())

We can adapt this approach to lists of arbitrary length by replacing each instance of 7 with len(arr), but limiting the number of list elements and distinct variables to a small number allows us to make an optimization by replacing weights with a 64-bit integer:

      0b_??????_??????_??????_??????_??????_??????_??????
weights: gggggg ffffff eeeeee dddddd cccccc bbbbbb aaaaaa

Now, we can simply transform the references as follows, and sum them up:

&a     (0)     => 0b_000000_000000_000000_000000_000000_000000_000001
&b     (1)     => 0b_000000_000000_000000_000000_000000_000001_000000
...
&g     (6)     => 0b_000001_000000_000000_000000_000000_000000_000000
&mut a (0 + 7) => 0b_000000_000000_000000_000000_000000_000000_000111
&mut b (1 + 7) => 0b_000000_000000_000000_000000_000000_000111_000000
...
&mut g (6 + 7) => 0b_000111_000000_000000_000000_000000_000000_000000

The .map(|x|x/7*6+1<<x%7*6) part of the code is responsible for transforming references this way.

To test whether any of the weights exceed 7, we can bitwise-AND the sum with a number whose binary representation ends in 111000_111000_111000_111000_111000_111000_111000 -- in this case, floordiv(2^64 - 1, 18) -- and checking if the result is not all 0s. If any of the 3 top bits for any of the weights are set, then at least one weight is above 7, which means at least one variable exhibits mutable aliasing. Note that 7 mutable references to the same variable yields a weight of 0b110001, which is not enough to cause problems with overflow.

APL(Dyalog Unicode), 15 14 bytes^SBCS

A dfn that takes [mut,not mut ...] boolean array as its left argument, and takes the variable names as its right argument.

Unique ∪ of the intersection ∩ between is_mutable ⍺ and the second or more appearance of variables ~≠⍵ over the corresponding variable ⌿∘⍵.

{∪⍺∩⍥(⌿∘⍵)~≠⍵}

Try it on APLgolf!

Try it on APLgolf! 15 bytes

APL (Dyalog Unicode), 9 bytes ^SBCS

/∧/⍤≠⍤∩⍨⊢

Try it on APLgolf!

A tacit function which takes a vector of mutabilities on the left and a string of variable names on the right. (Test harness stolen from akamayu.) Port of my Jelly solution. My first time actually trying to golf in APL, so I've probably done something terribly wrong--I did check APLCart for an "all unique" idiom, but given that it isn't the start of a train (⊢≡∪) loses by 1 to ∧/⍤≠.

/            Replicate: filter the names to only mutable references.
      ∩⍨⊢    Intersection: filter all of the names to those with mutable references.
/      ⍨     (The / glyph is ambiguous between Replicate and Reduce if not danced around.)
     ⍤       Then
    ≠        nub sieve,
   ⍤         and then
 ∧/          reduce by AND.

10 bytes as a dfn: {∧/≠⍵∩⍺/⍵}

Jelly,  9  7 bytes

-2 building upon UnrelatedString's suggested eight, ṢƙṪ€UḄḂƑ.

ṢƙṪ€SḊẸ

A monadic Link that accepts a list of pairs, each of the form^* \$(N, M) \mid N \in \Bbb{N}^+, M \in \Bbb{Z}_2\$, and yields \$1\$ if mutable aliasing is present or \$0\$ if not.

^{* e.g. &mut c, &f would be input as [[3, 1], [6, 0]]}

Try it online! or see the test-suite.

How?

ṢƙṪ€SḊẸ - Link: list of pairs P = [[N1, M1], [N2, M2], ...]
  Ṫ€    - tail of each of {P} (altering P to [[N1], [N2], ...] in the process)
 ƙ      - group {that} by {the altered P} and apply to each:
Ṣ       -   sort
    S   - sum (column-wise)
     Ḋ  - dequeue
      Ẹ - any?

Jelly, 4 bytes

fxQƑ

Try it online!

Takes a list of variable names on the left and a list of their mutabilities on the right.

 x      Replicate: yield a list of only mutable references.
f       Filter the *full* list of referenced names to those in that list.
  QƑ    Is every element of the filtered list unique?

Haskell + hgl, 12 bytes

ay cr<xqB st

Attempt This Online!

Explanation

• xqB remove elements that have a unique ...
• st first element (variable name)
• ay does any remaining value have a true ...
• cr final element (mutability)

Reflection

This is pretty solid. I don't really thing there's anything that needs to be improved in hgl. However I should check if ay cr or ay st has been used before, if either of these has I think that would be justification to add both.

Retina 0.8.2, 15 13 bytes

O`.#?
1`(.)\1

Try it online! Takes input as a list of just the letters with the immutable references marked by a trailing # but link is to test suite that converts the test cases to this format for you. Outputs 0 for absent and 1 for present (if inconsistent larger numbers are allowed then the 1 can be removed to save two bytes). Explanation:

O`.#?

Sort all of the references in order, so the mutable references for a comes first and the immutable references for g comes last.

1`(.)\1

Check for a mutable reference followed by another reference to the same variable.

Nekomata + -e, 5 bytes

ĕ∏Hᵗf

Attempt This Online!

Takes input as a list of [variable, is_mutable] pairs, where variable is a string and is_mutable is an integer (0 or 1).

Outputs True for present and False for absent.

ĕ∏Hᵗf
ĕ       Take one element out from the input
 ∏      Product; strings are converted to their code points
  H     Convert the code points back to a string
        After these two steps, [v,1] becomes v and [v,0] becomes a null character
   ᵗf   Check that the rest of the input contains this string

-e checks if there is a solution.

Let's take [["f",0],["e",0],["e",1],["d",0]] as an example. In the first step (ĕ), we can take out ["e",1], which becomes "e" after applying ∏H. The rest of the input is [["f",0],["e",0],["d",0]], which contains "e". Therefore, the output is True.

Charcoal, 10 bytes

⊙θ›№θ↥ι№αι

Try it online! Link is to verbose version of code. Takes input as a string of letters where lowercase letters are immutable references and uppercase letters are mutable references and outputs a Charcoal boolean, i.e. - for present, nothing for absent. Explanation: Port of @xnor's Python answer.

 θ          Input string
⊙           Any letter satisfies
   №        Count of
      ι     Current letter
     ↥      Uppercased
    θ       In input string
  ›         Is greater than
       №    Count of
         ι  Current letter in
        α   Predefined variable uppercase alphabet
            Implicitly print

Python, 40 bytes

lambda l:any(l.count(n|1)>n%2for n in l)

Try it online!

Takes input as "a list of integers in [0..14), each representing one of the 14 possible values", with the last bit for mutability (1=mutable) and the rest indicating the variable. Output is True/False.

For each element n in the list, checks if n|1, which has its mutability bit set, appears at least once if n is even (immutable) and twice if n is odd (mutable).

42 bytes with (variable, is_mutable) tuple inputs:

lambda l:any(b<l.count((k,1))for k,b in l)

Python, 48 bytes

lambda L,*k:all(m*k!=(k:=l)for l,m in sorted(L))

Attempt This Online!

Takes a list of pairs (name, is_mutable).

Funge-98, 43 bytes

#;~:a`j@4k:0g1+\0p1g&+\1p0g'!`\1g' `*2j@._;

Try it online!

Takes input as pairs of letters (a-g) and binary digits, such as a1, each of which must be followed by a newline. These pairs must be followed by another newline. The digits are 1 if a reference is mutable, and 0 if it is not.

Outputs 0 if mutable aliasing occurs, and nothing otherwise.

Vyxal, 75 bits^v2, 9.375 bytes

⁽hġƛvtÞżU₃;A

Try it Online!

Bitstring:

111001011100101011110100010010000000011001111000100101100100001011101110111

Bitstring:

111001011100101011110100010010000000110011101001010111100110010

Takes input as [[var: str, mut: bool (0/1)]], returns 1 for absent, 0 for present. The header converts the tuples in the example input into lists (which you'd otherwise do manually).

Explained

⁽hġƛvtÞżU₃;A­⁡​‎‎⁡⁠⁡‏⁠‎⁡⁠⁢‏⁠‎⁡⁠⁣‏‏​⁡⁠⁡‌⁢​‎‎⁡⁠⁤‏⁠‎⁡⁠⁣⁡‏‏​⁡⁠⁡‌⁣​‎‎⁡⁠⁢⁡‏⁠‎⁡⁠⁢⁢‏‏​⁡⁠⁡‌⁤​‎‎⁡⁠⁢⁣‏⁠‎⁡⁠⁢⁤‏‏​⁡⁠⁡‌⁢⁡​‎‎⁡⁠⁣⁡‏‏​⁡⁠⁡‌⁢⁢​‎‎⁡⁠⁣⁢‏‏​⁡⁠⁡‌⁢⁣​‎‎⁡⁠⁣⁤‏‏​⁡⁠⁡‌­
⁽hġ           # ‎⁡Group the input based on the variable name
   ƛ    U     # ‎⁢To each group:
    vt        # ‎⁣  Get whether each reference is mutable
      Þż      # ‎⁤  Multiply each item by its 1-based index
        U     # ‎⁢⁡  Uniquify - this ensures that only one immutable reference is kept, while keeping all mutable references. Basically, treat all immutable references as the same.
         ₃    # ‎⁢⁢  Is there only one item in that list?
           A  # ‎⁢⁣Is that true for all possible variables?
💎

Created with the help of Luminespire.

JavaScript (Node.js), 28 bytes

x=>/t (.).*\1.*\1/.test(x+x)

Try it online!

Handles both direction by 2 copies