This is a tough question to answer, since simplicity is in the eye of the beholder.
Certainly $\lambda$-encodings have their drawbacks, there are reasons why Coq decided to move away from them, the most obvious one is the inability to introspect the subterms during recursion. The second is the general awkwardness in defining deeply or mutually recursive functions.
As you note, the "fix-encoding" avoids this but then it is hard to define non-constant functions (which is the point Damiano brings up)! You have to choose: introspection or recursion. Often we want both.
I'm also a bit skeptical of Gabriel's proposal: how does he compute exponentials on "native" ints without recursion?
In addition, the fact that EAL can only express elementary functions seems intuitively like it should restrict "natural" ways of writing recursions. In particular this shouldn't be well-defined:
Fixpoint acker m := match m with
| O => S
| S m => (fix acker' f n := match n with
| O => f 1
| S n => f (acker' f n)
end)
(acker m)
end.
since it defines a non-elementary function. So what feature of EAL is preventing this definition? If I understand correctly (and I'm not sure I do), the term f (acker' f n) cannot be well-typed, there must be some "stratum" which prevents the final application of f.
So certainly the natural way to write this function is forbidden. What other natural things are forbidden in this framework? It's hard to say without asking a specialist, but my guess is that there will be a fair number of things. Linear type systems can be powerful frameworks, but they aren't very convenient or natural for writing programs.
It's also an important fact (but maybe this is asking for a lot) that $0\neq 1$ is directly provable in Coq, thanks to large elimination. Is adding this feature easy in your proposal?
Finally, there's something I'm always worried about when I hear about type systems with linear logic: how hard is it to write a type checker? Certainly the checker has to figure out which pieces of the context go where when performing checking. Also the user or the front-end has to figure out where to put all the !s, if you want to have any non-linear components (and you usually do!).
To summarize, my answer to the question "is EAL with dependent types simple, consistent and expressive?" is probably not: it is probably consistent, but I'm not sure it's simple, and I don't think it is sufficiently expressive.
However, there is a "simple" way to refute this claim: write down the system definition, ideally prove it consistent, and write down some simple functions using it, probably up to, say, red-black trees or something. If the fully detailed syntax and typing rules is large, then the system is complex, if it is very tough to write down the functions, then it is insufficiently expressive. If it is neither of those, then you've answered a tough open problem in type theory!
Nat = fix self . (Nat : *) -> (self -> Nat) -> Nat -> Nat. While this encoding captures pattern matching, it doesn't capture recursion. To allow recursion with pattern matching you need term level fixed points or a more complex machinery (mutually recursive definitions) as the paper on self types says. $\endgroup$