remove redundant constraints

examples/Snarkl/Example/Basic.hs

@@ -31,7 +31,7 @@ mult_ex ::
   Comp 'TField k
 mult_ex x y = return $ x * y
 
-arr_ex :: (GaloisField k) => TExp 'TField k -> Comp 'TField k
+arr_ex :: TExp 'TField k -> Comp 'TField k
 arr_ex x = do
   a <- arr 2
   forall [0 .. 1] (\i -> set (a, i) x)
@@ -63,13 +63,13 @@ interp2' = comp_interp p2 [256]
 compile1 :: (GaloisField k) => R1CS k
 compile1 = compileCompToR1CS Simplify p1
 
-comp1 :: (GaloisField k, Typeable a) => Comp ('TSum 'TBool a) k
+comp1 :: (Typeable a) => Comp ('TSum 'TBool a) k
 comp1 = inl false
 
 comp2 :: (GaloisField k, Typeable a) => Comp ('TSum a 'TField) k
 comp2 = inr (fromField 0)
 
-test1 :: (GaloisField k) => State (Env k) (TExp 'TBool k)
+test1 :: (GaloisField k) => Comp 'TBool k
 test1 = do
   b <- fresh_input
   z <- if return b then comp1 else comp2

examples/Snarkl/Example/Keccak.hs

@@ -35,7 +35,6 @@ ln_width :: Int
 ln_width = 32
 
 round1 ::
-  (GaloisField k) =>
   (Int -> TExp 'TBool k) ->
   -- | 'i'th bit of round constant
   TExp ('TArr ('TArr ('TArr 'TBool))) k ->
@@ -198,7 +197,7 @@ keccak_f1 num_rounds a =
     )
 
 -- num_rounds = 12+2l, where 2^l = ln_width
-keccak1 :: (GaloisField k) => Int -> Comp 'TBool k
+keccak1 :: Int -> Comp 'TBool k
 keccak1 num_rounds =
   do
     a <- input_arr3 5 5 ln_width

examples/Snarkl/Example/Lam.hs

@@ -33,7 +33,7 @@ type TFSubst = 'TFSum ('TFConst 'TField) ('TFProd ('TFConst TTerm) 'TFId)
 
 type TSubst = 'TMu TFSubst
 
-subst_nil :: (GaloisField k) => TExp 'TField k -> Comp TSubst k
+subst_nil :: TExp 'TField k -> Comp TSubst k
 subst_nil n =
   do
     n' <- inl n
@@ -66,7 +66,6 @@ type TF = 'TFSum ('TFConst 'TField) ('TFSum 'TFId ('TFProd 'TFId 'TFId))
 type TTerm = 'TMu TF
 
 varN ::
-  (GaloisField k) =>
   TExp 'TField k ->
   Comp TTerm k
 varN e =
@@ -84,7 +83,6 @@ varN' i =
     roll v
 
 lam ::
-  (GaloisField k) =>
   TExp TTerm k ->
   Comp TTerm k
 lam t =
@@ -94,7 +92,6 @@ lam t =
     roll v
 
 app ::
-  (GaloisField k) =>
   TExp TTerm k ->
   TExp TTerm k ->
   Comp TTerm k
@@ -106,9 +103,7 @@ app t1 t2 =
     roll v
 
 case_term ::
