Decidability of equivalence is broken somewhere between simply typed lambda calculus and System-F. Without recursive types you are strongly normalizing and thus “trivially” decidable. However, just adding recursive types does not break decidability (e.g. see http://www.di.unito.it/~felice/pdf/ictcs.pdf). Similarly, just adding some higher-order functions or parametric polymorphism does also not necessarily break decidability (e.g. see Hindley-Milner). In my (admittedly limited) experience, when making a type system stronger, it is usually some strange, sometimes subtle interaction of these “type system features” that break decidability.
So the first problem raised in the OP is probably tractable for many, quite expressive type systems, even including recursive types.
Though I fully agree with you that the second problem is usually how undecidability proofs start and I’m more skeptical towards that one.
Decidability of equivalence is broken somewhere between simply typed lambda calculus and System-F. Without recursive types you are strongly normalizing and thus “trivially” decidable. However, just adding recursive types does not break decidability (e.g. see http://www.di.unito.it/~felice/pdf/ictcs.pdf). Similarly, just adding some higher-order functions or parametric polymorphism does also not necessarily break decidability (e.g. see Hindley-Milner). In my (admittedly limited) experience, when making a type system stronger, it is usually some strange, sometimes subtle interaction of these “type system features” that break decidability.
So the first problem raised in the OP is probably tractable for many, quite expressive type systems, even including recursive types.
Though I fully agree with you that the second problem is usually how undecidability proofs start and I’m more skeptical towards that one.