`Sample` fails to handle polymorphism and cumulativity

[JasonGross]

This code works

From QuickChick Require Import QuickChick.
Definition a : G nat := MkGen (fun _ _ => 1).
Polymorphic Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
{ ret : forall {t : Type@{d}}, t -> m t
; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
}.
Polymorphic Definition liftM@{d c}
  {m : Type@{d} -> Type@{c}}
  {M : Monad m}
  {T U : Type@{d}} (f : T -> U) : m T -> m U :=
  fun x => bind x (fun x => ret (f x)).
#[global] Instance MonadGen : Monad G :=
  { ret A x := MkGen (fun _ _ => x)
  ; bind A B g k := MkGen (fun n r => let (r1,r2) := randomSplit r in run (k (run g n r1)) n r2) }.
Sample (liftM Some a).

But it fails if I make MonadGen Polymorphic or if I make Monad Polymorphic Cumulative.

From QuickChick Require Import QuickChick.
Definition a : G nat := MkGen (fun _ _ => 1).
Polymorphic Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
{ ret : forall {t : Type@{d}}, t -> m t
; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
}.
Polymorphic Definition liftM@{d c}
  {m : Type@{d} -> Type@{c}}
  {M : Monad m}
  {T U : Type@{d}} (f : T -> U) : m T -> m U :=
  fun x => bind x (fun x => ret (f x)).
#[global] Polymorphic Instance MonadGen : Monad G :=
  { ret A x := MkGen (fun _ _ => x)
  ; bind A B g k := MkGen (fun n r => let (r1,r2) := randomSplit r in run (k (run g n r1)) n r2) }.
Sample (liftM Some a).
(* Error: Anomaly "in Univ.repr: Universe foo.23 undefined."
Please report at http://coq.inria.fr/bugs/.
*)

From QuickChick Require Import QuickChick.
Definition a : G nat := MkGen (fun _ _ => 1).
Polymorphic Cumulative Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
{ ret : forall {t : Type@{d}}, t -> m t
; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
}.
Polymorphic Definition liftM@{d c}
  {m : Type@{d} -> Type@{c}}
  {M : Monad m}
  {T U : Type@{d}} (f : T -> U) : m T -> m U :=
  fun x => bind x (fun x => ret (f x)).
#[global] Instance MonadGen : Monad G :=
  { ret A x := MkGen (fun _ _ => x)
  ; bind A B g k := MkGen (fun n r => let (r1,r2) := randomSplit r in run (k (run g n r1)) n r2) }.
Sample (liftM Some a).
(* Error: Conversion test raised an anomaly: Anomaly "in Univ.repr: Universe foo.22 undefined."
Please report at http://coq.inria.fr/bugs/.
*)

In both cases, Set Debug "backtrace" points the finger at
Called from Typing.type_of in file "pretyping/typing.ml", line 615, characters 17-36
Called from Quickchick_plugin__QuickChick.define in file "quickChick.mlg", line 114, characters 16-40
Called from Quickchick_plugin__QuickChick.define_and_run in file "quickChick.mlg", line 135, characters 13-29

QuickChick/plugin/quickChick.mlg.cppo

Line 114 in 235f6f2

let (evd,_) = Typing.type_of env evd c in

It looks like all that's happening is that QuickChick is constructing the term (@QuickChick.Show.show _ _ (@QuickChick.Generators.sampleGen _ (liftM Some a)))

QuickChick/plugin/quickChick.mlg.cppo

Line 644 in 235f6f2

| ["Sample" constr(c)] -> {run sample [c]}

QuickChick/plugin/quickChick.mlg.cppo

Lines 312 to 314 in 235f6f2

	let run f args =
	let env = Global.env () in
	let evd = Evd.from_env env in

QuickChick/plugin/quickChick.mlg.cppo

Lines 321 to 323 in 235f6f2

	let args = List.map (fun x -> (x,None)) args in
	let c = CAst.make @@ CApp (f, args) in
	runTest c env evd

QuickChick/plugin/quickChick.mlg.cppo

Lines 292 to 296 in 235f6f2

	let runTest c env evd : unit =
	(* [c] is a constr_expr representing the test to run,
	so we first build a new constr_expr representing
	show c **)
	let c = CAst.make @@ CApp (show, [(c, None)])

then calling interp_constr on it and throwing away the evd (maybe this is what's going wrong?)

QuickChick/plugin/quickChick.mlg.cppo

Lines 298 to 302 in 235f6f2

	(* Build the kernel term from the const_expr *)
	(* Printf.printf "Before interp constr\n"; flush stdout; *)
	let (c,_evd) = interp_constr env evd c in

and then calling type_of

QuickChick/plugin/quickChick.mlg.cppo

Line 305 in 235f6f2

define_and_run c env evd

QuickChick/plugin/quickChick.mlg.cppo

Lines 133 to 135 in 235f6f2

	let define_and_run c env evd =
	(* Extract the term and its dependencies *)
	let main = define c env evd in

QuickChick/plugin/quickChick.mlg.cppo

Lines 113 to 114 in 235f6f2

	let define c env evd =
	let (evd,_) = Typing.type_of env evd c in

Presumably interp_constr is introducing some new universes here and they get incorrectly thrown away?

This is blocking rocq-community/coq-ext-lib#136

[Lysxia]

@lemonidas do you understand what's going on here?