-  ( Typeable ty,
-    Zippable ty k,
-    GaloisField k
+  ( Zippable ty k
   ) =>
   TExp TTerm k ->
   (TExp 'TField k -> Comp ty k) ->
@@ -126,7 +121,7 @@ case_term t f_var f_lam f_app =
         e2 <- fst_pair p
         f_app e1 e2
 
-is_lam :: (GaloisField k) => TExp TTerm k -> Comp 'TBool k
+is_lam :: TExp TTerm k -> Comp 'TBool k
 is_lam t =
   case_term
     t

examples/Snarkl/Example/List.hs

@@ -27,12 +27,12 @@ type TList a = 'TMu (TF a)
 
 type List a k = TExp (TList a) k
 
-nil :: (Typeable a, GaloisField k) => Comp (TList a) k
+nil :: (Typeable a) => Comp (TList a) k
 nil = do
   t <- inl unit
   roll t
 
-cons :: (Typeable a, GaloisField k) => TExp a k -> List a k -> Comp (TList a) k
+cons :: (Typeable a) => TExp a k -> List a k -> Comp (TList a) k
 cons f t =
   do
     p <- pair f t
@@ -41,9 +41,7 @@ cons f t =
 
 case_list ::
   ( Typeable a,
-    Typeable ty,
-    Zippable ty k,
-    GaloisField k
+    Zippable ty k
   ) =>
   List a k ->
   Comp ty k ->
@@ -62,9 +60,7 @@ case_list t f_nil f_cons =
 
 head_list ::
   ( Typeable a,
-    Zippable a k,
-    Derive a k,
-    GaloisField k
+    Zippable a k
   ) =>
   TExp a k ->
   List a k ->
@@ -78,8 +74,7 @@ head_list def l =
 tail_list ::
   ( Typeable a,
     Zippable a k,
-    Derive a k,
-    GaloisField k
+    Derive a k
   ) =>
   List a k ->
   Comp (TList a) k
@@ -96,8 +91,7 @@ tail_list l =
 app_list ::
   ( Typeable a,
     Zippable a k,
-    Derive a k,
-    GaloisField k
+    Derive a k
   ) =>
   List a k ->
   List a k ->
@@ -116,8 +110,7 @@ app_list l1 l2 = fix go l1
 rev_list ::
   ( Typeable a,
     Zippable a k,
-    Derive a k,
-    GaloisField k
+    Derive a k
   ) =>
   List a k ->
   Comp (TList a) k
@@ -136,12 +129,9 @@ rev_list l = fix go l
 
 map_list ::
   ( Typeable a,
-    Zippable a k,
-    Derive a k,
     Typeable b,
     Zippable b k,
-    Derive b k,
-    GaloisField k
+    Derive b k
   ) =>
   (TExp a k -> Comp b k) ->
   List a k ->
@@ -161,7 +151,7 @@ map_list f l =
         )
 
 last_list ::
-  (Typeable a, Zippable a k, Derive a k, GaloisField k) =>
+  (Typeable a, Zippable a k) =>
   TExp a k ->
   List a k ->
   Comp a k

examples/Snarkl/Example/Peano.hs

@@ -22,13 +22,13 @@ type TF = 'TFSum ('TFConst 'TUnit) 'TFId
 
 type TNat = 'TMu TF
 
-nat_zero :: (GaloisField k) => Comp TNat k
+nat_zero :: Comp TNat k
 nat_zero =
   do
     x <- inl unit
     roll x
 
-nat_succ :: (GaloisField k) => TExp TNat k -> Comp TNat k
+nat_succ :: TExp TNat k -> Comp TNat k
 nat_succ n =
   do
     x <- inr n

examples/Snarkl/Example/Queue.hs

@@ -27,14 +27,14 @@ type TQueue a = 'TProd (TStack a) (TStack a)
 
 type Queue a k = TExp (TQueue a) k
 
-empty_queue :: (Typeable a, GaloisField k) => Comp (TQueue a) k
+empty_queue :: (Typeable a) => Comp (TQueue a) k
 empty_queue = do
   l <- empty_stack
   r <- empty_stack
   pair l r
 
 enqueue ::
-  (Typeable a, GaloisField k) =>
+  (Typeable a) =>
   TExp a k ->
   Queue a k ->
   Comp (TQueue a) k
@@ -45,7 +45,7 @@ enqueue v q = do
   pair l' r
 
 dequeue ::
-  (Zippable a k, Derive a k, Typeable a, GaloisField k) =>
+  (Zippable a k, Derive a k, Typeable a) =>
   Queue a k ->
   TExp a k ->
   Comp ('TProd a (TQueue a)) k
@@ -73,7 +73,7 @@ dequeue q def = do
       pair h p
 
 dequeue_rec ::
-  (Zippable a k, Derive a k, Typeable a, GaloisField k) =>
+  (Zippable a k, Derive a k, Typeable a) =>
   Queue a k ->
   TExp a k ->
   Comp ('TProd a (TQueue a)) k
@@ -113,7 +113,7 @@ is_empty q = do
     (\_ _ -> return false)
 
 last_queue ::
-  (Zippable a k, Derive a k, Typeable a, GaloisField k) =>
+  (Zippable a k, Derive a k, Typeable a) =>
   Queue a k ->
   TExp a k ->
   Comp a k

examples/Snarkl/Example/Stack.hs

@@ -28,19 +28,19 @@ type TStack a = TList a
 
 type Stack a k = TExp (TStack a) k
 
-empty_stack :: (Typeable a, GaloisField k) => Comp (TStack a) k
+empty_stack :: (Typeable a) => Comp (TStack a) k
 empty_stack = nil
 
-push_stack :: (Typeable a, GaloisField k) => TExp a k -> Stack a k -> Comp (TStack a) k
+push_stack :: (Typeable a) => TExp a k -> Stack a k -> Comp (TStack a) k
 push_stack p q = cons p q
 
-pop_stack :: (Derive a k, Zippable a k, Typeable a, GaloisField k) => Stack a k -> Comp (TStack a) k
+pop_stack :: (Derive a k, Zippable a k, Typeable a) => Stack a k -> Comp (TStack a) k
 pop_stack f = tail_list f
 
-top_stack :: (Derive a k, Zippable a k, Typeable a, GaloisField k) => TExp a k -> Stack a k -> Comp a k
+top_stack :: (Zippable a k, Typeable a) => TExp a k -> Stack a k -> Comp a k
 top_stack def e = head_list def e
 
-is_empty_stack :: (Typeable a, GaloisField k) => Stack a k -> Comp 'TBool k
+is_empty_stack :: (Typeable a) => Stack a k -> Comp 'TBool k
 is_empty_stack s =
   case_list s (return true) (\_ _ -> return false)
 

examples/Snarkl/Example/Tree.hs

@@ -27,12 +27,12 @@ type Rat k = TExp 'TField k
 
 type Tree a k = TExp (TTree a) k
 
-leaf :: (Typeable a, GaloisField k) => Comp (TTree a) k
+leaf :: (Typeable a) => Comp (TTree a) k
 leaf = do
   t <- inl unit
   roll t
 
-node :: (Typeable a, GaloisField k) => TExp a k -> Tree a k -> Tree a k -> Comp (TTree a) k
+node :: (Typeable a) => TExp a k -> Tree a k -> Tree a k -> Comp (TTree a) k
 node v t1 t2 = do
   p <- pair t1 t2
   p' <- pair v p
@@ -41,8 +41,6 @@ node v t1 t2 = do
 
 case_tree ::
   ( Typeable a,
-    GaloisField k,
-    Typeable a1,
     Zippable a1 k
   ) =>
   Tree a k ->
@@ -64,8 +62,7 @@ map_tree ::
   ( Typeable a,
     Typeable a1,
     Zippable a1 k,
-    Derive a1 k,
-    GaloisField k
+    Derive a1 k
   ) =>
   (TExp a k -> Comp a1 k) ->
   TExp (TTree a) k ->