`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 https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L114

It looks like all that's happening is that QuickChick is constructing the term (@QuickChick.Show.show _ _ (@QuickChick.Generators.sampleGen _ (liftM Some a))) https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L644 https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L312-L314 https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L321-L323 https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L292-L296 then calling interp_constr on it and throwing away the evd (maybe this is what's going wrong?) https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L298-L302 and then calling type_of https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L305 https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L133-L135 https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L113-L114

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

This is blocking https://github.com/coq-community/coq-ext-lib/pull/136

[Lysxia]

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