Merge pull request #445 from GaloisInc/logic-class

Introduce a `Logic` class for bitwise logical operations

lib/Cryptol.cry

@@ -100,7 +100,7 @@ primitive negate : {a} (Arith a) => a -> a
  * Bitwise complement. The prefix notation '~ x'
  * is syntactic sugar for 'complement x'.
  */
-primitive complement : {a} a -> a
+primitive complement : {a} (Logic a) => a -> a
 
 /**
  * Less-than. Only works on comparable arguments.
@@ -259,35 +259,35 @@ a ==> b = if a then b else True
 /**
  * Logical `and' over bits. Extends element-wise over sequences, tuples.
  */
-primitive (&&) : {a} a -> a -> a
+primitive (&&) : {a} (Logic a) => a -> a -> a
 
 /**
  * Logical `or' over bits. Extends element-wise over sequences, tuples.
  */
-primitive (||) : {a} a -> a -> a
+primitive (||) : {a} (Logic a) => a -> a -> a
 
 /**
  * Logical `exclusive or' over bits. Extends element-wise over sequences, tuples.
  */
-primitive (^) : {a} a -> a -> a
+primitive (^) : {a} (Logic a) => a -> a -> a
 
 /**
  * Gives an arbitrary shaped value whose bits are all False.
  * ~zero likewise gives an arbitrary shaped value whose bits are all True.
  */
-primitive zero : {a} a
+primitive zero : {a} (Zero a) => a
 
 /**
  * Left shift.  The first argument is the sequence to shift, the second is the
  * number of positions to shift by.
 */
