Relationship between inductive families and type-returning functions
As mentioned by Andrej, this is an instance of transporting along an equivalence of families and display maps. In this specific case, we have an equivalence of graphs and relations.
open import Function
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Level renaming (zero to lzero; suc to lsuc)

-- type of relations on a set
Rel : ∀{i j} → Set i → Set (i ⊔ lsuc j)
Rel {i}{j} V = V → V → Set j

-- type of graphs with set of vertices V
record Graph {i j}(V : Set i) : Set (i ⊔ lsuc j) where
  field
    E   : Set j   -- edges
    src : E → V   -- source vertex
    tgt : E → V   -- target vertex
open Graph

Rel→Graph : ∀ {i j V} → Rel {i}{j} V → Graph {i}{i ⊔ j} V
Rel→Graph R = record {
  E   = ∃₂ λ s t → R s t ;
  src = proj₁ ;
  tgt = proj₁ ∘ proj₂ }

Graph→Rel : ∀ {i j V} → Graph {i}{j} V → Rel {i}{i ⊔ j} V
Graph→Rel {V} G s t = ∃ λ e → (G .src e ≡ s) × (G .tgt e ≡ t)

Note that we can only define the round-tripping functions if i ≤ j, since then the output i ⊔ j level becomes j, and the trip is well-typed. Your Link definition does not fit into this, but it's possible to just redefine it as Link : Set → Set → Set₁ without loss of generality (as the two definitions are equivalent).
If the levels check out, we can show that round-tripping in both directions yields equivalent relations and graphs respectively. We don't need to know anything about the internals of the relations and graphs involved; this equivalence always holds.
Your transformation makes use of the fact that the set of edges for the graph is equivalent to a small set, since the relation only has two possible edges.
open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.Nat

data Link : Set → Set → Set where
  link-a : Link ⊤ Bool
  link-b : Link ℕ ℤ

-- the graph of Link
Link' : Graph Set
Link' = Rel→Graph Link

-- an equivalent graph with smaller edges
Link'' : Graph Set
Link'' = record {
  E   = Bool ;
  src = λ {false → ⊤; true → ℕ} ;
  tgt = λ {false → Bool; true → ℤ} }

Now, anything which depends on an edge only needs do depend on a Bool. In particular, Tie' Link'' : Set.
record Tie {j} (R : Rel {_}{j} Set) : Set (lsuc j) where
  field
    E   : ∃₂ λ A B → R A B
    fun : proj₁ E → proj₁ (proj₂ E)

record Tie' {j} (G : Graph {_}{j} Set) : Set j where
  field
    E   : G .E
    fun : G .src E → G .tgt E

The equivalence of graphs and relations generalizes to relations of any arity, and also to multiple relations of arbitrary arities, where relations can be indexed over other relations. In general, the equivalence says that for each telescope of dependent n-ary relations, there is a direct category $C$ such that the telescope is equivalent to the set of functors from $C$ to $\textbf{Set}$.
In the case of graphs, $C$ has two objects and two arrows between them, going in the same direction, so a functor $F : [C,\textbf{Set}]$ consists of two sets $V,E$ and two functions $src, tgt : E \rightarrow V$, so we can see that every $F$ is a graph.

Are Tie and Tie′ meaningfully distinct, in the sense that Tie allows
doing things that Tie′ does not?

They are equivalent, we get one from the other by transporting the parameter along the graph-relation equivalence.

Seeing as the transformation is entirely mechanical, intuitively it
seems we ought to be able to somehow achieve Tie Link : Set while
retaining Link as an indexed type, but it isn’t clear to me that this
is actually possible.

If we're working in cubical Agda, the graph-relation equivalence can be proven using univalence. Then, every possible construction which depends on relation can be transported to another which depends on a graph. Additionally, everything which depends on Link can be transported to depend on Rel→Graph Link. So at least this part works completely automatically.
However, the resizing part is not automatic, i.e. we have to prove that Rel→Graph Link is equivalent to Link'' with the small set of edges. It is not true in general that the set of edges for a relation is smaller than the set of vertices. Probably it's possible to have a conservative algorithm which tries to find such resizings, I don't think it has been researched.

... in a similar sense to that described in Inductive families need
not store their indices. Is this reasoning flawed, or is this simply
an implementation infelicity?

The technique in &quot;Inductive types need not store their indices&quot; is related but not exactly the same thing. In that paper, the transformation is a bit more restricted &amp; specific thing, as there the point is to convert an inductive type family to a purely recursive one. The family-display map translation can be also used to get rid of indices, but that works in a &quot;non-algorithmic&quot; and different way. A classic example is vectors.
Let's have Vec A : ℕ → Set. We have an equivalence between ℕ → Set and Σ Set λ A → (A → ℕ) (as another case of the family-display map equivalence).
open import Data.Vec
-- Vec : Set → ℕ → Set

Vec' : Set → Σ Set λ A → (A → ℕ)
Vec' A = ∃ (Vec A) , proj₁

But now we can notice that ∃ (Vec A), the so-called &quot;total&quot; type (analogous to the type of edges previously) is equivalent to List A.
open import Data.List

Vec'' : Set → (∃ λ A → A → ℕ)
Vec'' A = List A , Data.List.length

Now, we can convert back to the family version with the generic equivalence:
Vec''' : Set → ℕ → Set
Vec''' A n = ∃ λ (l : List A) → Data.List.length l ≡ n

Which is a definition of vectors which does not store indices. But this is more like a hint, and this de-indexing does not work in a mechanical way, unlike the &quot;need not store indices&quot; technique.

Has the relationship between these two constructions been treated
explicitly in any existing literature?

I don't know of any reference which is exclusively about this equivalence, but it's commonly featured in category theory and type theory (or math in general). The two definitions of graphs is a classic example. There's also the equivalence of indexed categories (family version) and fibrations (display map).