diff --git a/Data/BinaryTree.juvix b/Data/BinaryTree.juvix
index 31bea8d..1a68bec 100644
--- a/Data/BinaryTree.juvix
+++ b/Data/BinaryTree.juvix
@@ -6,19 +6,14 @@ type BinaryTree (A : Type) :=
   | leaf : BinaryTree A
   | node : BinaryTree A -> A -> BinaryTree A -> BinaryTree A;
 
--- fold a tree in depth first order
-fold
-  : {A B : Type}
-    -> (A -> B -> B -> B)
-    -> B
-    -> BinaryTree A
-    -> B
-  | {A} {B} f acc :=
-    let
-      go (acc : B) : BinaryTree A -> B
-        | leaf := acc
-        | (node l a r) := f a (go acc l) (go acc r);
-    in go acc;
+--- fold a tree in depth first order
+fold {A B} (f : A -> B -> B -> B) (acc : B)
+  : BinaryTree A -> B :=
+  let
+    go (acc : B) : BinaryTree A -> B
+      | leaf := acc
+      | (node l a r) := f a (go acc l) (go acc r);
+  in go acc;
 
 length : {A : Type} -> BinaryTree A -> Nat :=
   fold λ {_ l r := 1 + l + r} 0;
diff --git a/Data/Map.juvix b/Data/Map.juvix
index 069c8c1..1e64b1c 100644
--- a/Data/Map.juvix
+++ b/Data/Map.juvix
@@ -19,7 +19,7 @@ import Stdlib.Trait.Ord as Ord open using {Ord};
 
 import Test.JuvixUnit open;
 
-type Binding (A B : Type) := binding A B;
+type Binding A B := binding A B;
 
 key {A B} : Binding A B -> A
   | (binding a _) := a;
@@ -34,13 +34,13 @@ instance
 bindingKeyOrdering {A B} {{Ord A}} : Ord (Binding A B) :=
   mkOrd λ {b1 b2 := Ord.cmp (key b1) (key b2)};
 
-type Map (A B : Type) := mkMap (AVLTree (Binding A B));
+type Map A B := mkMap (AVLTree (Binding A B));
 
-empty : {A B : Type} -> Map A B := mkMap AVL.empty;
+empty {A B} : Map A B := mkMap AVL.empty;
 
-insertWith {A B} {{Ord A}}
-  : (B -> B -> B) -> A -> B -> Map A B -> Map A B
-  | f k v (mkMap s) :=
+insertWith {A B} {{Ord A}} (f : B -> B -> B) (k : A) (v : B)
+  : Map A B -> Map A B
+  | (mkMap s) :=
     let
       f' : Binding A B -> Binding A B -> Binding A B
         | (binding a b1) (binding _ b2) := binding a (f b1 b2);
@@ -53,16 +53,15 @@ insert {A B : Type} {{Ord A}}
 lookup {A B} {{Ord A}} (k : A) : Map A B -> Maybe B
   | (mkMap s) := mapMaybe value (Set.lookupWith key k s);
 
-fromListWith {A B} {{Ord A}}
-  : (B -> B -> B) -> List (A × B) -> Map A B
-  | f xs :=
-    for (acc := empty) (k, v in xs)
-      insertWith f k v acc;
+fromListWith {A B} {{Ord A}} (f : B -> B -> B) (xs : List
+  (A × B)) : Map A B :=
+  for (acc := empty) (k, v in xs)
+    insertWith f k v acc;
 
 fromList {A B} {{Ord A}} : List (A × B) -> Map A B :=
   fromListWith λ {old new := new};
 
-toList {A B : Type} : Map A B -> List (A × B)
+toList {A B} : Map A B -> List (A × B)
   | (mkMap s) := map (x in Set.toList s) toPair x;
 
 size {A B} : Map A B -> Nat
diff --git a/Data/Queue/Base.juvix b/Data/Queue/Base.juvix
index cde5162..e1913e4 100644
--- a/Data/Queue/Base.juvix
+++ b/Data/Queue/Base.juvix
@@ -1,10 +1,10 @@
 --- This module provides an implementation of a First-In, First-Out (FIFO)
 --- queue based on Okasaki's "Purely Functional Data Structures." Ch.3.
 ---