-primitive (<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
+primitive (<<) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
 
 /**
  * Right shift.  The first argument is the sequence to shift, the second is the
  * number of positions to shift by.
  */
-primitive (>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
+primitive (>>) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
 
 /**
  * Left rotate.  The first argument is the sequence to rotate, the second is the

lib/Cryptol/Extras.cry

@@ -12,7 +12,7 @@ module Cryptol::Extras where
 /**
  * Logical negation
  */
-not : {a} a -> a
+not : {a} (Logic a) => a -> a
 not a = ~ a
 
 /**
@@ -66,7 +66,7 @@ foldr f acc xs = ys ! 0
 /**
  * Compute the sum of the words in the array.
  */
-sum : {a,n} (fin n, Arith a) => [n]a -> a
+sum : {a,n} (fin n, Zero a, Arith a) => [n]a -> a
 sum xs = foldl (+) zero xs
 
 /**
@@ -101,7 +101,7 @@ extendSigned  xs = repeat (xs @ 0) # xs
  * Repeat a value.
  */
 repeat : {n, a} a -> [n]a
-repeat x = [ x | _ <- zero ]
+repeat x = [ x | _ <- zero : [n] ]
 
 /**
  * `elem x xs` Returns true if x is equal to a value in xs.

src/Cryptol/ModuleSystem/Renamer.hs

@@ -495,6 +495,8 @@ instance Rename Prop where
     CFin t        -> CFin       <$> rename t
     CEqual l r    -> CEqual     <$> rename l  <*> rename r
     CGeq l r      -> CGeq       <$> rename l  <*> rename r
+    CZero t       -> CZero      <$> rename t
+    CLogic t      -> CLogic     <$> rename t
     CArith t      -> CArith     <$> rename t
     CCmp t        -> CCmp       <$> rename t
     CSignedCmp t  -> CSignedCmp <$> rename t

src/Cryptol/Parser/AST.hs

@@ -377,6 +377,8 @@ tconNames  = Map.fromList
 data Prop n   = CFin (Type n)             -- ^ @ fin x   @
               | CEqual (Type n) (Type n)  -- ^ @ x == 10 @
               | CGeq (Type n) (Type n)    -- ^ @ x >= 10 @
+              | CZero (Type n)            -- ^ @ Zero a  @
+              | CLogic (Type n)           -- ^ @ Logic a @
               | CArith (Type n)           -- ^ @ Arith a @
               | CCmp (Type n)             -- ^ @ Cmp a @
               | CSignedCmp (Type n)       -- ^ @ SignedCmp a @
@@ -836,6 +838,8 @@ instance PPName name => PP (Prop name) where
   ppPrec n prop =
     case prop of
       CFin t       -> text "fin"   <+> ppPrec 4 t
+      CZero t      -> text "Zero"  <+> ppPrec 4 t
+      CLogic t     -> text "Logic" <+> ppPrec 4 t
       CArith t     -> text "Arith" <+> ppPrec 4 t
       CCmp t       -> text "Cmp"   <+> ppPrec 4 t
       CSignedCmp t -> text "SignedCmp" <+> ppPrec 4 t
@@ -1000,6 +1004,8 @@ instance NoPos (Prop name) where
       CEqual  x y   -> CEqual  (noPos x) (noPos y)
       CGeq x y      -> CGeq (noPos x) (noPos y)
       CFin x        -> CFin (noPos x)
+      CZero x       -> CZero  (noPos x)
+      CLogic x      -> CLogic (noPos x)
       CArith x      -> CArith (noPos x)
       CCmp x        -> CCmp   (noPos x)
       CSignedCmp x  -> CSignedCmp (noPos x)

src/Cryptol/Parser/Names.hs

@@ -180,6 +180,8 @@ namesC vs prop =
     CFin t        -> namesT vs t
     CEqual t1 t2  -> Set.union (namesT vs t1) (namesT vs t2)
     CGeq t1 t2    -> Set.union (namesT vs t1) (namesT vs t2)
+    CZero t       -> namesT vs t
+    CLogic t      -> namesT vs t
     CArith t      -> namesT vs t
     CCmp t        -> namesT vs t
     CSignedCmp t  -> namesT vs t
@@ -283,6 +285,8 @@ tnamesC prop =
     CFin t       -> tnamesT t
     CEqual t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
     CGeq t1 t2   -> Set.union (tnamesT t1) (tnamesT t2)
+    CZero t      -> tnamesT t
+    CLogic t     -> tnamesT t
     CArith t     -> tnamesT t
     CCmp t       -> tnamesT t
     CSignedCmp t -> tnamesT t

src/Cryptol/Parser/ParserUtils.hs

@@ -436,6 +436,8 @@ mkProp ty =
 
   -- these can be translated right away
   prefixProp r f xs
+    | i == zeroIdent,      [x] <- xs = return [CLocated (CZero x) r]
+    | i == logicIdent,     [x] <- xs = return [CLocated (CLogic x) r]
     | i == arithIdent,     [x] <- xs = return [CLocated (CArith x) r]
     | i == finIdent,       [x] <- xs = return [CLocated (CFin x) r]
     | i == cmpIdent,       [x] <- xs = return [CLocated (CCmp x) r]
@@ -444,7 +446,9 @@ mkProp ty =
     where
     i = getIdent f
 
-arithIdent, finIdent, cmpIdent, signedCmpIdent :: Ident
+zeroIdent, logicIdent, arithIdent, finIdent, cmpIdent, signedCmpIdent :: Ident
+zeroIdent      = mkIdent (S.pack "Zero")
+logicIdent     = mkIdent (S.pack "Logic")
 arithIdent     = mkIdent (S.pack "Arith")
 finIdent       = mkIdent (S.pack "fin")
 cmpIdent       = mkIdent (S.pack "Cmp")

src/Cryptol/TypeCheck/Kind.hs

@@ -330,6 +330,8 @@ checkProp prop =
     P.CFin t1       -> tcon (PC PFin)           [t1]    (Just KProp)
     P.CEqual t1 t2  -> tcon (PC PEqual)         [t1,t2] (Just KProp)
     P.CGeq t1 t2    -> tcon (PC PGeq)           [t1,t2] (Just KProp)
+    P.CZero t1      -> tcon (PC PZero)          [t1]    (Just KProp)
+    P.CLogic t1     -> tcon (PC PLogic)         [t1]    (Just KProp)
     P.CArith t1     -> tcon (PC PArith)         [t1]    (Just KProp)
     P.CCmp t1       -> tcon (PC PCmp)           [t1]    (Just KProp)
     P.CSignedCmp t1 -> tcon (PC PSignedCmp)     [t1]    (Just KProp)

src/Cryptol/TypeCheck/SimpleSolver.hs

@@ -7,7 +7,8 @@ import Cryptol.TypeCheck.Type hiding
 import Cryptol.TypeCheck.Solver.Types
 import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType)
 import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
-import Cryptol.TypeCheck.Solver.Class(solveArithInst,solveCmpInst, solveSignedCmpInst)
+import Cryptol.TypeCheck.Solver.Class
+  (solveZeroInst, solveLogicInst, solveArithInst, solveCmpInst, solveSignedCmpInst)
 
 import Cryptol.Utils.Debug(ppTrace)
 import Cryptol.TypeCheck.PP
@@ -36,6 +37,8 @@ simplifyStep ctxt prop =
     TCon (PC PTrue)  []       -> SolvedIf []
     TCon (PC PAnd)   [l,r]    -> SolvedIf [l,r]
 
+    TCon (PC PZero)  [ty]     -> solveZeroInst ty
+    TCon (PC PLogic) [ty]     -> solveLogicInst ty
     TCon (PC PArith) [ty]     -> solveArithInst ty
     TCon (PC PCmp)   [ty]     -> solveCmpInst   ty
     TCon (PC PSignedCmp) [ty] -> solveSignedCmpInst ty

src/Cryptol/TypeCheck/Solver/Class.hs

@@ -11,6 +11,8 @@
 {-# LANGUAGE PatternGuards #-}
 module Cryptol.TypeCheck.Solver.Class
   ( classStep
+  , solveZeroInst
+  , solveLogicInst
   , solveArithInst
   , solveCmpInst
   , solveSignedCmpInst
@@ -22,13 +24,62 @@ import Cryptol.TypeCheck.Solver.Types
 
 -- | Solve class constraints.
 -- If not, then we return 'Nothing'.
--- If solved, ther we return 'Just' a list of sub-goals.
+-- If solved, then we return 'Just' a list of sub-goals.
 classStep :: Prop -> Solved
 classStep p = case tNoUser p of
+  TCon (PC PLogic) [ty] -> solveLogicInst (tNoUser ty)
   TCon (PC PArith) [ty] -> solveArithInst (tNoUser ty)
   TCon (PC PCmp) [ty]   -> solveCmpInst   (tNoUser ty)
   _                     -> Unsolved
 
+-- | Solve a Zero constraint by instance, if possible.
+solveZeroInst :: Type -> Solved
+solveZeroInst ty = case tNoUser ty of
+
+  -- Zero Error -> fails
+  TCon (TError _ e) _ -> Unsolvable e
+
+  -- Zero Bit
+  TCon (TC TCBit) [] -> SolvedIf []
+
+  -- Zero a => Zero [n]a
+  TCon (TC TCSeq) [_, a] -> SolvedIf [ pZero a ]
+
+  -- Zero b => Zero (a -> b)
+  TCon (TC TCFun) [_, b] -> SolvedIf [ pZero b ]
+
+  -- (Zero a, Zero b) => Zero (a,b)
+  TCon (TC (TCTuple _)) es -> SolvedIf [ pZero e | e <- es ]
+
+  -- (Zero a, Zero b) => Zero { x1 : a, x2 : b }
+  TRec fs -> SolvedIf [ pZero ety | (_,ety) <- fs ]
+
+  _ -> Unsolved
+
+-- | Solve a Logic constraint by instance, if possible.
+solveLogicInst :: Type -> Solved
+solveLogicInst ty = case tNoUser ty of
+
+  -- Logic Error -> fails
+  TCon (TError _ e) _ -> Unsolvable e
+
+  -- Logic Bit
+  TCon (TC TCBit) [] -> SolvedIf []
+
+  -- Logic a => Logic [n]a
+  TCon (TC TCSeq) [_, a] -> SolvedIf [ pLogic a ]
+
+  -- Logic b => Logic (a -> b)
+  TCon (TC TCFun) [_, b] -> SolvedIf [ pLogic b ]
+
+  -- (Logic a, Logic b) => Logic (a,b)
+  TCon (TC (TCTuple _)) es -> SolvedIf [ pLogic e | e <- es ]
+
+  -- (Logic a, Logic b) => Logic { x1 : a, x2 : b }
+  TRec fs -> SolvedIf [ pLogic ety | (_,ety) <- fs ]
+
+  _ -> Unsolved
+
 -- | Solve an Arith constraint by instance, if possible.
 solveArithInst :: Type -> Solved
 solveArithInst ty = case tNoUser ty of

src/Cryptol/TypeCheck/Type.hs

@@ -97,6 +97,8 @@ data PC     = PEqual        -- ^ @_ == _@
 
             -- classes
             | PHas Selector -- ^ @Has sel type field@ does not appear in schemas
+            | PZero         -- ^ @Zero _@
+            | PLogic        -- ^ @Logic _@
             | PArith        -- ^ @Arith _@
             | PCmp          -- ^ @Cmp _@
             | PSignedCmp    -- ^ @SignedCmp _@
@@ -188,6 +190,8 @@ instance HasKind PC where
       PGeq       -> KNum :-> KNum :-> KProp
       PFin       -> KNum :-> KProp
       PHas _     -> KType :-> KType :-> KProp
+      PZero      -> KType :-> KProp
+      PLogic     -> KType :-> KProp
       PArith     -> KType :-> KProp
       PCmp       -> KType :-> KProp
       PSignedCmp -> KType :-> KProp
@@ -398,6 +402,16 @@ pIsEq ty = case tNoUser ty of
              TCon (PC PEqual) [t1,t2] -> Just (t1,t2)
              _                        -> Nothing
 
+pIsZero :: Prop -> Maybe Type
+pIsZero ty = case tNoUser ty of
+               TCon (PC PZero) [t1] -> Just t1
+               _                    -> Nothing
+
+pIsLogic :: Prop -> Maybe Type
+pIsLogic ty = case tNoUser ty of
+                TCon (PC PLogic) [t1] -> Just t1
+                _                     -> Nothing
+
 pIsArith :: Prop -> Maybe Type
 pIsArith ty = case tNoUser ty of
                 TCon (PC PArith) [t1] -> Just t1
@@ -550,6 +564,12 @@ x =#= y = TCon (PC PEqual) [x,y]
 (=/=) :: Type -> Type -> Prop
 x =/= y = TCon (PC PNeq) [x,y]
 
+pZero :: Type -> Prop
+pZero t = TCon (PC PZero) [t]
+
+pLogic :: Type -> Prop
+pLogic t = TCon (PC PLogic) [t]
+
 pArith :: Type -> Prop
 pArith t = TCon (PC PArith) [t]
 
@@ -789,6 +809,8 @@ instance PP PC where
       PGeq       -> text "(>=)"
       PFin       -> text "fin"
       PHas sel   -> parens (ppSelector sel)
+      PZero      -> text "Zero"
+      PLogic     -> text "Logic"
       PArith     -> text "Arith"
       PCmp       -> text "Cmp"
       PSignedCmp -> text "SignedCmp"

src/Cryptol/TypeCheck/TypeOf.hs

@@ -65,10 +65,19 @@ fastSchemaOf tyenv expr =
     ETAbs tparam e -> case fastSchemaOf tyenv e of
                         Forall tparams props ty -> Forall (tparam : tparams) props ty
     ETApp e t      -> case fastSchemaOf tyenv e of
-                        Forall (tparam : tparams) props ty -> Forall tparams (apSubst s props) (apSubst s ty)
+                        Forall (tparam : tparams) props ty
-                                                                where s = singleSubst (tpVar tparam) t
+                          -> Forall tparams (map (plainSubst s) props) (apSubst s ty)
+                          where s = singleSubst (tpVar tparam) t
                         _ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
                                [ "ETApp body with no type parameters" ]
+                        -- When calling 'fastSchemaOf' on a
+                        -- polymorphic function with instantiated type
+                        -- variables but undischarged type
+                        -- constraints, we would prefer to see the
+                        -- instantiated constraints in an
+                        -- un-simplified form. Thus we use
+                        -- 'plainSubst' instead of 'apSubst' on the
+                        -- type constraints.
     EProofAbs p e  -> case fastSchemaOf tyenv e of
                         Forall [] props ty -> Forall [] (p : props) ty
                         _ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
@@ -95,6 +104,17 @@ fastSchemaOf tyenv expr =
   where
     monomorphic = Forall [] [] (fastTypeOf tyenv expr)
 
+-- | Apply a substitution to a type *without* simplifying
+-- constraints like @Arith [n]a@ to @Arith a@. (This is in contrast to
+-- 'apSubst', which performs simplifications wherever possible.)
+plainSubst :: Subst -> Type -> Type
+plainSubst s ty =
+  case ty of
+    TCon tc ts   -> TCon tc (map (plainSubst s) ts)
+    TUser f ts t -> TUser f (map (plainSubst s) ts) (plainSubst s t)
+    TRec fs      -> TRec [ (x, plainSubst s t) | (x, t) <- fs ]
+    TVar x       -> apSubst s (TVar x)
+
 -- | Yields the return type of the selector on the given argument type.
 typeSelect :: Type -> Selector -> Type
 typeSelect (TUser _ _ ty) sel = typeSelect ty sel

tests/issues/issue086.icry.stdout

@@ -1,2 +1,2 @@
 Loading module Cryptol
-(&&) : {a} a -> a -> a
+(&&) : {a} (Logic a) => a -> a -> a

tests/issues/issue226.icry.stdout

@@ -20,7 +20,7 @@ Symbols
            a} (fin front) => [front]a -> [back]a -> [front + back]a
     (%) : {a} (Arith a) => a -> a -> a
     (%$) : {a} (Arith a) => a -> a -> a
-    (&&) : {a} a -> a -> a
+    (&&) : {a} (Logic a) => a -> a -> a
     (*) : {a} (Arith a) => a -> a -> a
     (+) : {a} (Arith a) => a -> a -> a
     (-) : {a} (Arith a) => a -> a -> a
@@ -29,7 +29,7 @@ Symbols
     (/\) : Bit -> Bit -> Bit
     (<) : {a} (Cmp a) => a -> a -> Bit
     (<$) : {a} (SignedCmp a) => a -> a -> Bit
-    (<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
+    (<<) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
     (<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
     (<=) : {a} (Cmp a) => a -> a -> Bit
     (<=$) : {a} (SignedCmp a) => a -> a -> Bit
@@ -40,7 +40,7 @@ Symbols
     (>$) : {a} (SignedCmp a) => a -> a -> Bit
     (>=) : {a} (Cmp a) => a -> a -> Bit
     (>=$) : {a} (SignedCmp a) => a -> a -> Bit
-    (>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
+    (>>) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
     (>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
     (>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
     (@) : {a, b, c} (fin c) => [a]b -> [c] -> b
@@ -48,10 +48,10 @@ Symbols
     False : Bit
     True : Bit
     (\/) : Bit -> Bit -> Bit
-    (^) : {a} a -> a -> a
+    (^) : {a} (Logic a) => a -> a -> a
     (^^) : {a} (Arith a) => a -> a -> a
     carry : {n} (fin n) => [n] -> [n] -> Bit
-    complement : {a} a -> a
+    complement : {a} (Logic a) => a -> a
     demote : {val, bits} (fin val, fin bits,
                           bits >= width val) => [bits]
     drop : {front, back, elem} (fin front) => [front +
@@ -106,7 +106,7 @@ Symbols
                                fin d) => [a]b -> [d][c] -> [d]b -> [a]b
     width : {bits, len, elem} (fin len, fin bits,
                                bits >= width len) => [len]elem -> [bits]
-    zero : {a} a
+    zero : {a} (Zero a) => a
     zext : {n, m} (fin m, m >= n) => [n] -> [m]
-    (||) : {a} a -> a -> a
+    (||) : {a} (Logic a) => a -> a -> a
 

tests/issues/issue410.icry.stdout

@@ -1,6 +1,8 @@
 Loading module Cryptol
-{a, b} a == min (1 + a) a
+{a, b} (Logic b) => a == min (1 + a) a
-{a, b} True
+{a, b} (Logic b) => Logic b
+{a, b} (Logic b) => Logic b
+{a, b} (Logic b) => True
 (s
  where
    s x =
@@ -9,7 +11,7 @@ Loading module Cryptol
           bs = [complement b | b <- [complement x] # bs
                              | _ <- bs]
         )
- ) : {a, b} b -> [a]b
+ ) : {a, b} (Logic b) => b -> [a]b
 {a, b} a == a
 (bs
  where

tests/mono-binds/test05.icry.stdout

@@ -14,8 +14,8 @@ test05::foo : [10]
 test05::foo = Cryptol::demote 10 10 <> <> <>
 
 /* Not recursive */
-test05::test : {a, b, c} (c >= 4, fin c) => [a]b -> [c]
+test05::test : {a, b, c} (Zero b, c >= 4, fin c) => [a]b -> [c]
-test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
+test05::test = \{a, b, c} (Zero b, c >= 4, fin c) (a : [a]b) ->
                Cryptol::demote 10 c <> <> <>
                where
                  /* Not recursive */
@@ -34,7 +34,7 @@ test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
                                /* Not recursive */
                                test05::bar : {e} (fin e) => [e + a]b
                                test05::bar = \{e} (fin e) ->
-                                             (Cryptol::#) e a b <> (Cryptol::zero ([e]b)) test05::foo
+                                             (Cryptol::#) e a b <> (Cryptol::zero ([e]b) <>) test05::foo
                                
                              
                  
@@ -60,8 +60,8 @@ test05::foo : [10]
 test05::foo = Cryptol::demote 10 10 <> <> <>
 
 /* Not recursive */
-test05::test : {a, b, c} (c >= 4, fin c) => [a]b -> [c]
+test05::test : {a, b, c} (Zero b, c >= 4, fin c) => [a]b -> [c]
-test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
+test05::test = \{a, b, c} (Zero b, c >= 4, fin c) (a : [a]b) ->
                Cryptol::demote 10 c <> <> <>
                where
                  /* Not recursive */
@@ -78,7 +78,7 @@ test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
                                
                                /* Not recursive */
                                test05::bar : [a]b
-                               test05::bar = (Cryptol::#) 0 a b <> (Cryptol::zero ([0]b)) test05::foo
+                               test05::bar = (Cryptol::#) 0 a b <> (Cryptol::zero ([0]b) <>) test05::foo
                                
                              
                  

tests/mono-binds/test06.cry

@@ -1,6 +1,6 @@
 module test06 where
 
-test : {a} a -> a
+test : {a} (Zero a) => a -> a
 test a = bar
   where
   foo : a

tests/mono-binds/test06.icry.stdout

@@ -4,13 +4,13 @@ Loading module test06
 module test06
 import Cryptol
 /* Not recursive */
-test06::test : {a} a -> a
+test06::test : {a} (Zero a) => a -> a
-test06::test = \{a} (a : a) ->
+test06::test = \{a} (Zero a) (a : a) ->
                test06::bar
                where
                  /* Not recursive */
                  test06::foo : a
-                 test06::foo = Cryptol::zero a
+                 test06::foo = Cryptol::zero a <>
                  
                  /* Not recursive */
                  test06::bar : a
@@ -23,13 +23,13 @@ Loading module test06
 module test06
 import Cryptol
 /* Not recursive */
-test06::test : {a} a -> a
+test06::test : {a} (Zero a) => a -> a
-test06::test = \{a} (a : a) ->
+test06::test = \{a} (Zero a) (a : a) ->
                test06::bar
                where
                  /* Not recursive */
                  test06::foo : a
-                 test06::foo = Cryptol::zero a
+                 test06::foo = Cryptol::zero a <>
                  
                  /* Not recursive */
                  test06::bar : a