diff --git a/src/Solcore/Frontend/Parser/SolcoreParser.y b/src/Solcore/Frontend/Parser/SolcoreParser.y
index b47241ab..8444add1 100644
--- a/src/Solcore/Frontend/Parser/SolcoreParser.y
+++ b/src/Solcore/Frontend/Parser/SolcoreParser.y
@@ -163,7 +163,7 @@ DeclList : Decl DeclList                           { $1 : $2 }
 Decl :: { ContractDecl }
 Decl : FieldDef                                    {CFieldDecl $1}
      | DataDef                                     {CDataDecl $1}
-     | Function                                    {CFunDecl $1}
+     | AnnFunction                                    {CFunDecl $1}
      | Constructor                                 {CConstrDecl $1}
 
 -- type synonym
@@ -223,6 +223,9 @@ Signatures : Signature ';' Signatures              {$1 : $3}
 Signature :: { Signature }
 Signature : SigPrefix 'function' Name '(' ParamList ')' OptRetTy {Signature (fst $1) (snd $1) $3 $5 $7}
 
+AnnSignature :: { Signature }
+AnnSignature : SigPrefix 'function' Name '(' AnnParamList ')' OptRetTy {Signature (fst $1) (snd $1) $3 $5 (maybe unitTy Just $7)}
+
 SigPrefix :: {([Ty], [Pred])}
 SigPrefix : 'forall' Tyvars '.' ConstraintList '=>' {($2, $4)}
           | 'forall' Tyvars '.'                     {($2, [])}
@@ -233,10 +236,18 @@ ParamList : Param                                  {[$1]}
           | Param  ',' ParamList                   {$1 : $3}
           | {- empty -}                            {[]}
 
+AnnParamList :: { [Param] }
+AnnParamList : AnnParam                            {[$1]}
+             | AnnParam ',' AnnParamList           {$1 : $3}
+             | {- empty -}                         {[]}
+
 Param :: { Param }
 Param : Name ':' Type                              {Typed $1 $3}
       | Name                                       {Untyped $1}
 
+AnnParam :: { Param }
+AnnParam : Name ':' Type                           {Typed $1 $3}
+
 -- instance declarations
 
 InstDef :: { Instance }
@@ -259,18 +270,22 @@ Tyvars :: {[Ty]}
 Tyvars : Name Tyvars { (TyCon $1 []) : $2}
        | {-empty-}     {[]}
 
-Functions :: { [FunDef] }
-Functions : Function Functions                     {$1 : $2}
-          | {- empty -}                            {[]}
+AnnFunctions :: { [FunDef] }
+AnnFunctions : AnnFunction AnnFunctions            {$1 : $2}
+             | {- empty -}                         {[]}
+
 
 InstBody :: {[FunDef]}
-InstBody : '{' Functions '}'                       {$2}
+InstBody : '{' AnnFunctions '}'                       {$2}
 
 -- Function declaration
 
 Function :: { FunDef }
 Function : Signature Body {FunDef $1 $2}
 
+AnnFunction :: { FunDef }
+AnnFunction : AnnSignature Body {FunDef $1 $2}
+
 OptRetTy :: { Maybe Ty }
 OptRetTy : '->' Type                               {Just $2}
          | {- empty -}                             {Nothing}
@@ -567,6 +582,9 @@ tupleExp (t1 : ts) = pairExp t1 (tupleExp ts)
 rmquotes :: String -> String
 rmquotes = read
 
+unitTy :: Maybe Ty
+unitTy = Just (TyCon (Name "()") [])
+
 parseError (Token (line, col) lexeme)
   = alexError $ "Parse error while processing lexeme: " ++ show lexeme
                 ++ "\n at line " ++ show line ++ ", column " ++ show col
diff --git a/test/Cases.hs b/test/Cases.hs
index 6bf0b2ef..cd5cc9ea 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -234,6 +234,7 @@ cases =
     , runTestForFile "yul-function-typing.solc" caseFolder
     , runTestForFile "yul-return.solc" caseFolder
     , runTestExpectingFailure "unbound-instance-var.solc" caseFolder
+    , runTestForFile "optional-return-function-contract.solc" caseFolder
     ]
  where
   caseFolder = "./test/examples/cases"
