Why haven't newer dependently typed languages adopted SSReflect's approach? : <p>There are two conventions I've found in Coq's SSReflect extension that seem particularly useful but which I haven't seen widely adopted in newer dependently-typed languages (Lean, Agda, Idris).</p>

<p>Firstly, where possible predicates are expressed as boolean-returning functions rather than inductively defined datatypes. This brings decidability by default, opens up more opportunities for proof by computation, and improves checking performance by avoiding the need for the proof engine to carry around large proof terms. The main disadvantage I see is the need to use reflection lemmas to manipulate these boolean predicates when proving.</p>

<p>Secondly, datatypes with invariants are defined as dependent records containing a simple datatype plus a proof of the invariant. For instance, fixed length sequences are defined in SSReflect like: </p>

<pre><code>Structure tuple_of : Type := Tuple {tval :&gt; seq T; _ : size tval == n}.
</code></pre>

<p>A <code>seq</code> and a proof of that sequence's length being a certain value. This is opposed to how e.g. Idris defines this type:</p>

<pre><code>data Vect : (len : Nat) -&gt; (elem : Type) -&gt; Type 
</code></pre>

<p>A dependently typed datastructure in which the invariant is part of its type. One advantage of SSReflect's approach is that it allows reuse, so that for instance many of the functions defined for <code>seq</code> and proofs about them can still be used with <code>tuple</code> (by operating on the underlying <code>seq</code>), whereas with Idris' approach functions like <code>reverse</code>, <code>append</code> and the like need to be rewritten for <code>Vect</code>. Lean actually has a SSReflect style equivalent in its standard library, <code>vector</code>, but it also has an Idris-style <code>array</code> which seems to have an optimised implementation in the runtime.</p>

<p>One <a href="http://ilyasergey.net/pnp/pnp.pdf" rel="noreferrer">SSReflect-oriented book</a> even claims the <code>Vect n A</code> style approach is an antipattern:</p>

<blockquote>
  <p>A common anti-pattern in dependently-typed languages and Coq in particular is to encode such algebraic properties into the definitions of the datatypes and functions themselves (a canonical example
  of such approach are length-indexed lists). While this approach looks appealing, as it demonstrates
  the power of dependent types to capture certain properties of datatypes and functions on them, it
  is inherently non-scalable, as there will be always another property of interest, which has not been
  foreseen by a designer of the datatype/function, so it will have to be encoded as an external fact
  anyway. This is why we advocate the approach, in which datatypes and functions are defined as close
  to the way they would be defined by a programmer as possible, and all necessary properties of them
  are proved separately.</p>
</blockquote>

<p>My question is hence, why haven't these approaches been more widely adopted. Are there disadvantages I'm missing, or maybe their advantages are less significant in languages with better support for dependent pattern matching than Coq?</p>
