I don't understand why you expect bar to typecheck: signature explicitly contradicts the body, since Y_ {d=S d} whatever has type Y (S d)

There's no spec yet so I can only guess what should happen. But to be consistent, because foo doesn't fail then bar shouldn't fail either, or they both should fail. Right now, foo typechecks but bar does not.

I can't agree with you. Roughtly,

record Ty (q param : Ty2) where
  constructor MkTy
  field1 : Ty3
  field2: Ty4

is syntactically translated to

data Ty : (q param : Ty2) -> Type where
  MkTy : {q param : Ty2} -> (field1 : Ty3) -> (field2 : Ty4) -> Ty param

That's why, type of X_ is {0 d : Nat} -> (d : Nat) -> (a : Nat) -> X d, that's why the value of parameter of X is determined by the explicit argument, not the implicit one. Since Y doesn't have shadowing implicit parameter, there is no such a problem.

So, considering the current (very simple in its spirit) translation of records to data, all behaves as expected.

There is another question of what translation would you expect having the same names in the type signature and the field (your X example). Would you expect X_ to have a type (d : Nat) -> (a : Nat) -> X d or (d : Nat) -> (a : Nat) -> {0 d : Nat} -> X d?

I mean, since you are matching implicit d and explicit d2 separately, I see that you are expecting them to be separate parameters. However, in ideal world, I would expect X to not to have any implicit parameter at all having your definition.

I was under the assumption that in the following code, copied from above for convenience,

record X (d : Nat) where -- <-- #1
  constructor X_
  d : Nat -- <-- #2
  a : Nat

that the d in line marked #1 would reference the same variable as the d in line marked #2.

I think you are agreeing with me on this, although maybe you can confirm?

That was my guess as to how it should behave, that is, you should be able to do:

record X (d : Nat) where -- <-- #1
  constructor X_
  d : Nat -- <-- #2
  a : Nat

foo : X d -> X (S d)
foo (X_ d a) = X_ (S d) a

However that didn't work, so I found the implicit and explicit vars available and in

foo : X d -> X d -- <-- #3
foo (X_ {d} d2 a) = X_ {d=S d} d2 a -- <-- #4

it seems that the d parameter in line #3 is actually the implicit variable in the body of the above function, {d} in line #4. However, since you can modify it to be S, and not change the return type of X d to X (S d), it can't be that, so it seems that it references the d in line #2. That to me is very strange since #2 is explicit so why is it being treated as an implicit variable. But actually, that is not the case.

If you run the following with showimplicits on, you get:

λΠ> foo {d=1} (the (X 1) $ X_ 1 1)
X_ {d = S ?d} 1 1

Which is very strange.

Also I may not be quite understanding what this means, but my interpretation is there is a initial variable with no name that isn't used in the definition on X_:

λΠ> :t X_
Main.X_ : {0 _ : Nat} -> (d : Nat) -> Nat -> X d

So actually, I don't know what to make it, but it seems like something isn't right here.

Also, I don't understand your syntactic translation, specifically what param is suppose to mean. I tried typechecking it in idris and it fails with:

-   Errors (1)
 `-- Feex.idr line 2 col 0:
     Expected end of input.
     
     Feex:2:1--2:5
      1 | 
      2 | data Ty : (q param : Ty2) -> Type where
          ^^^^

that the d in line marked #1 would reference the same variable as the d in line marked #2.

I don't think that should be the case. Records don't have any way to constrain the shape of their
parameters. If you could force a specific field to appear as a parameter, you'd accidentally add
this ability but only for variables, not for arbitrary expressions like in data declaration.
This is an accident of the (broken) way in which records are currently elaborated.