Encapsulate effects in QuickCheck function arguments

base/Prelude.toml

@@ -6,7 +6,7 @@
 # Metadata                                                                   #
 ##############################################################################
 
-version = 4
+version = 5
 module-name = 'Prelude'
 library-name = 'Base'
 exported-types = [
@@ -83,6 +83,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Bool -> Prelude.Bool -> Prelude.Bool'
@@ -92,6 +93,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 ##############################################################################
 # Integer                                                                    #
@@ -112,6 +114,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer -> Prelude.Integer'
@@ -121,6 +124,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer -> Prelude.Integer'
@@ -130,6 +134,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer -> Prelude.Integer'
@@ -139,6 +144,7 @@ exported-values = [
   arity           = 2
   effects         = ['Partiality']
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer -> Prelude.Bool'
@@ -148,6 +154,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer -> Prelude.Bool'
@@ -157,6 +164,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer -> Prelude.Bool'
@@ -166,6 +174,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer -> Prelude.Bool'
@@ -175,6 +184,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer -> Prelude.Bool'
@@ -184,6 +194,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer -> Prelude.Bool'
@@ -193,6 +204,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 [[functions]]
   haskell-type    = 'Prelude.Integer -> Prelude.Integer'
@@ -202,6 +214,7 @@ exported-values = [
   arity           = 1
   effects         = []
   needs-free-args = true
+  encapsulates-effects = false
 
 ##############################################################################
 # Lists                                                                      #

base/Test/QuickCheck.toml

@@ -7,7 +7,7 @@
 # Metadata                                                                   #
 ##############################################################################
 
-version = 4
+version = 5
 module-name = 'Test.QuickCheck'
 library-name = 'Base'
 exported-types = [
@@ -45,6 +45,7 @@ exported-values = [
   arity           = 1
   effects         = []
   needs-free-args = true
+  encapsulates-effects = true
 
 ##############################################################################
 # Operators                                                                  #
@@ -58,6 +59,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = true
 
 [[functions]]
   haskell-type    = 'a -> a -> Test.QuickCheck.Property'
@@ -67,6 +69,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = true
 
 [[functions]]
   haskell-type    = 'a -> a -> Test.QuickCheck.Property'
@@ -76,6 +79,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = true
 
 [[functions]]
   haskell-type    = 'Test.QuickCheck.Property -> Test.QuickCheck.Property -> Test.QuickCheck.Property'
@@ -85,6 +89,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = true
 
 [[functions]]
   haskell-type    = 'Test.QuickCheck.Property -> Test.QuickCheck.Property -> Test.QuickCheck.Property'
@@ -94,6 +99,7 @@ exported-values = [
   arity           = 2
   effects         = []
   needs-free-args = true
+  encapsulates-effects = true
 
 ##############################################################################
 # Imported from `Prelude`                                                    #

base/coq/Free.v

@@ -1,6 +1,7 @@
 From Base Require Export Free.Class.
 From Base Require Export Free.ForFree.
 From Base Require Export Free.Induction.
+From Base Require Export Free.Instance.Identity.
 From Base Require Export Free.Malias.
 From Base Require Export Free.Monad.
 From Base Require Export Free.Tactic.ProveInd.

base/coq/Free/Class/Normalform.v

@@ -5,32 +5,37 @@
 
 From Base Require Import Free.Monad.
 
+From Base Require Import Free.Instance.Identity.
+
 Class Normalform (Shape : Type) (Pos : Shape -> Type)
-                 (A B : Type) :=
+                 (A : Type) :=
   {
+    (** The normalized return type. *)
+    nType : Type;
     (** The function is split into two parts due to termination check errors
         for recursive data types. *)
-    nf' : A -> Free Shape Pos B
+    nf' : A -> Free Shape Pos nType
   }.
 
-Definition nf {Shape : Type} {Pos : Shape -> Type} {A B : Type}
-                  `{Normalform Shape Pos A B} (n : Free Shape Pos A)
- : Free Shape Pos B
+(* Normalizes a Free value. *)
+Definition nf {Shape : Type} {Pos : Shape -> Type} {A : Type}
+                  `{Normalform Shape Pos A} (n : Free Shape Pos A)
+ : Free Shape Pos nType
 := n >>= nf'.
 
-Lemma nfImpure {Shape : Type} {Pos : Shape -> Type} {A B : Type}
-                     `{Normalform Shape Pos A B}
+Lemma nfImpure {Shape : Type} {Pos : Shape -> Type} {A : Type}
+                     `{Normalform Shape Pos A}
   : forall s (pf : _ -> Free Shape Pos A),
   nf (impure s pf) = impure s (fun p => nf (pf p)).
 Proof. trivial. Qed.
 
-Lemma nfPure {Shape : Type} {Pos : Shape -> Type} {A B : Type}
-                     `{Normalform Shape Pos A B} : forall (x : A),
+Lemma nfPure {Shape : Type} {Pos : Shape -> Type} {A : Type}
+                     `{Normalform Shape Pos A} : forall (x : A),
   nf (pure x) = nf' x.
 Proof. trivial. Qed.
 
 (* Normalform instance for functions.
    Effects inside of functions are not pulled to the root. *)
 Instance NormalformFunc (Shape : Type) (Pos : Shape -> Type) (A B : Type)
- : Normalform Shape Pos (A -> B) (A -> B) :=
+ : Normalform Shape Pos (A -> B) :=
   { nf' := pure }.