---- This Okasaki Queue version data structure ensures worst-case constant-time
+--- This Okasaki Queue version data structure ensures amortized constant-time
 --- performance for basic operations such as push, pop, and front.
 ---
---- The OkasakiQueue consists of two lists (front and back) to separate
+--- The Okasaki Queue consists of two lists (front and back) to separate
 --- the concerns of adding and removing elements for ensuring efficient
 --- performance.
 module Data.Queue.Base;
@@ -33,18 +33,20 @@ head {A} : Queue A -> Maybe A
   | (queue nil _) := nothing
   | (queue (x :: _) _) := just x;
 
---- 𝒪(1). Removes the first element from the ;Queue;. If the ;Queue; is empty then returns ;nothing;.
+--- 𝒪(1). Removes the first element from the ;Queue;. If the ;Queue; is empty
+--  then returns ;nothing;.
 tail {A} : Queue A -> Maybe (Queue A)
   | (queue nil _) := nothing
   | (queue (_ :: front) back) := just (queue front back);
 
---- 𝒪(n) in the worst-case scenario, but 𝒪(1) amortized
+--- 𝒪(n) worst-case, but 𝒪(1) amortized
+{-# inline: true #-}
 check {A} : Queue A -> Queue A
   | (queue nil back) := queue (reverse back) nil
   | q := q;
 
---- 𝒪(1). Returns the first element and the rest of the ;Queue;.
---- If the ;Queue; is empty then returns ;nothing;.
+--- 𝒪(n) worst-case, but 𝒪(1) amortized. Returns the first element and the
+--  rest of the ;Queue;. If the ;Queue; is empty then returns ;nothing;.
 pop {A} : Queue A -> Maybe (A × Queue A)
   | (queue nil _) := nothing
   | (queue (x :: front) back) :=
@@ -55,8 +57,9 @@ push {A} (x : A) : Queue A -> Queue A
   | (queue front back) := check (queue front (x :: back));
 
 --- 𝒪(n). Adds a list of elements to the end of the ;Queue;.
-pushMany {A} (xs : List A) : Queue A -> Queue A
-  | q := foldr push q xs;
+pushMany {A} (xs : List A) (q : Queue A) : Queue A :=
+  for (acc := q) (x in xs)
+    push x acc;
 
 --- 𝒪(n). Build a ;Queue; from a ;List;.
 fromList {A} (xs : List A) : Queue A := pushMany xs empty;
@@ -65,7 +68,7 @@ fromList {A} (xs : List A) : Queue A := pushMany xs empty;
 --- The elements are in the same order as they appear in the ;Queue;
 --- (i.e. the first element of the ;Queue; is the first element of the ;List;).
 toList {A} : Queue A -> List A
-  | (queue front back) := back ++ reverse front;
+  | (queue front back) := front ++ reverse back;
 
 --- 𝒪(n). Returns the number of elements in the ;Queue;.
 size {A} : Queue A -> Nat
diff --git a/Data/Set.juvix b/Data/Set.juvix
index 487aad3..1240431 100644
--- a/Data/Set.juvix
+++ b/Data/Set.juvix
@@ -7,8 +7,7 @@ import Stdlib.Trait.Eq as Eq open using {Eq};
 
 import Stdlib.Trait.Ord as Ord open using {Ord};
 
-Set : Type -> Type
-  | A := AVLTree A;
+syntax alias Set := AVLTree;
 
 eqSetI {A} {{Eq A}} : Eq (Set A) := eqAVLTreeI;
 
diff --git a/Data/Set/AVL.juvix b/Data/Set/AVL.juvix
index 0819b13..ec92081 100644
--- a/Data/Set/AVL.juvix
+++ b/Data/Set/AVL.juvix
@@ -43,6 +43,7 @@ type BalanceFactor :=
   | --- Right children is higher.
     LeanRight;
 
+{-# inline: true #-}
 diffFactor {A} : AVLTree A -> Int
   | empty := 0
   | (node _ _ left right) :=
@@ -50,18 +51,18 @@ diffFactor {A} : AVLTree A -> Int
 
 --- 𝒪(1). Computes the balance factor, i.e., the height of the right subtree
 --- minus the height of the left subtree.
-balanceFactor {A} : AVLTree A -> BalanceFactor
-  | n :=
-    let
-      diff : Int := diffFactor n;
-    in if
-      (0 Int.< diff)
-      LeanRight
-      (if (diff Int.< 0) LeanLeft LeanNone);
+balanceFactor {A} (t : AVLTree A) : BalanceFactor :=
+  let
+    diff : Int := diffFactor t;
+  in if
+    (0 Int.< diff)
+    LeanRight
+    (if (diff Int.< 0) LeanLeft LeanNone);
 
 --- 𝒪(1). Helper function for creating a node.
-mknode {A} : A -> AVLTree A -> AVLTree A -> AVLTree A
-  | val l r := node val (1 + max (height l) (height r)) l r;
+mknode {A} (val : A) (l : AVLTree A) (r : AVLTree A)
+  : AVLTree A :=
+  node val (1 + max (height l) (height r)) l r;
 
 --- 𝒪(1). Left rotation.
 rotateLeft {A} : AVLTree A -> AVLTree A
@@ -75,7 +76,7 @@ rotateRight {A} : AVLTree A -> AVLTree A
   | n := n;
 
 --- 𝒪(1). Applies local rotations if needed.
-balance : {a : Type} -> AVLTree a -> AVLTree a
+balance : {A : Type} -> AVLTree A -> AVLTree A
   | empty := empty
   | n@(node x h l r) :=
     let
@@ -95,60 +96,61 @@ balance : {a : Type} -> AVLTree a -> AVLTree a
     };
 
 --- 𝒪(log 𝓃). Lookup a member from the ;AVLTree; using a projection function.
---- Ord a, Ord k and f must be compatible. i.e cmp_k (f a1) (f a2) == cmp_a a1 a2
-lookupWith {a k} {{Ord k}}
-  : (a -> k) -> k -> AVLTree a -> Maybe a
-  | f x :=
-    let
-      go : AVLTree a -> Maybe a
-        | empty := nothing
-        | m@(node y h l r) :=
-          case Ord.cmp x (f y) of {
-            | LT := go l
-            | GT := go r
-            | EQ := just y
-          };
-    in go;
+--- Ord A, Ord K and f must be compatible. i.e cmp_k (f a1) (f a2) == cmp_a a1 a2
+{-# specialize: [1] #-}
+lookupWith {A K} {{Ord K}} (f : A -> K) (x : K)
+  : AVLTree A -> Maybe A :=
+  let
+    {-# specialize-by: [f] #-}
+    go : AVLTree A -> Maybe A
+      | empty := nothing
+      | m@(node y h l r) :=
+        case Ord.cmp x (f y) of {
+          | LT := go l
+          | GT := go r
+          | EQ := just y
+        };
+  in go;
 
 --- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;.
-member? {a} {{Ord a}} : a -> AVLTree a -> Bool
-  | x := isJust ∘ lookupWith id x;
+member? {A} {{Ord A}} (x : A) : AVLTree A -> Bool :=
+  isJust ∘ lookupWith id x;
 
 --- 𝒪(log 𝓃). Inserts an element into and ;AVLTree; using a function to
 --- deduplicate entries.
 ---
 --- Assumption: Given a1 == a2 then f a1 a2 == a1 == a2
 --- where == comes from Ord a.
-insertWith {a} {{Ord a}}
-  : (a -> a -> a) -> a -> AVLTree a -> AVLTree a
-  | f x :=
-    let
-      go : AVLTree a -> AVLTree a
-        | empty := mknode x empty empty
-        | m@(node y h l r) :=
-          case Ord.cmp x y of {
-            | LT := balance (mknode y (go l) r)
-            | GT := balance (mknode y l (go r))
-            | EQ := node (f y x) h l r
-          };
-    in go;
+{-# specialize: [1] #-}
+insertWith {A} {{Ord A}} (f : A -> A -> A) (x : A)
+  : AVLTree A -> AVLTree A :=
+  let
+    {-# specialize-by: [f] #-}
+    go : AVLTree A -> AVLTree A
+      | empty := mknode x empty empty
+      | m@(node y h l r) :=
+        case Ord.cmp x y of {
+          | LT := balance (mknode y (go l) r)
+          | GT := balance (mknode y l (go r))
+          | EQ := node (f y x) h l r
+        };
+  in go;
 
 --- 𝒪(log 𝓃). Inserts an element into and ;AVLTree;.
-insert {a : Type} {{Ord a}} : a -> AVLTree a -> AVLTree a :=
+insert {A} {{Ord A}} : A -> AVLTree A -> AVLTree A :=
   insertWith (flip const);
 
 --- 𝒪(log 𝓃). Removes an element from an ;AVLTree;.
-delete {a : Type} {{Ord a}} (x : a)
-  : AVLTree a -> AVLTree a :=
+delete {A} {{Ord A}} (x : A) : AVLTree A -> AVLTree A :=
   let
-    deleteMin : AVLTree a -> Maybe (a × AVLTree a)
+    deleteMin : AVLTree A -> Maybe (A × AVLTree A)
       | empty := nothing
       | (node v _ l r) :=
         case deleteMin l of {
           | nothing := just (v, r)
           | just (m, l') := just (m, mknode v l' r)
         };
-    go : AVLTree a -> AVLTree a
+    go : AVLTree A -> AVLTree A
       | empty := empty
       | (node y h l r) :=
         case Ord.cmp x y of {
@@ -167,50 +169,49 @@ delete {a : Type} {{Ord a}} (x : a)
   in go;
 
 --- 𝒪(log 𝓃). Returns the minimum element of the ;AVLTree;.
-lookupMin : {a : Type} -> AVLTree a -> Maybe a
+lookupMin {A} : AVLTree A -> Maybe A
   | empty := nothing
   | (node y _ empty empty) := just y
   | (node _ _ empty r) := lookupMin r
   | (node _ _ l _) := lookupMin l;
 
 --- 𝒪(log 𝓃). Returns the maximum element of the ;AVLTree;.
-lookupMax : {a : Type} -> AVLTree a -> Maybe a
+lookupMax {A} : AVLTree A -> Maybe A
   | empty := nothing
   | (node y _ empty empty) := just y
   | (node _ _ l empty) := lookupMax l
   | (node _ _ _ r) := lookupMax r;
 
 --- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree;.
-deleteMany {a : Type} {{Ord a}}
-  : List a -> AVLTree a -> AVLTree a
-  | d t := for (acc := t) (x in d) delete x acc;
+deleteMany {A} {{Ord A}} (d : List A) (t : AVLTree A)
+  : AVLTree A := for (acc := t) (x in d) delete x acc;
 
 --- 𝒪(𝓃). Checks the ;AVLTree; height invariant. I.e. that
 --- every two children do not differ on height by more than 1.
-isBalanced : {a : Type} -> AVLTree a -> Bool
+isBalanced {A} : AVLTree A -> Bool
   | empty := true
   | n@(node _ _ l r) :=
     isBalanced l && isBalanced r && abs (diffFactor n) <= 1;
 
 --- 𝒪(𝓃 log 𝓃). Create an ;AVLTree; from an unsorted ;List;.
-fromList {a : Type} {{Ord a}} (l : List a) : AVLTree a :=
+fromList {A} {{Ord A}} (l : List A) : AVLTree A :=
   for (acc := empty) (x in l)
     insert x acc;
 
 --- 𝒪(𝓃). Returns the number of elements of an ;AVLTree;.
-size : {a : Type} -> AVLTree a -> Nat
+size {A} : AVLTree A -> Nat
   | empty := 0
   | (node _ _ l r) := 1 + size l + size r;
 
 --- 𝒪(𝓃). Returns the elements of an ;AVLTree; in ascending order.
-toList : {a : Type} -> AVLTree a -> List a
+toList {A} : AVLTree A -> List A
   | empty := nil
   | (node x _ l r) := toList l ++ (x :: nil) ++ toList r;
 
 --- 𝒪(𝓃). Formats the tree in a debug friendly format.
-prettyDebug {a : Type} {{Show a}} : AVLTree a -> String :=
+prettyDebug {A} {{Show A}} : AVLTree A -> String :=
   let
-    go : AVLTree a -> String
+    go : AVLTree A -> String
       | empty := "_"
       | n@(node v h l r) :=
         "("
@@ -225,14 +226,14 @@ prettyDebug {a : Type} {{Show a}} : AVLTree a -> String :=
   in go;
 
 --- 𝒪(𝓃).
-toTree : {a : Type} -> AVLTree a -> Maybe (Tree a)
+toTree {A} : AVLTree A -> Maybe (Tree A)
   | empty := nothing
   | (node v _ l r) :=
     just
       (Tree.node v (catMaybes (toTree l :: toTree r :: nil)));
 
 --- Returns the textual representation of an ;AVLTree;.
-pretty {a} {{Show a}} : AVLTree a -> String :=
+pretty {A} {{Show A}} : AVLTree A -> String :=
   maybe "empty" Tree.treeToString ∘ toTree;
 
 instance
diff --git a/Data/String.juvix b/Data/String.juvix
index 87fd9b3..db6c806 100644
--- a/Data/String.juvix
+++ b/Data/String.juvix
@@ -3,5 +3,4 @@ module Data.String;
 import Stdlib.Prelude open;
 import Stdlib.Data.String.Ord open;
 
-null? : String -> Bool
-  | s := s == "";
+null? (s : String) : Bool := s == "";
diff --git a/Data/Tmp.juvix b/Data/Tmp.juvix
index 7b053e9..4aa21c2 100644
--- a/Data/Tmp.juvix
+++ b/Data/Tmp.juvix
@@ -8,16 +8,10 @@ printNatListLn : List Nat → IO
   | (x :: xs) :=
     printNat x >> printString " :: " >> printNatListLn xs;
 
-mapMaybe : {A B : Type} -> (A -> B) -> Maybe A -> Maybe B
-  | f m :=
-    case m of {
-      | nothing := nothing
-      | just a := just (f a)
-    };
+mapMaybe {A B} (f : A -> B) : Maybe A -> Maybe B
+  | nothing := nothing
+  | (just a) := just (f a);
 
-isJust : {A : Type} -> Maybe A -> Bool
-  | m :=
-    case m of {
-      | nothing := false
-      | just _ := true
-    };
+isJust {A} : Maybe A -> Bool
+  | nothing := false
+  | (just _) := true;
diff --git a/Data/Tree.juvix b/Data/Tree.juvix
index f930470..683f06f 100644
--- a/Data/Tree.juvix
+++ b/Data/Tree.juvix
@@ -4,17 +4,15 @@ module Data.Tree;
 import Stdlib.Prelude open;
 
 --- A ;List; of trees.
-Forest : Type -> Type
-  
-  | A := List (Tree A);
+Forest (A : Type) : Type := List (Tree A);
 
 --- N-Ary tree.
 positive
 type Tree (A : Type) := node A (List (Tree A));
 
-shift : String -> String -> List String -> List String
-  | first other xs :=
-    zipWith (++str) (first :: replicate (length xs) other) xs;
+shift (first other : String) (xs : List String)
+  : List String :=
+  zipWith (++str) (first :: replicate (length xs) other) xs;
 
 terminating
 draw {A} {{Show A}} : Tree A -> List String
diff --git a/Data/UnbalancedSet.juvix b/Data/UnbalancedSet.juvix
index 568e1a7..ddc4d90 100644
--- a/Data/UnbalancedSet.juvix
+++ b/Data/UnbalancedSet.juvix
@@ -12,11 +12,11 @@ open Tree using {BinaryTree; leaf; node};
 type UnbalancedSet (A : Type) :=
   unbalancedSet : Ord A -> BinaryTree A -> UnbalancedSet A;
 
-empty : {A : Type} -> Ord A -> UnbalancedSet A
-  | o := unbalancedSet o leaf;
+empty {A} {{o : Ord A}} : UnbalancedSet A :=
+  unbalancedSet o leaf;
 
-member? : {A : Type} -> A -> UnbalancedSet A -> Bool
-  | {A} x (unbalancedSet o@(mkOrd cmp) t) :=
+member? {A} (x : A) : UnbalancedSet A -> Bool
+  | (unbalancedSet o@(mkOrd cmp) t) :=
     let
       go : BinaryTree A -> Bool
         | leaf := false
@@ -28,9 +28,8 @@ member? : {A : Type} -> A -> UnbalancedSet A -> Bool
           };
     in go t;
 
-insert
-  : {A : Type} -> A -> UnbalancedSet A -> UnbalancedSet A
-  | {A} x (unbalancedSet o@(mkOrd cmp) t) :=
+insert {A} (x : A) : UnbalancedSet A -> UnbalancedSet A
+  | (unbalancedSet o@(mkOrd cmp) t) :=
     let
       go : BinaryTree A -> BinaryTree A
         | leaf := node leaf x leaf
@@ -42,16 +41,12 @@ insert
           };
     in unbalancedSet o (go t);
 
-length : {A : Type} -> UnbalancedSet A -> Nat
+length {A} : UnbalancedSet A -> Nat
   | (unbalancedSet _ t) := Tree.length t;
 
-to-list : {A : Type} -> UnbalancedSet A -> List A
+to-list {A} : UnbalancedSet A -> List A
   | (unbalancedSet _ t) := Tree.to-list t;
 
-set-ordering : {A : Type} -> Ord A -> Ord (UnbalancedSet A)
-  | {A} o :=
-    let
-      from-ord-list : Ord (List A) -> Ord (UnbalancedSet A)
-        | (mkOrd cmp) :=
-          mkOrd λ {s1 s2 := cmp (to-list s1) (to-list s2)};
-    in from-ord-list (ordListI {{o}});
+instance
+set-ordering {A} {{Ord A}} : Ord (UnbalancedSet A) :=
+  mkOrd λ {s1 s2 := Ord.cmp (to-list s1) (to-list s2)};
diff --git a/Test/AVL.juvix b/Test/AVL.juvix
index f74d66c..a5174cd 100644
--- a/Test/AVL.juvix
+++ b/Test/AVL.juvix
@@ -33,7 +33,10 @@ s3 : TestDescr := "s3", 6, fromList [5; 4; 3; 2; 1; 0];
 s4 : TestDescr := "s4", 5, fromList [1; 2; 3; 4; 5];
 
 tests : List Test :=
-  concatMap mkTests [s1; s2; s3; s4; s2-delete];
+  [testCase
+      "s1-member"
+      (assertTrue "member? 3 s1" (member? 3 (snd (snd s1))))]
+    ++ concatMap mkTests [s1; s2; s3; s4; s2-delete];
 
 main : IO :=
   printStringLn (pretty (snd (snd s1)))
diff --git a/Test/Queue.juvix b/Test/Queue.juvix
index cb19933..ceb2500 100644
--- a/Test/Queue.juvix
+++ b/Test/Queue.juvix
@@ -27,7 +27,7 @@ tests : List Test :=
     "Queue.push should add an element"
     (checkWithList q1 [1]); testCase
     "Queue.push first element should be first pushed"
-    (checkWithList q2 [2; 1]); testCase
+    (checkWithList q2 [1; 2]); testCase
     "Queue.head should return first element"
     (assertEqual
       "head of queue q3"
@@ -42,11 +42,11 @@ tests : List Test :=
     (assertEqual
       "pop of queue q3"
       (pop q3)
-      (just (1, fromList [3; 2]))); testCase
+      (just (1, fromList [2; 3]))); testCase
     "Queue.tail should return queue without first element"
     (assertEqual
       "tail of queue q3"
       (tail q3)
-      ((just ∘ fromList) [3; 2]))];
+      ((just ∘ fromList) [2; 3]))];
 
 main : IO := runTestSuite $ testSuite "Queue" tests;
diff --git a/Test/UnbalancedSet.juvix b/Test/UnbalancedSet.juvix
index 8db189b..82df585 100644
--- a/Test/UnbalancedSet.juvix
+++ b/Test/UnbalancedSet.juvix
@@ -13,9 +13,9 @@ tests : List Test :=
         1
         (Set.insert
           3
-          (Set.insert 2 (Set.insert 1 (Set.empty ordNatI))));
+          (Set.insert 2 (Set.insert 1 Set.empty)));
     setInSet : UnbalancedSet (UnbalancedSet Nat) :=
-      Set.insert s (Set.empty (Set.set-ordering ordNatI));
+      Set.insert s Set.empty;
   in [testCase
     "Set.length computes the expected size"
     (assertEqual "unexpected size" (Set.length s) 3); testCase