bug fixes to vm computation + test cases.

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/success/vm_univ_poly_match.v b/test-suite/success/vm_univ_poly_match.v
new file mode 100644
index 000000000..abe6d0fe0
--- /dev/null
+++ b/test-suite/success/vm_univ_poly_match.v
@@ -0,0 +1,28 @@
+Set Dump Bytecode.
+Set Printing Universes.
+Set Printing All.
+
+Polymorphic Class Applicative@{d c} (T : Type@{d} -> Type@{c}) :=
+{ pure : forall {A : Type@{d}}, A -> T A
+ ; ap : forall {A B : Type@{d}}, T (A -> B) -> T A -> T B
+}.
+
+Universes Uo Ua.
+
+Eval compute in @pure@{Uo Ua}.
+
+Global Instance Applicative_option : Applicative@{Uo Ua} option :=
+{| pure := @Some
+ ; ap := fun _ _ f x =>
+           match f , x with
+             | Some f , Some x => Some (f x)
+             | _ , _ => None
+           end
+|}.
+
+Definition foo := ap (ap (pure plus) (pure 1)) (pure 1).
+
+Print foo.
+
+
+Eval vm_compute in foo.