diff --git a/test/examples/cases/Add1.solc b/test/examples/cases/Add1.solc
index fe34bd94..1c88f1e9 100644
--- a/test/examples/cases/Add1.solc
+++ b/test/examples/cases/Add1.solc
@@ -1,5 +1,5 @@
 contract Add1 {
-  function main() {
+  function main() -> word {
     let res: word;
     assembly {
        res := add(40, 2)
diff --git a/test/examples/cases/Compose2.solc b/test/examples/cases/Compose2.solc
index ac36564e..762adbd1 100644
--- a/test/examples/cases/Compose2.solc
+++ b/test/examples/cases/Compose2.solc
@@ -1,17 +1,17 @@
 contract Compose {
-  function compose(f,g) {
+  forall a b c. function compose(f :(b) -> c, g :((a) -> b)) -> ((a) -> c) {
     return lam (x) {
       return f(g(x));
     } ;
   }
 
-  function id(x) { return x; }
+  forall a . function id(x : a) -> a { return x; }
 
-  function idid() { return compose(id,id); }
+  forall a . function idid() -> ((a) -> a) { return compose(id,id); }
 
   // function main() { return idid(42); }
 
-   function main() {
+   function main() -> word {
      let f = compose(id,id);
      return f(42);
    }
diff --git a/test/examples/cases/Compose3.solc b/test/examples/cases/Compose3.solc
index 9ae5ac17..825a452a 100644
--- a/test/examples/cases/Compose3.solc
+++ b/test/examples/cases/Compose3.solc
@@ -1,17 +1,17 @@
 contract Compose {
-  function compose(f,g) {
+  forall a b c . function compose(f : (b) -> c,g : (a) -> b) -> ((a) -> c){
     return lam (x) {
       return f(g(x));
     } ;
   }
 
-  function id(x) { return x; }
+  forall a . function id(x : a) -> a { return x; }
 
-  function idid() { return compose(id,id); }
+  forall a . function idid() -> ((a) -> a) { return compose(id,id); }
 
-  function apply1(f, a) { return f(a); }
+  forall a b . function apply1(f : (a) -> b , a : a) -> b { return f(a); }
 
-  function main() {
+  function main() -> word {
     return apply1(compose(id, id), 42);
   }
 }
diff --git a/test/examples/cases/CondExp.solc b/test/examples/cases/CondExp.solc
index c13afac6..52e36b54 100644
--- a/test/examples/cases/CondExp.solc
+++ b/test/examples/cases/CondExp.solc
@@ -1,8 +1,8 @@
 contract CondExp {
-   function main() {
+   function main() -> word {
      return
        if if true then false else true
        then if false then 1 else 2
        else if true then 42 else 56;
    }
-}
\ No newline at end of file
+}
diff --git a/test/examples/cases/EitherModule.solc b/test/examples/cases/EitherModule.solc
index 2b0845d8..742b2b65 100644
--- a/test/examples/cases/EitherModule.solc
+++ b/test/examples/cases/EitherModule.solc
@@ -2,7 +2,7 @@ contract EitherModule {
   data Either(a,b) = Left(a) | Right(b);
   data List(a) = Nil | Cons(a,List(a));
 
-  function lefts(xs) {
+  forall a b . function lefts(xs : List(Either(a,b))) -> List(a) {
     match xs {
     | Nil => return Nil ;
     | Cons(y,ys) =>
diff --git a/test/examples/cases/EvenOdd.solc b/test/examples/cases/EvenOdd.solc
index 28b20820..8c47fa44 100644
--- a/test/examples/cases/EvenOdd.solc
+++ b/test/examples/cases/EvenOdd.solc
@@ -2,14 +2,14 @@ contract EvenOdd {
   data Nat = Zero | Succ(Nat);
   data Bool = False | True;
 
-  function even (n) {
+  function even (n : Nat) -> Bool {
     match n {
     | Zero => return True;
     | Succ(m) => return odd(m);
     }
   }
 
-  function odd(n) {
+  function odd(n : Nat) -> Bool {
     match n {
     | Zero => return False;
     | Succ(m) => return even(m);
diff --git a/test/examples/cases/Id.solc b/test/examples/cases/Id.solc
index 918cd856..b7a8a151 100644
--- a/test/examples/cases/Id.solc
+++ b/test/examples/cases/Id.solc
@@ -1,9 +1,9 @@
-function id() {
+forall a . function id() -> ((a) -> a) {
     return lam (x) { return x; } ;
 }
 
 contract Id {
-  function main () {
+  function main () -> word {
     let f = id();
     return f(0);
   }
diff --git a/test/examples/cases/ListModule.solc b/test/examples/cases/ListModule.solc
index 59a14c10..2251565a 100644
--- a/test/examples/cases/ListModule.solc
+++ b/test/examples/cases/ListModule.solc
@@ -3,7 +3,7 @@ contract ListModule {
   data Bool = True | False;
 
 
-  function zipWith (f,xs,ys) {
+  forall a b c . function zipWith (f : (a,b) -> c,xs : List(a),ys : List(b)) -> List(c) {
     match xs, ys {
     | Nil, Nil => return Nil ;
     | Cons(x1,xs1), Cons(y1,ys1) =>
@@ -11,7 +11,7 @@ contract ListModule {
     }
   }
 
-  function foldr(f, v, xs) {
+  forall a b . function foldr(f : (a,b) -> b, v : b, xs : List(a)) -> b {
     match xs {
     | Nil => return v;
     | Cons(y,ys) =>
diff --git a/test/examples/cases/Logic.solc b/test/examples/cases/Logic.solc
index 1a5372c1..8c89e7f2 100644
--- a/test/examples/cases/Logic.solc
+++ b/test/examples/cases/Logic.solc
@@ -1,21 +1,21 @@
 contract Logic {
   data Bool = True | False;
 
-  function not (x) {
+  function not (x : Bool) -> Bool {
     match x {
     | True => return False ;
     | False => return True ;
     }
   }
 
-  function and(x, y) {
+  function and(x : Bool, y : Bool) -> Bool {
     match x, y {
     | False, _ => return False ;
     | True , _ => return y ;
     }
   }
 
-  function and1 (x, y) {
+  function and1 (x : Bool, y : Bool) -> Bool{
     match x, y {
     | False, False => return False ;
     | True , False => return False;
@@ -24,7 +24,7 @@ contract Logic {
     }
   }
 
-  function elim (f, g, x) {
+  forall a . function elim (f : a, g : a, x : Bool) -> a {
     match x {
     | True => return f;
     | False => return g;
diff --git a/test/examples/cases/MatchCall.solc b/test/examples/cases/MatchCall.solc
index b9b946a3..0d29db7c 100644
--- a/test/examples/cases/MatchCall.solc
+++ b/test/examples/cases/MatchCall.solc
@@ -1,11 +1,11 @@
 data Bool = False | True;
 
 contract MatchCall {
-  function f() {
+  function f() -> Bool {
     return True;
   }
 
-  function main() {
+  function main() -> word {
     match f() {
      | True => return 42;
     }
diff --git a/test/examples/cases/Mutuals.solc b/test/examples/cases/Mutuals.solc
index 7729d1ba..efba1b6e 100644
--- a/test/examples/cases/Mutuals.solc
+++ b/test/examples/cases/Mutuals.solc
@@ -1,8 +1,8 @@
 contract Mutual {
-   function main () {
+   function main () -> word {
       return f();
    }
-   function f () {
+   function f() -> word {
       return 42;
    }
 }
diff --git a/test/examples/cases/NegPair.solc b/test/examples/cases/NegPair.solc
index 5946b9f2..85dfe169 100644
--- a/test/examples/cases/NegPair.solc
+++ b/test/examples/cases/NegPair.solc
@@ -35,19 +35,19 @@ forall a b . a : Neg, b : Neg => instance (a,b):Neg {
 
 contract NegPair {
 
- function bnot(x) {
+ function bnot(x : B) -> B {
    match x {
      | T => return F;
      | F => return T;
    }
 }
 
- function fromB(b) {
+ function fromB(b : B) -> word {
   match b  {
     | F => return 0;
     | T => return 1;
   }
 }
 
- function main() { return  fromB(fst(Neg.neg((F,T)))); }
+ function main() -> word { return  fromB(fst(Neg.neg((F,T)))); }
 }
diff --git a/test/examples/cases/Option.solc b/test/examples/cases/Option.solc
index 49a7119d..16cd6ef7 100644
--- a/test/examples/cases/Option.solc
+++ b/test/examples/cases/Option.solc
@@ -1,7 +1,7 @@
 contract Option {
   data Option(a) = None | Some(a);
 
-  function join(mmx) {
+  forall a . function join(mmx : Option(Option(a))) -> Option(a) {
     match mmx {
     | None => return None;
     | Some(Some(x)) => return Some(x);
diff --git a/test/examples/cases/SimpleLambda.solc b/test/examples/cases/SimpleLambda.solc
index 151e9c49..e524cc51 100644
--- a/test/examples/cases/SimpleLambda.solc
+++ b/test/examples/cases/SimpleLambda.solc
@@ -7,7 +7,7 @@ function addWord(x : word, y : word) -> word {
 }
 
 contract SimpleLambda{
-  function f (z) {
+  function f (z : word) -> word {
     let n = lam (x,y) {
       return addWord(x,addWord(y,1));
     } ;
@@ -16,7 +16,7 @@ contract SimpleLambda{
     } ;
     return m(n(1,0));
   }
-  function main() {
+  function main() -> word {
     return f(40);
   }
 }
diff --git a/test/examples/cases/array.solc b/test/examples/cases/array.solc
index f720c53b..7c72da80 100644
--- a/test/examples/cases/array.solc
+++ b/test/examples/cases/array.solc
@@ -105,7 +105,7 @@ forall size elem . size : ToWord, elem:MemoryType => instance memory(array(size,
 
 contract Array {
 
-    function main() {
+    function main() -> word {
         let arr : memory(array(Succ(Succ(Succ(Succ(Zero)))), word)) = memory(42);  // = (1,2,3,4,5,6,7,8,9,10);
         IndexAccessible.set(arr, 3, 33);
 
diff --git a/test/examples/cases/const.solc b/test/examples/cases/const.solc
index 6c6ed3b2..1a47b43c 100644
--- a/test/examples/cases/const.solc
+++ b/test/examples/cases/const.solc
@@ -3,7 +3,7 @@ function const() {
 }
 
 contract Foo {
-  function main () {
+  function main () -> word {
     let f = const();
     return f(0,1);
   }
diff --git a/test/examples/cases/import-std.solc b/test/examples/cases/import-std.solc
index 5e4a5771..914e42f8 100644
--- a/test/examples/cases/import-std.solc
+++ b/test/examples/cases/import-std.solc
@@ -1,7 +1,7 @@
 import std;
 
 contract Test {
-  function main() {
+  function main() -> word {
     return Add.add(21, 21);
   }
-}
\ No newline at end of file
+}
diff --git a/test/examples/cases/join.solc b/test/examples/cases/join.solc
index 3a20daa9..b5aa032b 100644
--- a/test/examples/cases/join.solc
+++ b/test/examples/cases/join.solc
@@ -2,14 +2,14 @@ contract Option {
   data Option(a) = None | Some(a);
   data Bool = False | True;
 
-  function maybe(n, o) {
-    match o {
-      | None => return n;
+  forall a . function maybe(n : Option(a), o : a) -> a {
+    match n  {
+      | None => return o;
       | Some(x) => return x;
     }
   }
 
-  function join(mmx) {
+  forall a . function join(mmx : Option(Option(a))) -> Option(a) {
     let result = None;
     match mmx {
       | Some(Some(x)) => result = Some(x);
@@ -18,7 +18,7 @@ contract Option {
     return result;
   }
 
-  function main() {
-    return maybe(0, join(Some(Some(0))));
+  function main() -> word {
+    return maybe(join(Some(Some(0))), 0);
   }
 }
diff --git a/test/examples/cases/modifier.solc b/test/examples/cases/modifier.solc
index 96e56b46..c8f2ff39 100644
--- a/test/examples/cases/modifier.solc
+++ b/test/examples/cases/modifier.solc
@@ -1,5 +1,5 @@
 contract C {
-	function modifier(f) {
+	forall a b c. function modifier(f : (a,b) -> c) -> ((a,b) -> c){
 		return lam (x, y) {
 			// before solidity placeholder
 			let result = f(x,y); // Solidity's placeholder: _;
@@ -16,7 +16,7 @@ contract C {
 		return r;
 	}
 
-	function main() {
+	function main() -> word {
 		//function g(x, y) modifier(x,y) {
 		//	return add(x,y);
 		//}
diff --git a/test/examples/cases/option2.solc b/test/examples/cases/option2.solc
index 76c9af45..052f6b4f 100644
--- a/test/examples/cases/option2.solc
+++ b/test/examples/cases/option2.solc
@@ -1,16 +1,16 @@
 contract Option {
   data Option(a) = None | Some(a);
 
-  function just(x) { return Some(x); }
+  forall a . function just(x : a) -> Option (a){ return Some(x); }
 
-  function maybe(n, o) {
+  forall a . function maybe(n : a, o : Option(a)) -> a {
     match o {
       | None => return n;
       | Some(x) => return x;
     }
   }
 
-  function join(mmx) {
+  forall a . function join(mmx : Option(Option(a))) -> Option(a) {
     match mmx {
       | None => return None;
       | Some(None) => return None;
@@ -18,7 +18,7 @@ contract Option {
     }
   }
 
-  function join2(mmx) {
+  forall a . function join2(mmx : Option(Option(a))) -> Option(a) {
     match mmx {
       | Some(m) => match m {
           | None => return None;
@@ -28,7 +28,7 @@ contract Option {
     }
   }
 
-  function main() {
+  function main() -> word {
    //  return maybe(0, join(Some(Some(42))));
    return 42;
   }
diff --git a/test/examples/cases/optional-return-function-contract.solc b/test/examples/cases/optional-return-function-contract.solc
new file mode 100644
index 00000000..f9dea838
--- /dev/null
+++ b/test/examples/cases/optional-return-function-contract.solc
@@ -0,0 +1,6 @@
+contract Foo {
+
+  function foo (x : word) {
+
+  }
+}
diff --git a/test/examples/cases/reference-encoding-good.solc b/test/examples/cases/reference-encoding-good.solc
index 15a1c11c..cd9ff7f5 100644
--- a/test/examples/cases/reference-encoding-good.solc
+++ b/test/examples/cases/reference-encoding-good.solc
@@ -227,7 +227,7 @@ function g() {
     Assign.assign(LValueMemberAccess.memberAccess(MemberAccessProxy(s, z_sel)), RValueMemberAccess.memberAccess(MemberAccessProxy(s, x_sel)));
 }
 contract C {
-    function main() {
+    function main() -> () {
         f();
         g();
     }
diff --git a/test/examples/cases/reference-encoding-good1.solc b/test/examples/cases/reference-encoding-good1.solc
index 14011a02..5a6b77d9 100644
--- a/test/examples/cases/reference-encoding-good1.solc
+++ b/test/examples/cases/reference-encoding-good1.solc
@@ -228,7 +228,7 @@ function g() {
     Assign.assign(LValueMemberAccess.memberAccess(MemberAccessProxy(s, z_sel)), RValueMemberAccess.memberAccess(MemberAccessProxy(s, x_sel)));
 }
 contract C {
-    function main() {
+    function main() -> () {
         f();
         g();
     }
diff --git a/test/examples/cases/tiamat.solc b/test/examples/cases/tiamat.solc
index 31747f88..36571199 100644
--- a/test/examples/cases/tiamat.solc
+++ b/test/examples/cases/tiamat.solc
@@ -127,7 +127,7 @@ instance storage(a):Assign(a) {
 }
 
 contract Tiamat {
-  function main() {
+  function main() -> word {
     let allowances : storage(dict(address, dict(address, word)));
     let src = address(17);
     setAllowance(allowances, address(1),address(2), 666);
diff --git a/test/examples/cases/tuple-trick.solc b/test/examples/cases/tuple-trick.solc
index 09367079..30528b98 100644
--- a/test/examples/cases/tuple-trick.solc
+++ b/test/examples/cases/tuple-trick.solc
@@ -27,10 +27,10 @@ forall n a b c . n : Nth (b,c) => instance Succ(n) : Nth ((a,b), c) {
 }
 
 contract C {
-  function id (x) {
+  forall a . function id (x : a) -> a {
     return x;
   }
-  function main () {
+  function main () -> () {
     let p : (word, word, word, ());
     let x : word = Nth.nth(Proxy : Proxy(Zero), p);
     let y : word = Nth.nth(Proxy : Proxy(Succ(Zero)), p);
diff --git a/test/examples/cases/uintdesugared.solc b/test/examples/cases/uintdesugared.solc
index 0439ab6a..a378094d 100644
--- a/test/examples/cases/uintdesugared.solc
+++ b/test/examples/cases/uintdesugared.solc
@@ -9,12 +9,12 @@ contract Uint {
   totalSupply : uint;
   balances : mapping(address,uint);
 
-  function mint(amount:uint) {
+  function mint(amount:uint) -> () {
     balances[owner] = Num.add(balances[owner], amount);
     totalSupply = Num.add(totalSupply, amount);
   }
 
-  function init() {
+  function init() -> () {
     owner = address(0x123456789abcdef);
     decimals = Num.fromWord(18);
   }
@@ -494,11 +494,11 @@ data balances_sel = balances_sel  ;
 instance StructField(ContractStorage(UintCxt), balances_sel) : StructField (mapping(address, uint), (word, (address, (uint, (uint, ()))))) {
 }
 contract Uint {
-   function mint (amount : uint) {
+   function mint (amount : uint) -> (){
       Assign.assign(LValueMemberAccess.memberAccess(IndexAccessProxy(LValueMemberAccess.memberAccess(MemberAccessProxy(ContractStorage(UintCxt), balances_sel)), rval(MemberAccessProxy(ContractStorage(UintCxt), owner_sel)))), Num.add(rval(IndexAccessProxy(LValueMemberAccess.memberAccess(MemberAccessProxy(ContractStorage(UintCxt), balances_sel)), rval(MemberAccessProxy(ContractStorage(UintCxt), owner_sel)))), amount));
       Assign.assign(LValueMemberAccess.memberAccess(MemberAccessProxy(ContractStorage(UintCxt), totalSupply_sel)), Num.add(rval(MemberAccessProxy(ContractStorage(UintCxt), totalSupply_sel)), amount));
    }
-   function init () {
+   function init () -> () {
       Assign.assign(LValueMemberAccess.memberAccess(MemberAccessProxy(ContractStorage(UintCxt), owner_sel)), address(81985529216486895));
       Assign.assign(LValueMemberAccess.memberAccess(MemberAccessProxy(ContractStorage(UintCxt), decimals_sel)), Num.fromWord(18));
    }
diff --git a/test/examples/cases/undefined.solc b/test/examples/cases/undefined.solc
index 00943b81..cabcf58a 100644
--- a/test/examples/cases/undefined.solc
+++ b/test/examples/cases/undefined.solc
@@ -7,7 +7,7 @@ forall any.function undefined() -> any {
 function useWord(w:word) {}
 
 contract Magic {
-  function main() {
+  function main() -> () {
     useWord(undefined());
   }
 }
diff --git a/test/examples/cases/unit.solc b/test/examples/cases/unit.solc
index a697c1b8..4034527a 100644
--- a/test/examples/cases/unit.solc
+++ b/test/examples/cases/unit.solc
@@ -1,25 +1,25 @@
 contract Unit {
-function one (x : ()) {
-  return 1;
-}
+  function one (x : ()) -> word {
+    return 1;
+  }
 
-function unitVal() {
-  return ();
-}
+  function unitVal() -> () {
+    return ();
+  }
 
-function unitMatch (x) {
-  match x {
-  | () => return 1;
+  function unitMatch (x : ()) -> word {
+    match x {
+    | () => return 1;
+    }
   }
-}
 
-function foo (x : word) {
-  return ();
-}
+  function foo (x : word) -> () {
+    return ();
+  }
 
-function main() {
-  return unitMatch(foo(one(unitVal())));
-}
+  function main() -> word {
+    return unitMatch(foo(one(unitVal())));
+  }
 }
 
 forall a . class a : Def {
diff --git a/test/examples/spec/00answer.solc b/test/examples/spec/00answer.solc
index f7112655..6a754ee4 100644
--- a/test/examples/spec/00answer.solc
+++ b/test/examples/spec/00answer.solc
@@ -1,5 +1,5 @@
 contract Answer {
-  function main() {
+  function main() -> word {
     return 42;
   }
-}
\ No newline at end of file
+}
diff --git a/test/examples/spec/010answer.solc b/test/examples/spec/010answer.solc
index f7112655..736ced85 100644
--- a/test/examples/spec/010answer.solc
+++ b/test/examples/spec/010answer.solc
@@ -1,5 +1,5 @@
 contract Answer {
-  function main() {
+  function main()  -> word {
     return 42;
   }
-}
\ No newline at end of file
+}
diff --git a/test/examples/spec/011id.solc b/test/examples/spec/011id.solc
index a4ecc489..cd7a0ebc 100644
--- a/test/examples/spec/011id.solc
+++ b/test/examples/spec/011id.solc
@@ -2,13 +2,13 @@ contract Id1 {
 
   data Bool = False | True;
 
-  function id(x) {
+  forall a . function id(x : a) -> a {
     return x ;
   }
 
-  function const(x, y) { return x; }
+  forall a b . function const(x : a, y : b) -> a { return x; }
 
-  function main() {
+  function main() -> word {
     return const(id(42), False);
   }
 }
diff --git a/test/examples/spec/012nid.solc b/test/examples/spec/012nid.solc
index 16b629fb..7414313a 100644
--- a/test/examples/spec/012nid.solc
+++ b/test/examples/spec/012nid.solc
@@ -1,15 +1,15 @@
 contract Id1 {
-  function id(x) {
+  forall a . function id(x : a) -> a {
     return x ;
   }
 
-  function nid() {
+  forall a . function nid() -> ((a) -> a) {
     return id;
   }
 
-  function const(x, y) { return x; }
+  forall a b . function const(x : a, y : b) -> a { return x; }
 
-  function main() {
+  function main() -> word {
     return const(nid(42), id(1));
   }
 }
diff --git a/test/examples/spec/013comp.solc b/test/examples/spec/013comp.solc
index 2ce169c2..0e445edc 100644
--- a/test/examples/spec/013comp.solc
+++ b/test/examples/spec/013comp.solc
@@ -1,16 +1,16 @@
 contract Compose {
-  function compose(f,g) {
+  forall a b c . function compose(f : (b) -> c,g : (a) -> b) -> ((a) -> c){
     return lam (x) {
       return f(g(x));
     } ;
   }
 
-  function id(x) { return x; }
+  forall a . function id(x : a) -> a { return x; }
 
-  function idid() { return compose(id,id); }
+  forall a . function idid() -> ((a) -> a) { return compose(id,id); }
 
-  function main() {
+  function main() -> word {
     let f = compose(id,id);
     return f(42);
   }
-}
\ No newline at end of file
+}
diff --git a/test/examples/spec/01id.solc b/test/examples/spec/01id.solc
index a4ecc489..cd7a0ebc 100644
--- a/test/examples/spec/01id.solc
+++ b/test/examples/spec/01id.solc
@@ -2,13 +2,13 @@ contract Id1 {
 
   data Bool = False | True;
 
-  function id(x) {
+  forall a . function id(x : a) -> a {
     return x ;
   }
 
-  function const(x, y) { return x; }
+  forall a b . function const(x : a, y : b) -> a { return x; }
 
-  function main() {
+  function main() -> word {
     return const(id(42), False);
   }
 }
diff --git a/test/examples/spec/021not.solc b/test/examples/spec/021not.solc
index 053e9a6a..23a51f7d 100644
--- a/test/examples/spec/021not.solc
+++ b/test/examples/spec/021not.solc
@@ -1,18 +1,18 @@
 contract Not {
   data Bool = False | True;
 
-  function main() {
+  function main() -> word {
     return fromBool(bnot(False));
   }
 
-  function fromBool(b) {
+  function fromBool(b : Bool) -> word {
     match(b) {
       | False => return 0;
       | True  => return 1;
     }
   }
 
-  function bnot(b) {
+  function bnot(b : Bool) -> Bool {
     match b {
       | False => return True;
       | True => return False;
diff --git a/test/examples/spec/022add.solc b/test/examples/spec/022add.solc
index 202a0821..ef42a390 100644
--- a/test/examples/spec/022add.solc
+++ b/test/examples/spec/022add.solc
@@ -7,7 +7,7 @@ function add(x : word, y : word) {
 }
 
 contract Add1 {
-  function main() {
+  function main() -> word {
     return add(40, 2);
   }
 }
diff --git a/test/examples/spec/024arith.solc b/test/examples/spec/024arith.solc
index d462064c..ef42623f 100644
--- a/test/examples/spec/024arith.solc
+++ b/test/examples/spec/024arith.solc
@@ -58,7 +58,7 @@ function exp(x : word, y: word) {
 
 
 contract Arith {
-  function main() {
+  function main() -> word {
     return add(mod(sub(div(exp(2,18),4), 1), 16), 27);
   }
 }
diff --git a/test/examples/spec/027sstore.solc b/test/examples/spec/027sstore.solc
index b1006dfc..1f36efb6 100644
--- a/test/examples/spec/027sstore.solc
+++ b/test/examples/spec/027sstore.solc
@@ -1,10 +1,10 @@
 contract Sstore {
-  function main() {
+  function main() -> word {
     let res : word;
     assembly {
-	sstore(0, 42)
-	res := sload(0)
+      sstore(0, 42)
+      res := sload(0)
     }
     return res;
   }
-}
\ No newline at end of file
+}
diff --git a/test/examples/spec/02nid.solc b/test/examples/spec/02nid.solc
index d4633bbf..64e30616 100644
--- a/test/examples/spec/02nid.solc
+++ b/test/examples/spec/02nid.solc
@@ -1,15 +1,15 @@
 contract Id1 {
-  function id(x) {
+  forall a . function id(x : a) -> a {
     return x ;
   }
 
-  function nid() {
+  forall a . function nid() -> ((a) -> a) {
     return id;
   }
 
-  function const(x, y) { return x; }
+  forall a b . function const(x : a, y : b) -> a { return x; }
 
-  function main() {
+  function main() -> word {
     let f = nid();
     return const(f(42), id(1));
   }
diff --git a/test/examples/spec/031maybe.solc b/test/examples/spec/031maybe.solc
index ff7f679e..8841a555 100644
--- a/test/examples/spec/031maybe.solc
+++ b/test/examples/spec/031maybe.solc
@@ -1,16 +1,16 @@
 contract Option {
   data Option(a) = None | Some(a);
 
-  function just(x) { return Some(x); }
+  forall a . function just(x : a) -> Option(a){ return Some(x); }
 
-  function maybe(n, o) {
+  forall a . function maybe(n : a, o : Option(a)) -> a {
     match o {
       | None => return n;
       | Some(x) => return x;
     }
   }
 
-  function main() {
+  function main() -> word {
     return maybe(0, Some(42));
   }
 }
diff --git a/test/examples/spec/032simplejoin.solc b/test/examples/spec/032simplejoin.solc
index 47d17cf7..d627ec5a 100644
--- a/test/examples/spec/032simplejoin.solc
+++ b/test/examples/spec/032simplejoin.solc
@@ -1,9 +1,9 @@
 contract Option {
   data Option(a) = None | Some(a);
 
-  function just(x) { return Some(x); }
+  forall a . function just(x : a) -> Option(a) { return Some(x); }
 
-  function maybe(n, o) {
+  forall a . function maybe(n : a, o : Option(a)) -> a {
     match o {
       | None => return n;
       | Some(x) => return x;
@@ -11,7 +11,7 @@ contract Option {
   }
 
 
-  function join(mmx) {
+  forall a . function join(mmx : Option(Option(a))) -> Option(a) {
     match mmx {
       | None => return None;
       | Some(None) => return None;
@@ -19,7 +19,7 @@ contract Option {
     }
   }
 
-  function join2(mmx) {
+  forall a . function join2(mmx : Option(Option(a))) -> Option(a) {
     match mmx {
       | Some(m) => match m {
           | None => return None;
@@ -29,7 +29,7 @@ contract Option {
     }
   }
 
-  function main() {
+  function main() -> word {
     return maybe(0, join(Some(Some(42))));
   }
 }
diff --git a/test/examples/spec/033join.solc b/test/examples/spec/033join.solc
index a78be8a5..11aa0d75 100644
--- a/test/examples/spec/033join.solc
+++ b/test/examples/spec/033join.solc
@@ -1,23 +1,23 @@
 contract Option {
   data Option(a) = None | Some(a);
 
-  function just(x) { return Some(x); }
+  forall a . function just(x : a) -> Option(a) { return Some(x); }
 
-  function maybe(n, o) {
+  forall a . function maybe(n : a, o : Option(a)) -> a {
     match o {
       | None => return n;
       | Some(x) => return x;
     }
   }
 
-  function join(mmx) {
+  forall a . function join(mmx : Option(Option(a))) -> Option(a) {
     match mmx {
       | Some(Some(x)) => return Some(x);
       | _ => return None;
     }
   }
 
-  function main() {
+  function main() -> word {
     return maybe(0, join(Some(Some(42))));
   }
 }
diff --git a/test/examples/spec/034cojoin.solc b/test/examples/spec/034cojoin.solc
index c77f07f9..3a6b7d9f 100644
--- a/test/examples/spec/034cojoin.solc
+++ b/test/examples/spec/034cojoin.solc
@@ -1,16 +1,16 @@
 contract Option {
   data Option(a) = None | Some(a);
 
-  function just(x) { return Some(x); }
+  forall a . function just(x : a) -> Option(a){ return Some(x); }
 
-  function maybe(n, o) {
+  forall a . function maybe(n : a, o : Option(a)) -> a {
     match o {
       | None => return n;
       | Some(x) => return x;
     }
   }
 
-  function join(mmx) {
+  forall a . function join(mmx : Option(Option(a))) -> Option(a) {
     let result = None;
     match mmx {
       | Some(Some(x)) => result = Some(x);
@@ -19,20 +19,20 @@ contract Option {
     return result;
   }
 
- function extract(mx) {
+ forall a . function extract(mx : Option(a)) -> a {
    match mx {
      | Some(x) => return x;
    }
  }
 
-  function cojoin(x) { // Test that sum types can grow
+ forall a . function cojoin(x : a) -> Option(a) { // Test that sum types can grow
     let result = None;
     result = Some(x);
     return result;
    }
 
 
-  function main() {
+  function main() -> word {
     return maybe(0, join(cojoin(Some(42))));
   }
 }
diff --git a/test/examples/spec/035padding.solc b/test/examples/spec/035padding.solc
index 568c8aae..0c1d577d 100644
--- a/test/examples/spec/035padding.solc
+++ b/test/examples/spec/035padding.solc
@@ -1,14 +1,14 @@
 contract Option {
   data Option(a) = None | Some(a);
 
-  function maybe(n, o) {
+  forall a . function maybe(n : a, o : Option(a)) -> a {
     match o {
       | Some(x) => return x;
       | None => return n;
     }
   }
 
-  function main() {
+  function main() -> word {
     return maybe(7, None);
   }
 }
diff --git a/test/examples/spec/036wildcard.solc b/test/examples/spec/036wildcard.solc
index 38de9ba5..00d6fc7a 100644
--- a/test/examples/spec/036wildcard.solc
+++ b/test/examples/spec/036wildcard.solc
@@ -1,14 +1,14 @@
 contract Option {
   data Option(a) = None | Some(a);
 
-  function maybe(n, o) {
+  forall a . function maybe(n : a, o : Option(a)) -> a {
     match o {
       | Some(x) => return x;
       | _ => return n;
     }
   }
 
-  function main() {
+  function main() -> word {
     return maybe(7, None);
   }
 }
diff --git a/test/examples/spec/037dwarves.solc b/test/examples/spec/037dwarves.solc
index 8c12d410..04723a81 100644
--- a/test/examples/spec/037dwarves.solc
+++ b/test/examples/spec/037dwarves.solc
@@ -2,7 +2,7 @@ contract Dwarves {
   data Dwarf = Doc | Grumpy | Sleepy | Bashful | Happy | Sneezy | Dopey;
 
 
-  function fromEnum(c) {
+  function fromEnum(c : Dwarf) -> word {
     match c {
       | Doc      => return 1;
       | Grumpy   => return 2;
@@ -12,5 +12,5 @@ contract Dwarves {
     }
   }
 
-  function main() { return fromEnum(Happy); }
+  function main() -> word { return fromEnum(Happy); }
 }
diff --git a/test/examples/spec/038food0.solc b/test/examples/spec/038food0.solc
index a3340676..613a723c 100644
--- a/test/examples/spec/038food0.solc
+++ b/test/examples/spec/038food0.solc
@@ -13,11 +13,11 @@ data CFood = Red(Food) | Green(Food) | Nocolor;
 
 
 contract Food {
-  function id(x) {
+  forall a . function id(x : a) -> a {
     return(x);
   }
 
-  function main() {
+  function main() -> word {
   return fromEnum(id(Green(Beans)));
   }
 }
diff --git a/test/examples/spec/039food.solc b/test/examples/spec/039food.solc
index 225a9bd5..e530b3ca 100644
--- a/test/examples/spec/039food.solc
+++ b/test/examples/spec/039food.solc
@@ -15,7 +15,7 @@ data CFood = Red(Food) | Green(Food) | Nocolor;
 
 
 contract Food {
-  function eat(x) {
+  function eat(x : CFood) -> Food {
     match x {
        | Red(f) => return f;
        | Green(f) => return f;
@@ -23,7 +23,7 @@ contract Food {
     }
   }
 
-  function main() {
+  function main() -> word {
   return fromEnum(eat(Green(Beans)));
   }
 }
diff --git a/test/examples/spec/041pair.solc b/test/examples/spec/041pair.solc
index 41a414bc..d8c4737c 100644
--- a/test/examples/spec/041pair.solc
+++ b/test/examples/spec/041pair.solc
@@ -1,12 +1,12 @@
 contract Pair {
 
-  function fst(p) {
+  forall a b . function fst(p : (a,b)) -> a {
     match p {
       | (a,b) => return a;
     }
   }
 
-  function main() {
+  function main() -> word {
     return fst((1,0));
   }
 }
diff --git a/test/examples/spec/042triple.solc b/test/examples/spec/042triple.solc
index a15ba502..a37412eb 100644
--- a/test/examples/spec/042triple.solc
+++ b/test/examples/spec/042triple.solc
@@ -1,12 +1,12 @@
 contract Triple {
 
-  function asel(t) {
+  forall a b c . function asel(t : (a,b,c)) -> c {
     match t {
       | (a,b,c) => return c;
     }
   }
 
-  function main() {
+  function main() -> word {
     return asel((1,21,42));
   }
 }
diff --git a/test/examples/spec/043fstsnd.solc b/test/examples/spec/043fstsnd.solc
index a4074b23..8a3f1eb2 100644
--- a/test/examples/spec/043fstsnd.solc
+++ b/test/examples/spec/043fstsnd.solc
@@ -29,5 +29,5 @@ function addPair(p) {
 }
 
 contract FstSnd {
- function main() { return  addPair(Pair(41,1)); }
+ function main() -> word { return  addPair(Pair(41,1)); }
 }
diff --git a/test/examples/spec/047rgb.solc b/test/examples/spec/047rgb.solc
index f54e427b..f98833ea 100644
--- a/test/examples/spec/047rgb.solc
+++ b/test/examples/spec/047rgb.solc
@@ -1,6 +1,6 @@
 contract RGB {
   data Color = R | G | B;
-  function main() {
+  function main() -> word {
     match B {
       | R => return 4;
       | G => return 2;
diff --git a/test/examples/spec/048rgb2.solc b/test/examples/spec/048rgb2.solc
index c75b4880..afc995bd 100644
--- a/test/examples/spec/048rgb2.solc
+++ b/test/examples/spec/048rgb2.solc
@@ -1,7 +1,7 @@
 contract RGB {
   data Color = R | G | B;
 
-  function fromEnum(c) {
+  function fromEnum(c : Color) -> word {
     match c {
       | R => return 4;
       | G => return 2;
@@ -9,5 +9,5 @@ contract RGB {
     }
   }
 
-  function main() { return fromEnum(B); }
+  function main() -> word { return fromEnum(B); }
 }
diff --git a/test/examples/spec/051expreturn.solc b/test/examples/spec/051expreturn.solc
index 502a5d70..2921c530 100644
--- a/test/examples/spec/051expreturn.solc
+++ b/test/examples/spec/051expreturn.solc
@@ -1,5 +1,5 @@
 data Bool = False | True;
-data W = W(Word);
+data W = W(word);
 data U = U;
 
 // empty class needed since forall expects a nonempty context
@@ -19,7 +19,7 @@ forall a . function ereturn(x:a) -> Unit { let res: Unit; return res; }
 /* simulate match expression
   x = match { | False => return 77; | True => W(22) }
 */
-function elimBool1(b:Bool) -> Word {
+function elimBool1(b:Bool) -> word {
    let x : W;
    x = W(1);
    match b {
@@ -50,7 +50,7 @@ forall a b. function unsafeCast(x:a) -> b {
 
 
 contract ExpReturn {
-  function main() -> Word {
+  function main() -> word {
     return elimBool1(False);
     // return elimBool1(False);
   }
diff --git a/test/examples/spec/051negBool.solc b/test/examples/spec/051negBool.solc
index 26319342..5ad8cdd9 100644
--- a/test/examples/spec/051negBool.solc
+++ b/test/examples/spec/051negBool.solc
@@ -18,12 +18,12 @@ instance B : Neg {
 
 contract NegBool {
 
-  function fromB(b) {
+  function fromB(b : B) -> word {
     match b  {
     | F => return 0;
     | T => return 1;
     }
   }
 
-  function main() { return  fromB(Neg.neg(F)); }
+  function main() -> word { return  fromB(Neg.neg(F)); }
 }
diff --git a/test/examples/spec/052negPair.solc b/test/examples/spec/052negPair.solc
index 3d3542d0..edae8fce 100644
--- a/test/examples/spec/052negPair.solc
+++ b/test/examples/spec/052negPair.solc
@@ -45,19 +45,19 @@ instance (a:Neg,b:Neg) => Pair(a,b):Neg {
 */
 contract NegPair {
 
- function bnot(x) {
+ function bnot(x : B) -> B{
    match x {
      | T => return F;
      | F => return T;
    }
 }
 
- function fromB(b) {
+ function fromB(b : B) -> word {
   match b  {
     | F => return 0;
     | T => return 1;
   }
 }
 
- function main() { return  fromB(fst(Neg.neg(Pair(F,T)))); }
+ function main() -> word { return  fromB(fst(Neg.neg(Pair(F,T)))); }
 }
diff --git a/test/examples/spec/06comp.solc b/test/examples/spec/06comp.solc
index a74b3728..66d40e31 100644
--- a/test/examples/spec/06comp.solc
+++ b/test/examples/spec/06comp.solc
@@ -1,20 +1,20 @@
 contract Compose {
-  function compose(f,g) {
+  forall a b c . function compose(f : (b) -> c,g : (a) -> b) -> ((a) -> c) {
     return lam (x) {
       return f(g(x));
     } ;
   }
 
-  function id(x) { return x; }
+  forall a . function id(x : a) -> a { return x; }
 
-  function idid() { return compose(id,id); }
+  forall a . function idid() -> ((a) -> a){ return compose(id,id); }
 
-  function foo() {
+  function foo() -> word {
     let f = idid();
     return f(42);
   }
 
-  function main() {
+  function main() -> word {
     let f = compose(id,id);
     return f(42);
   }
diff --git a/test/examples/spec/09not.solc b/test/examples/spec/09not.solc
index 053e9a6a..23a51f7d 100644
--- a/test/examples/spec/09not.solc
+++ b/test/examples/spec/09not.solc
@@ -1,18 +1,18 @@
 contract Not {
   data Bool = False | True;
 
-  function main() {
+  function main() -> word {
     return fromBool(bnot(False));
   }
 
-  function fromBool(b) {
+  function fromBool(b : Bool) -> word {
     match(b) {
       | False => return 0;
       | True  => return 1;
     }
   }
 
-  function bnot(b) {
+  function bnot(b : Bool) -> Bool {
     match b {
       | False => return True;
       | True => return False;
diff --git a/test/examples/spec/101struct1Field.solc b/test/examples/spec/101struct1Field.solc
index 9e634bb4..f418cea5 100644
--- a/test/examples/spec/101struct1Field.solc
+++ b/test/examples/spec/101struct1Field.solc
@@ -247,7 +247,7 @@ function g() -> word {
 }
 
 contract C {
-    function main() {
+    function main() -> word {
         f();
         return g();
     }
diff --git a/test/examples/spec/102uintField.solc b/test/examples/spec/102uintField.solc
index 89a01289..80317575 100644
--- a/test/examples/spec/102uintField.solc
+++ b/test/examples/spec/102uintField.solc
@@ -254,7 +254,7 @@ function g() -> word {
 }
 
 contract C {
-    function main() {
+    function main() -> word {
         f();
         return g();
     }
diff --git a/test/examples/spec/103struct3Fields.solc b/test/examples/spec/103struct3Fields.solc
index fd2b8af5..8b2c93a0 100644
--- a/test/examples/spec/103struct3Fields.solc
+++ b/test/examples/spec/103struct3Fields.solc
@@ -278,7 +278,7 @@ function g() -> word {
 }
 
 contract C {
-    function main() {
+    function main() -> word {
         return g();
     }
 }
diff --git a/test/examples/spec/105nestedStruct.solc b/test/examples/spec/105nestedStruct.solc
index 6e36ed10..63438a24 100644
--- a/test/examples/spec/105nestedStruct.solc
+++ b/test/examples/spec/105nestedStruct.solc
@@ -334,7 +334,7 @@ function readW(w:memory(W)) -> memory(S) {
 }
 
 contract C {
-    function main() {
+    function main() -> word {
         let s:memory(S) = makeS();
 	let w:memory(W) = makeW(s);
 	let s2:memory(S) = readW(w);
diff --git a/test/examples/spec/10negBool.solc b/test/examples/spec/10negBool.solc
index 3def07db..f946e136 100644
--- a/test/examples/spec/10negBool.solc
+++ b/test/examples/spec/10negBool.solc
@@ -18,12 +18,12 @@ instance B : Neg {
 
 contract NegBool {
 
-  function fromB(b) {
+  function fromB(b : B) -> word {
     match b  {
     | F => return 0;
     | T => return 1;
     }
   }
 
-  function main() { return  fromB(Neg.neg(F)); }
+  function main() -> word { return  fromB(Neg.neg(F)); }
 }
diff --git a/test/examples/spec/111storageStruct.solc b/test/examples/spec/111storageStruct.solc
index f3a85f36..b40f288d 100644
--- a/test/examples/spec/111storageStruct.solc
+++ b/test/examples/spec/111storageStruct.solc
@@ -282,7 +282,7 @@ function g() -> word {
 }
 
 contract C {
-    function main() {
+    function main() -> word {
         return g();
     }
 }
diff --git a/test/examples/spec/11negPair.solc b/test/examples/spec/11negPair.solc
index 5946b9f2..e0c2562e 100644
--- a/test/examples/spec/11negPair.solc
+++ b/test/examples/spec/11negPair.solc
@@ -35,19 +35,19 @@ forall a b . a : Neg, b : Neg => instance (a,b):Neg {
 
 contract NegPair {
 
- function bnot(x) {
+ function bnot(x: B) -> B{
    match x {
      | T => return F;
      | F => return T;
    }
 }
 
- function fromB(b) {
+ function fromB(b : B) -> word {
   match b  {
     | F => return 0;
     | T => return 1;
   }
 }
 
- function main() { return  fromB(fst(Neg.neg((F,T)))); }
+ function main() -> word { return  fromB(fst(Neg.neg((F,T)))); }
 }
diff --git a/test/examples/spec/126nanoerc20.solc b/test/examples/spec/126nanoerc20.solc
index f098b28c..4dea6b1c 100644
--- a/test/examples/spec/126nanoerc20.solc
+++ b/test/examples/spec/126nanoerc20.solc
@@ -35,12 +35,12 @@ contract Uint {
   totalSupply : uint256;
   balances : mapping(address,uint256);
 
-  function mint(amount:uint256) {
+  function mint(amount:uint256)  -> () {
     balances[owner] = Num.add(balances[owner], amount);
     totalSupply = Num.add(totalSupply, amount);
   }
 
-  //     function transferFrom(address src, address dst, uint256 amt) public returns (bool) 
+  //     function transferFrom(address src, address dst, uint256 amt) public returns (bool)
   function transferFrom(src:address, dst:address, amt:uint256) -> bool {
      require1(ge(balances[src], amt));
 
@@ -54,20 +54,20 @@ contract Uint {
   }
 
 
-  function withdraw(src:address, amt:uint256) {
+  function withdraw(src:address, amt:uint256) -> () {
     balances[src] = Num.sub(balances[src], amt):uint256;
   }
-  
-  function deposit(dst:address, amt:uint256) {
+
+  function deposit(dst:address, amt:uint256) -> () {
     balances[dst] = Num.add(balances[dst], amt):uint256;
   }
 
-  function init() {
+  function init() -> () {
     owner = address(0x123456789abcdef);
     msg_sender = caller();
     decimals = uint256(18);
   }
-  
+
   function main() -> uint256 {
     init();
     mint(uint256(1000));
diff --git a/test/examples/spec/127microerc20.solc b/test/examples/spec/127microerc20.solc
index 85cf0454..a56491ee 100644
--- a/test/examples/spec/127microerc20.solc
+++ b/test/examples/spec/127microerc20.solc
@@ -1,5 +1,5 @@
 import std;
- 
+
 function caller() -> address {
   let res: word;
   assembly {
@@ -56,7 +56,7 @@ contract Mini {
 */
 
 //  function transferFrom(src:address, dst:address, amt:uint256) -> bool {
-  function transferFrom(src, dst, amt) -> bool  {
+  function transferFrom(src : address, dst : address, amt : uint256) -> bool  {
      require1(ge(balances[src], amt));
 
      match (Eq.eq(src, msg_sender)) {
@@ -71,7 +71,7 @@ contract Mini {
      if ((src != msg_sender) && (allowance [src][msg_sender] != (Num.maxVal():uint256)) ) {
        require1(allowance[src][msg.sender] >= amt);
      }
-*/   
+*/
      balances[src] = Num.sub(balances[src], amt);
      balances[dst] = Num.add(balances[dst], amt):uint256;
      return true;
diff --git a/test/examples/spec/903badassign.solc b/test/examples/spec/903badassign.solc
index 933261d7..4236821a 100644
--- a/test/examples/spec/903badassign.solc
+++ b/test/examples/spec/903badassign.solc
@@ -1,16 +1,16 @@
 contract Option {
   data Option(a) = None | Some(a);
 
-  function just(x) { return Some(x); }
+  forall a . function just(x : a) -> Option(a) { return Some(x); }
 
-  function maybe(n, o) {
+  forall a . function maybe(n : a, o : Option(a)) -> a {
     match o {
       | None => return n;
       | Some(x) => return x;
     }
   }
 
-  function join(mmx) {
+  forall a . function join(mmx : Option(Option(a))) -> Option(a) {
     let result = None;
     match mmx {
       | Some(Some(x)) => result = Some(x);
@@ -19,7 +19,7 @@ contract Option {
     return result;
   }
 
-  function main() {
+  function main() -> word {
     return maybe(0, join(Some(Some(42))));
   }
 }
diff --git a/test/examples/spec/939badfood.solc b/test/examples/spec/939badfood.solc
index 431eb13a..bc984264 100644
--- a/test/examples/spec/939badfood.solc
+++ b/test/examples/spec/939badfood.solc
@@ -15,7 +15,7 @@ instance Food : Enum {
 }
 
 contract Food {
-  function main() {
+  function main() -> word {
         return Enum.fromEnum(Beans);
   }
 }