Thanks @mtzguido! I've started work on a branch to retain universes in the SMT encoding. It requires a non-trivial structural change to the SMT translation, but it's also the right fix. Will post back here with updates.

This makes sense since no function can return itself due to the universe hierarchy

Let me restate that as "no total function..."

val fd : unit -> Dv (x:Type u#0 & x)
let rec fd () = (| _, fd |)

This works since a -> Dv b is always in Type0.

Following several discussions with @aseemr about this, we have the
following proposal for fixing this issue. Comments welcome. @mtzguido @catalin-hritcu?

Removing FStar.WellFounded.axiom1_dep/axiom1 and internalizing it

As Bug 2069 shows (#2069)
FStar.WellFounded.axiom1_dep (and it's non-dependent specialization
FStar.WellFoudned.axiom1) is incompatible with the universe-free
encoding of F* to SMT.

The trouble is that the axiom allows one to write and prove
things like id u#0 << id u#1 which in the SMT encoding, after
universe erasure, amounts to id << id, which is a
contradiction.

In nik_smt_univs, I have been trying out a variant of the SMT
encoding that does not erase universes and faithfully records
universe abstractions and applications. In that branch, such
inconsistencies are no longer provable. However, adding universes
to the SMT encoding is a heavy hammer that impacts proofs of all
programs, regardless of whether or not they rely on
FStar.WellFounded.axiom1_dep.

So, we have been considering other ways to express the intent of
FStar.WellFounded.axiom1 without needing to add universes everywhere
in the SMT encoding. Here is one proposal.

What is the purpose of FStar.WellFounded.axiom1_dep

Here's the troublesome axiom.

assume
val axiom1_dep : #a:Type -> #b:(a->Type) -> f:(y:a -> Tot (b y)) -> x:a ->
                        Lemma (f x << f)

let axiom1 #a #b (f:a -> Tot b) (x:a)
  : Lemma (f x << f)
  = axiom1_dep f x

The purpose of this axiom is to facilitate termination proofs of
recursive functions over inductive types in which it is required to
show that the elements of the codomain of a total function f are smaller
than a term containing f itself.

More concretely, consider:

noeq
type tree a =
  | Leaf : data:a -> tree a
  | Node : children:(nat -> tree a) -> tree a

let rec map #a #b (f:a -> b) (x:tree a)
  : Tot (tree b)
  = match x with
    | Leaf data -> Leaf (f data)
    | Node ch -> Node (fun n -> WF.axiom1 ch n; map f (ch n))

Here, to justify the recursive call map f (ch n), we need to show
that ch n is smaller than x. But, since (from axiom1),
ch n << ch and, from the subterm ordering on tree a, ch << x,
we have ch n << x by transitivity.

Removing FStar.WellFounded.axiom1_dep

The statement of WF.axiom1_dep is problematic---it immediately leads
to contradiction with the SMT encoding.

Further, needing to expliclity invoke WF.axiom1 at each call site is
also sub-optimal.

We will remove FStar.WellFounded.axiom1_dep.

Rather than providing a universe polymorphic WF.axiom1_dep for all
total functions, we will instead extend the encoding of F* inductive
types to provide more targeted axioms for recursive functions over
inductive types.

Consider this example:

noeq
type tree a =
  | Leaf : data:a -> tree a
  | Node : children:(nat -> tree a) -> tree a

Currently, in the SMT encoding of tree a, we generate the following
subterm ordering axioms:

forall (a:Type) (data:a). data << Leaf data
forall (a:Type) (children:nat -> tree a). children << Node children

The proposal is to add a third ordering axiom to this encoding, of
this form:

forall (a:Type) (children:nat -> tree a). (forall (n:nat). children n << Node children)

There are a few points to note about this axiom:

-- It states that every element of the co-domain of children is
smaller than Node children. It does not state that children n << children. We'll see why that's important below.

-- f x << f is no longer provable.

With this change, it should be possible to simply write:

let rec map #a #b (f:a -> b) (x:tree a)
  : Tot (tree b)
  = match x with
    | Leaf data -> Leaf (f data)
    | Node ch -> Node (fun n -> map f (ch n))

since we'll get ch n << x directly from the axiom at the recursive call.

Impact on the counterexample

Guido's original counterexample stems from being able to prove that
for a polymorphic identity function

let id (a : Type u#aa) (x:a) : a = x

id #u1 (a: Type u#0 -> a -> a) (id #u0)
== (by definition)
id u#0
<< (by WF.axiom1)
id u#1

and due to universe erasure, this leads to id u#0 << id u#0.

But, in this proposal, it is no longer possible to prove f x << f, so this
counterexample is blocked.

One might be concerned about an example such as this one:

An inductive type t holding a identity function.

noeq
type t : Type u#(a + 1) =
 | T : f:(a:Type u#a -> x:a -> a) -> t

Two instances of it, with identity functions at universes 0 and 1

let id (a:Type u#a) (x:a) = x
let t0 : t u#0 = T u#0 (id u#0)
let t1 : t u#1 = T u#1 (id u#1)

You can apply t1.f to t0.f

let test () =
  let id0 =
    t1.f (a:Type u#0 -> a -> a) t0.f
  in
  assert (id0 == t0.f)

But, you cannot relate t1.f to t0.f by <<.

General form of additional ordering axioms on inductives

Given mutually inductive type definitions introducing types
(t1, ..., tn), we will generate the additional axiom for
every argument of a constructor that contains a pure or ghost
function returning any one of the introduced types.

For instance, given

noeq
type t =
  | T0 : bool -> t
  | T : (nat -> s) -> t
and s =
  | S0 : bool -> s
  | S : (nat -> t) -> s

We will generate

forall (f:nat -> s). (forall (x:nat). f x << T f)
forall (f:nat -> t). (forall (x:nat). f x << S f)

Which should allow us to write the following without needing to use
WF.axiom1. In the mutually recursive calls, we are required to prove
that f y << x. With axiom1, we prove this via f y << f << x.
Whereas under the proposal here, we will directly prove f y << x
without relating it to f.

let rec neg_t (x:t) =
  match x with
  | T0 b -> T0 (not b)
  | T f -> T (fun y -> (* WF.axiom1 f y; *) neg_s (f y))

and neg_s (x:s) = 
  match x with
  | S0 b -> S0 (not b)
  | S f -> S (fun y -> (* WF.axiom1 f y; *) neg_t (f y))

Note, this flavor of inducing an ordering only between f x << T f is more in the spirit of sized types for type-based termination. See, e.g.,

@misc{Barthe02type-basedtermination,
author = {G. Barthe and M. J. Frade and E. Giménez and L. Pinto and T. Uustalu},
title = {Type-Based Termination of Recursive Definitions},
year = {2002}
}

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.4933

For a quick read, consider

• Example 2.9 and the signature of C(Ord), particularly the D(lim) case.
• Definition 2.10 for the instantiation of the type of constructor to a given "stage"
• The rule for (case) in Fig 3, where analysing a e' : d ^{\hat{s}} t (i.e., a term in stage s-hat (i.e., a stage above s), the arguments of each constructor are defined only at stage s.

See how this plays out in Example 2.18, the additional of ordinals. Notably, in the case of the limit ordinal, analyzing x:Ord^{i-hat}, the argument to the lim ordinal constructor is of type nat -> Ord^i. I.e., the co-domain of the argument of is in a smaller stage than x itself.

Rephrasing in our setting, given

type ord = 
 | Zero
 | Succ : ord -> ord
 | Lim : (nat -> ord) -> ord

For Lim f we don't have f x << f, but we do have f x << Lim f

Fixed in PR #2205