There is general consensus that the best way to handle effects is
a pure base language with an effect system on top.

No, there is absolutely no consensus on this. This approach is only
popular with researchers who pray at the church of lambda.
Essentially all programming languages that are not research prototypes
and that are used in industrial practise don't follow this approach.
There are valid reasons for this. A much better approach in my
opinion is to start with an unrestricted, effectful language and identify fragments with fewer effects via types. The problem is that adding interesting effects effects on top of something super restricted like pure functions leads to a high "encoding tax". That's because pure functions are not very expressive.

Why did type inference become the #1 criterion for a type system
in this discussion?

We have been talking about large-scale software engineering, and
whether Curry-Howard or program logic is a more scalable approach
towards program verification. My claim is that in large-scale software
engineering the single most important criterion is to minimise the
cost of change. Type-inference has 0 cost of change, since it's fully
automatic. I cannot see how a verification tool that I'm forced to use
in prototype phases when there is no stable specification is
cost-effective in large-scale software engineering.

There are far more important criteria than type inference, such
as expressiveness.

Sheer expressiveness is not interesting. You can produce trivial
typing systems where every program is typable. What really matters is
to find "sweetspots" between the following desirable features of
typing systems.

- Expressiveness.

- Strength of properties guaranteed by typing.

- Speed (including decidability) of type-checking or type-inference.

Unfortunately there are hard trade-offs between them.

Doing type inference for non HM-typeable parts of programs is
theoretically simple.

I don't believe it's that simple to do it well, and people do publish
in this area, see for example the Trellys project by Vilhelm Sjöberg.
I think it's an unsolved problem. It may be possible to get a
pragmatically viable system that combines proving and programming in a
unified system, but we are not there yet, and whether the result is
superior to, or on par with simple programming languages and an
associated logic can only be considered when such a language is
available. And note that work like Sjöberg's is about combining pure
functional programming with constructive logic in one system. Even if
some kind of polished Haskell with dependent types can be build,
whether that then generalises to state, concurrency, timing etc in a clean way is
another open question.

I would also suggest that your experience may not yet have been
that extensive if you didn't know about implicit parameters?

Having used Agda, I know about them, I just wasn't sure what you
meant. The term is used in with different meanings in different
contexts. For example they work differently in Scala. And no, it's not
the implicit parameters that make type inference for Agda's MLTT
undecidable.

Look at the Sage work for full inference for refinement types.

Do you mean Cormac Flanagan's Sage? That's not full type inference.
Sage use hybrid type-checking and inserts dynamic checks where type inference fails. This might be
a very good way of doing things in practise, I don't know. Maybe not.

Type inference for GADTs is undecidable.

Are you sure? http://research.microsoft.com/pubs/79812/outsidein-icfp09.pd...