rewrite tactic raises "Assertion failed" in infer.ml

[fblanqui]

In Stdlib.List:

opaque symbol rot_size [a] (l:𝕃 a) : π (rot (size l) l = l) ≔
begin
  assume a l; simplify; rewrite take_size l;
  rewrite @drop_size;
  reflexivity;
end;

fails with

Uncaught [File "src/core/infer.ml", line 156, characters 63-69: Assertion failed].

infer.ml:

and infer_aux : problem -> octxt -> term -> term * term * bool = fun pb c t ->
  match unfold t with
  [...]
  | Vari x ->
      let a = try Ctxt.type_of x (classic c) with Not_found -> assert false in
      (t, a, false)