Fix issue 1099

The `D_cnf` module didn't use the flag `toplevel` as it was done in `Cnf`.
This flag is important because the `Expr` AST doesn't store quantified
type variables with binders as it does for the term variable. Instead, we
use a `prenex polymorphism` approach, which means the quantified type
variables are at the top level only.

I believe this PR fixes the issue OCamlPro#1099.

src/lib/frontend/d_cnf.ml

@@ -1473,7 +1473,7 @@ let rec mk_expr
 
       | Binder ((Forall (tyvl, tvl) | Exists (tyvl, tvl)) as e, body) ->
         if tvl == []
-        then (Cache.store_tyvl tyvl; aux_mk_expr ~toplevel body)
+        then (Cache.store_tyvl tyvl; aux_mk_expr ~toplevel:false body)
         else
           let name =
             if !name_tag = 0 then name_base
@@ -1520,7 +1520,7 @@ let rec mk_expr
             end
           in
           let in_theory = decl_kind == E.Dtheory in
-          let f = aux_mk_expr ~toplevel body in
+          let f = aux_mk_expr ~toplevel:false body in
           let qbody = E.purify_form f in
           (*  All the triggers that are encoutered at this level are assumed
               to be user-defined. *)

tests/issues/1099.ae

@@ -0,0 +1,8 @@
+type 'a t
+logic p : 'a t, unit -> prop
+logic f : 'a t -> prop
+logic r : unit t
+
+axiom a : forall s:'a t. exists n:unit. p(s, n)
+
+goal g : f(r)

tests/issues/1099.expected

@@ -0,0 +1,2 @@
+
+unknown