We resolved fixme! already; let’s move on. 
Sure; the todo! macro could expand to the same construct in the language and thus be equivalent.
However, you’ll need to have that construct in the type system to be able to say things like let x: todo!() = expr;
Perhaps not necessary no; but it does make it clearer where the holes are and it makes less things legal syntax in the grammar (and this is significant due to macros). My experience with holes in Idris and Agda have been nothing but positive.
Elaborate? Why would it be so massive (and do you mean implementation complexity or user facing complexity?)?
From the side of the grammar you’d need to add the token ? (or something else, but this one seemed apt…) to 3 places: the term grammar, the type grammar, the trait grammar.
For the term grammar ? becomes a diverging expression for an unknown empty type which happens to coerce to everything else and also implements all traits (~ modulo some questions around what traits this is sound for; we can start with a conservative subset…).
For the type side of things, ? becomes a type error that tells you what the inferencer found; Most of this machinery should already exist; we mostly need to tailor the error messages.
For the bound side of things, you can now write where T: ? and inference should tell you what the most permissive bound ? could be to make the body typeck.
None of this strikes me as massively complex to implement; On the user complexity side of things ? is a fairly intuitive syntax for “I don’t know, please tell me”; it’s also uniformly the same syntax for incomplete programs everywhere so that seems simple enough to explain to people.
