diff --git a/Language/Copilot.hs b/Language/Copilot.hs
--- a/Language/Copilot.hs
+++ b/Language/Copilot.hs
@@ -2,7 +2,6 @@
   ( module Language.Copilot.Core
   , module Language.Copilot.Analyser
   , module Language.Copilot.Interpreter
-  -- , module Language.Copilot.Variables
   , module Language.Copilot.Help
   , module Language.Copilot.AtomToC
   , module Language.Copilot.Compiler
@@ -22,7 +21,6 @@
 import Language.Copilot.Core
 import Language.Copilot.Analyser
 import Language.Copilot.Interpreter
--- import Language.Copilot.Variables
 import Language.Copilot.Help
 import Language.Copilot.AtomToC
 import Language.Copilot.Compiler
diff --git a/Language/Copilot/Examples/Examples.hs b/Language/Copilot/Examples/Examples.hs
--- a/Language/Copilot/Examples/Examples.hs
+++ b/Language/Copilot/Examples/Examples.hs
@@ -14,83 +14,126 @@
 import Data.Int
 
 import Language.Copilot 
-import Language.Copilot.Variables
+-- import Language.Copilot.Variables
 
 fib :: Streams
 fib = do
-  "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")
-  "t"   .= even (var "fib")
+  let f = varW64 "f"
+  let t   = varB "t"
+  f .= [0,1] ++ f + (drop 1 f)
+  t .= even f
     where even :: Spec Word64 -> Spec Bool
           even w' = w' `mod` 2 == 0
 
 t1 :: Streams
-t1 = do
-     x .= [0, 1, 2] ++ var x - (drop 1 $ varI32 x)
-     y .= [True, False] ++ var y ^ var z
-     z .= varI32 "x" <= drop 1 (var x)
+t1 = 
+  let x = varI32 "x"
+      y = varB "y"
+      z = varB "z"
+  in do
+    x .= [0, 1, 2] ++ x - (drop 1 x)
+    y .= [True, False] ++ y ^ z
+    z .= x <= drop 1 x
 
-t2 :: Streams
-t2 = do
-     a .= [True] ++ not (var a) 
-     b .= mux (var a) 2 (int8 3) 
+-- t2 :: Streams
+-- t2 = do
+--      a .= [True] ++ not (var a) 
+--      b .= mux (var a) 2 (int8 3) 
 
 -- t3 :: use an external variable called ext, typed Word32
 t3 :: Streams
-t3 = do
-     a .= [0,1] ++ (var a) + extW32 "ext" 8 + extW32 "ext" 8 + extW32 "ext" 1
-     b .= [True, False] ++ 2 + var a < 5 + extW32 "_ext" 1
+t3 = 
+  let a    = varW32 "a"
+      b    = varB "b"
+      ext8 = extW32 "ext" 8
+      ext1 = extW32 "ext" 1
+  in do
+      a .= [0,1] ++ a + ext8 + ext8 + ext1
+      b .= [True, False] ++ 2 + a < 5 + ext1
 
 t4 :: Streams
-t4 = do
-     a .= [True,False] ++ not (var a)
-     b .= drop 1 (varB a)
+t4 = let
+    a = varB "a"
+    b = varB "b"
+  in do
+    a .= [True,False] ++ not a
+    b .= drop 1 a
 
 t5 :: Streams
-t5 = do
-    x .= drop 3 (varB y)
-    y .= [True, True] ++ not (var z)
-    z .= [False, False] ++ not (var z)
-    w .= varB x || var y
+t5 = 
+  let x = varB "x"
+      y = varB "y"
+      w = varB "w"
+      z = varB "z"
+  in do
+      x .= drop 3 y
+      y .= [True, True] ++ not z
+      z .= [False, False] ++ not z
+      w .= x || y
 
 yy :: Streams
-yy = do a .= constW64 4  
+yy = 
+  let a = varW64 "a"
+  in  do a .= 4  
 
 zz :: Streams
-zz = do --a .= [0..4] ++ drop 4 (varW32 a) + 1
-  a .= (varW32 a) + 1
-  b .= drop 3 (varW32 a)
+zz = 
+  let a = varW32 "a"
+      b = varW32 "b"
+  in do --a .= [0..4] ++ drop 4 (varW32 a) + 1
+      a .= a + 1
+      b .= drop 3 a
 
 xx :: Streams
-xx = do 
-     a .= extW32 "ext" 5 
-     b .= [3] ++ (varW32 a)
-     c .= [0, 1, 3, 4] ++ drop 1 (varW32 b)
+xx = 
+  let a = varW32 "a"
+      b = varW32 "b"
+      c = varW32 "c"
+      ext = extW32 "ext" 1
+  in do 
+      a .= ext
+      b .= [3] ++ a
+      c .= [0, 1, 3, 4] ++ drop 1 b
 
 -- If the temperature rises more than 2.3 degrees within 0.2 seconds, then the
 -- engine is immediately shut off.  From the paper.
 engine :: Streams
 engine = do
-   "temps" .= [0, 0, 0] ++ extF "temp" 1
-   "overTempRise" .= drop 2 (varF "temps") > 2.3 + var "temps"
-   "trigger" .= (var "overTempRise") ==> (extB "shutoff" 2) 
+  -- external vars
+  let temp     = extF "temp" 1      
+  let shutoff  = extB "shutoff" 2
+  -- Copilot vars
+  let temps    = varF "temps"
+  let overTemp = varB "overTemp"
+  let trigger  = varB "trigger"
 
+  temps    .= [0, 0, 0] ++ temp
+  overTemp .= drop 2 temps > 2.3 + temps
+  trigger  .= overTemp ==> shutoff
+
 -- To compile: > let (streams, ss) = dist in interface $ compileOpts streams ss "dist"
 -- s at phase 2 on port 1.  Not stable.
 dist :: DistributedStreams
 dist = 
-  ( a .= [0,1] ++ (var a) + constW8 1
-  ,     sendW8 a (2, 1)
-    ..| emptySM
-  )
+  let a = varW8 "a"
+  in 
+    ( a .= [0,1] ++ a + 1
+    ,     sendW8 a (2, 1)
+      ..| emptySM
+    )
 
 -- greatest common divisor.
 gcd :: Word16 -> Word16 -> Streams
-gcd n0 n1 = do 
+gcd n0 n1 = do
+  let a = varW16 "a"
+  let b = varW16 "b"
   a .= alg n0 a b
   b .= alg n1 b a
-  "ans" .= varW16 a == var b
-    where alg x0 x1 x2 = [x0] ++ mux (varW16 x1 > var x2) (var x1 - var x2) (var x1)
 
+  let ans = varB "ans"
+  ans .= a == b
+    where alg x0 x1 x2 = [x0] ++ mux (x1 > x2) (x1 - x2) x1
+
 -- greatest common divisor of two external vars.  Compare to
 -- Language.Atom.Example Try 
 --
@@ -101,38 +144,60 @@
 -- sample the external variables.
 gcd' :: Streams
 gcd' = do 
-  a .= alg "n" (sub a b)
-  b .= alg "m" (sub b a)
-  "ans" .= varW16 a == varW16 b && not (var "init")
-  "init" .= [True] ++ false
-    where sub hi lo = mux (varW16 hi > var lo) (var hi - var lo) (var hi)
-          alg ext ex = [0] ++ mux (var "init") (extW16 ext 1) ex
+  let n = extW16 "n" 1
+  let m = extW16 "m" 1
 
+  let a = varW16 "a"
+  let b = varW16 "b"
+  let init = varB "init"
+  a .= alg n (sub a b) init
+  b .= alg m (sub b a) init
+
+  let ans = varB "ans"
+  ans .= a == b && not init
+
+  init .= [True] ++ false
+
+  where sub hi lo = mux (hi > lo) (hi - lo) hi
+        alg ext ex init = [0] ++ mux init ext ex
+
 testCoercions :: Streams
 testCoercions = do
-    "word" .= [1] ++ (varW8 "word") * (-2)
-    "int"  .= 1 + castI16 (varW8 "word") 
+  let word = varW8 "word"
+  word .= [1] ++ word * (-2)
+  let int = varI16 "int"
+  int  .= 1 + cast word
 
 testCoercions2 :: Streams
 testCoercions2 = do
-    b .= [True] ++ not (var b)
-    i .= castI8 (varB b)
+  let b = varB "b"
+  b .= [True] ++ not b
+  let i = varI16 "i"
+  let j = varI16 "j"
+  i .= cast j
+  j .= 3
 
 testCoercions3 :: Streams
 testCoercions3 = do
-  x .= [True] ++ not (var x)
-  y .= castI32 (varB x) + castI32 (castW8 (varB x)) 
+  let x = varB "x"
+  x .= [True] ++ not x
+  let y = varI32 "y"
+  y .= cast x + cast x
 
 i8 :: Streams
-i8 = do v .= [0, 1] ++ (varI8 v) + 1 
+i8 = 
+  let v = varI8 "v" in v .= [0, 1] ++ v + 1 
     
 trap :: Streams
 trap = do
-    "target" .= [0] ++ varW32 "target" + 1 
-    "x" .= [0,0] ++ var "y" + varW32 "target" 
-    "y" .= [0,0] ++ var "x" + varW32 "target" 
-    
+  let target = varW32 "target"
+  target .= [0] ++ target + 1 
 
+  let x = varW32 "x"
+  let y = varW32 "y"
+  x .= [0,0] ++ y + target
+  y .= [0,0] ++ x + target
+
 -- vicious :: Streams
 -- vicious = do 
 --     "varExt" .= extW32 "ext" 5 
@@ -188,17 +253,24 @@
   -- b .= [0] ++ extArrW16 ("gg", varW16 b) 4 
   -- c .= [True] ++ var c
   -- d .= varB c 
-  e .= [6,7,8] ++ (constW16 3) -- + extArrW16 ("gg", varW16 b) 2
+  let e = varW16 "e"
+  e .= [6,7,8] ++ 3 -- + extArrW16 ("gg", varW16 b) 2
 --  f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2 
-  g .= (extArrW16 ("gg", varW16 e) 1) == (extArrW16 ("gg", varW16 e) 1)
+  let g = varB "g"
+  let gg = extArrW16 "gg" e 
+  g .= gg 1 == gg 2
   -- h .= [0] ++ drop 1 (varW16 g)
 
 
 -- t3 :: use an external variable called ext, typed Word32
 t99 :: Streams
 t99 = do
-     a .= [0,1] ++ (var a) + extW32 "ext" 8 + extW32 "ext" 8 + extW32 "ext" 1
-     b .= [True, False] ++ 2 + var a < 5 + extW32 "_ext" 1
+  let ext = extW32 "ext"
+  let a = varW32 "a"
+  a .= [0,1] ++ a + ext 8 + ext 8 + ext 1
+
+  let b = varB "b"
+  b .= [True, False] ++ 2 + a < 5 + ext 1
 
 -- test external idx before after and in the stream it references
 -- test multiple defs
diff --git a/Language/Copilot/Examples/LTLExamples.hs b/Language/Copilot/Examples/LTLExamples.hs
--- a/Language/Copilot/Examples/LTLExamples.hs
+++ b/Language/Copilot/Examples/LTLExamples.hs
@@ -8,64 +8,76 @@
 import Language.Copilot
 import Language.Copilot.Libs.Indexes
 import Language.Copilot.Libs.LTL
-import Language.Copilot.Variables
 
 ----------------
 -- LTL tests ---
 ----------------
 
-testing, output :: Var
-testing = "testing"
-output = "output"
-
 -- Can be tested with various values of val.  Use the interpreter to see the
 -- outputs.
 
+testing, output :: Spec Bool
+testing = varB "testing"
+output = varB "output"
+
 tSoonest :: Int -> Streams
 tSoonest val = do 
   testing .= replicate (val+2) False ++ true
-  output  .= soonest val (var testing)
+  let out = varI16 "out"
+  out     .= soonest val testing
 
 tLatest :: Int -> Streams
 tLatest val = do 
   testing .= replicate (val-2) False ++ true
-  output  .= latest val (var testing)
+  let out = varI16 "out"
+  out     .= latest val testing
 
 tAlways :: Int -> Int -> Streams
 tAlways i1 i2 = do 
   testing .=    (replicate i1 True P.++ [False]) ++ true
-  output  `ltl` always i2 (varB testing)
+  output  `ltl` always i2 testing
 
 tNext :: Int -> Streams
 tNext i1 = do 
   testing .=    (replicate i1 False P.++ [True]) ++ false
-  output  `ltl` next (varB testing)
+  output  `ltl` next testing
 
 tFuture :: Int -> Int -> Streams
 tFuture i1 i2 = do 
-  testing .=    (replicate i1 False P.++ [True]) ++ varB testing
-  output  `ltl` eventually i2 (varB testing)
+  testing .=    (replicate i1 False P.++ [True]) ++ testing
+  output  `ltl` eventually i2 testing
 
+
+c, t0, t1 :: Spec Bool
+t0 = varB "t0"
+t1 = varB "t1"
+c = varB "c"
+
 tUntil :: Int -> Int -> Int -> Streams
 tUntil i1 i2 i3 = do 
-  "t1"   .=    replicate i1 False ++ true
-  "t0"   .=    replicate i2 True ++ false
-  output `ltl` until i3 (varB "t0") (varB "t1")
+  t1   .=    replicate i1 False ++ true
+  t0   .=    replicate i2 True ++ false
+  output `ltl` until i3 t0 t1
 
 tRelease0 :: Int -> Streams
 tRelease0 val = output `ltl` release val false true
 
 tRelease1 :: Int -> Int -> Streams
 tRelease1 i1 i2 = do 
-  "t1"   .=    replicate i1 True ++ varB c
-  c      .=    [False] ++ not (var c)
-  "t0"   .=    true
-  output `ltl` release i2 (varB "t0") (varB "t1")
+  t1   .=    replicate i1 True ++ c
+  c    .=    [False] ++ not c
+  t0   .=    true
+  output `ltl` release i2 t0 t1
           
 testRules :: Streams
 testRules = do
-    "v1" .=    (not true) || Var "v2" 
-    "v2" .=    [True, False] ++ [True] ++ Var "v3" < extI8 "v4" 5 
-    "v3" .=    0 + drop 3 (int8 6) 
-    "v4" `ltl` always 5 (Var "v1") 
+  let v1 = varB "v1"
+  let v2 = varB "v2"
+  let v3 = varI16 "v3"
+  let v4 = varB "v4"
+  let ext = extI8 "ext" 5 
+  v1 .=    (not true) || v2
+  v2 .=    [True, False] ++ [True] ++ v3 < cast ext
+  v3 .=    0 + drop 3 6
+  v4 `ltl` always 5 v1
 
diff --git a/Language/Copilot/Examples/PTLTLExamples.hs b/Language/Copilot/Examples/PTLTLExamples.hs
--- a/Language/Copilot/Examples/PTLTLExamples.hs
+++ b/Language/Copilot/Examples/PTLTLExamples.hs
@@ -2,101 +2,125 @@
 
 module Language.Copilot.Examples.PTLTLExamples where
 
-import Prelude (($), String, repeat, replicate, IO())
+import Prelude (($), repeat, replicate, IO())
 import qualified Prelude as P
 import Data.Map (fromList)
 
 import Language.Copilot
 import Language.Copilot.Libs.PTLTL
-import Language.Copilot.Variables
 
 -- Next examples are for testing of the ptLTL library
 
 -- test of previous
 tstdatprv :: Streams
-tstdatprv = a .= [True, False] ++ varB a 
+tstdatprv = do
+  let a = varB "a"
+  a .= [True, False] ++ a 
                
 tprv :: Streams
 tprv = do
+  let c = varB "c"
+  let a = varB "a"
   tstdatprv 
-  c `ptltl` (previous $ varB a)
+  c `ptltl` previous a
 
 -- test of alwaysBeen
 tstdatAB ::  Streams
-tstdatAB = d .= [True, True, True, True, True, True, True, False] ++ varB d
+tstdatAB = do
+  let d = varB "d"
+  d .= [True, True, True, True, True, True, True, False] ++ d
 
 tAB :: Streams
 tAB = do
+   let f = varB "f"
+   let d = varB "d"
    tstdatAB 
-   f `ptltl` (alwaysBeen $ var d)
+   f `ptltl` alwaysBeen d
 
 -- test of eventuallyPrev
 tstdatEP ::  Streams
-tstdatEP = g .= [False, False, False, False, False, True, False] ++ varB g 
+tstdatEP = do
+  let g = varB "g"
+  g .= [False, False, False, False, False, True, False] ++ g 
 
 tEP :: Streams
 tEP = do
+    let h = varB "h"
+    let g = varB "g"
     tstdatEP 
-    h `ptltl` (eventuallyPrev $ varB g)
+    h `ptltl` eventuallyPrev g
 
+q1, q2, z :: Spec Bool
+q1 = varB "q1"
+q2 = varB "q2"
+z = varB "z"
+
 -- test of since
 tstdat1Sin :: Streams
-tstdat1Sin = "q1" .= [False, False, False, False, True] ++ true --varB "q1"
+tstdat1Sin = q1 .= [False, False, False, False, True] ++ true --varB "q1"
 
 tstdat2Sin :: Streams
-tstdat2Sin = "q2" .= [False, False, True, False, False, False, False ] ++ varB "q2"
+tstdat2Sin = q2 .= [False, False, True, False, False, False, False ] ++ q2
+
                   
 tSince :: Streams 
 tSince = do
     tstdat1Sin 
     tstdat2Sin 
-    "z1" `ptltl` (varB "q1" `since` varB "q2")
+    z `ptltl` (q1 `since` q2)
 
 -- with external variables
 -- interface $ setE (emptySM {bMap = fromList [("e1", [True,True ..]), ("e2", [False,False ..])]}) $ interpretOpts tSinExt 20
 tSinExt :: Streams 
 tSinExt = do
-  ptltl "z1" $ extB "e1" 2 `since`extB "q2" 3
+  let e1 = extB "e1" 2
+  let e2 = extB "e2" 3
+  z `ptltl` (e1 `since` e2)
 
 tSinExt2 :: Streams 
 tSinExt2 = do
-  a .= not (extB "e1" 2)
-  b .= constW16 3 > 2
-  s `ptltl` ((extB "e2" 2) `since` (var b))
-  t `ptltl` (alwaysBeen $ not (varB a))
-  e .= extB "e1" 2 ==> varB d
-
+  let e1 = extB "e1" 2
+  let e2 = extB "e2" 2
+  let a = varB "a"
+  let s = varB "s"
+  let d = varB "d"
+  let t = varB "t"
+  let e = varB "e"
 
-engineTemp, engineOff, coolerOn, monitor, temp, cooler, off, cnt :: String
-engineTemp = "engineTemp"
-engineOff  = "engineOff"
-coolerOn   = "coolerOn"
-monitor    = "trigger"
-temp       = "temp"
-off        = "off"
-cnt        = "cnt"
-cooler     = "cooler"
+  a .= not e1
+  s `ptltl` (e2 `since` d)
+  t `ptltl` (alwaysBeen $ not a)
+  e .= e1 ==> d
 
 -- "If the engine temperature exeeds 250 degrees, then the engine is shutoff
 -- within the next 10 periods, and in the period following the shutoff, the
 -- cooler is engaged and remains engaged."
 engine :: Streams
 engine = do
-  temp    `ptltl` alwaysBeen (extW8 engineTemp 1 > 250)
-  cnt     .=      [0] ++ mux (varB temp && varW8 cnt < 10) 
-                             (varW8 cnt + 1)
-                             (varW8 cnt)
-  off     .=      (varW8 cnt >= 10 ==> extB engineOff 1)
-  cooler  `ptltl` (extB coolerOn 1 `since` extB engineOff 1)
-  monitor .=      varB off && varB cooler
+  -- external vars
+  let engineTemp = extW8 "engineTemp" 1
+  let engineOff  = extB "engineOff" 1
+  let coolerOn   = extB "coolerOn" 1
+  -- Copilot vars
+  let cnt        = varW8 "cnt"
+  let temp       = varB "temp"
+  let cooler     = varB "cooler"
+  let off        = varB "off"
+  let monitor    = varB "monitor"
 
+  temp    `ptltl` (alwaysBeen (engineTemp > 250))
+  cnt     .=      [0] ++ mux (temp && cnt < 10) (cnt + 1) cnt
+  off     .=      cnt >= 10 ==> engineOff
+  cooler  `ptltl` (coolerOn `since` engineOff)
+  monitor .=      off && cooler
+
 engineRun :: IO ()
 engineRun = 
   interpret engine 40 $ 
     setE (emptySM { bMap = fromList 
-                            [ (engineOff, replicate 8 False P.++ repeat True)
-                            , (coolerOn, replicate 9 False P.++ repeat True)
+                            [ ("engineOff", replicate 8 False P.++ repeat True)
+                            , ("coolerOn", replicate 9 False P.++ repeat True)
                             ]
-                  , w8Map = fromList [(engineTemp, [99,100..])]
+                  , w8Map = fromList [("engineTemp", [99,100..])]
                   }) baseOpts
 
diff --git a/Language/Copilot/Examples/StatExamples.hs b/Language/Copilot/Examples/StatExamples.hs
--- a/Language/Copilot/Examples/StatExamples.hs
+++ b/Language/Copilot/Examples/StatExamples.hs
@@ -4,18 +4,25 @@
 import Language.Copilot.Core
 import Language.Copilot.Language
 import Language.Copilot.Interface
-import Language.Copilot.Variables
 import Language.Copilot.PrettyPrinter
 import Language.Copilot.Libs.Statistics
 
 t0 :: Streams
 t0 = do
-  a .= [0..5] ++ (varW16 a) + 6
-  "min" .= min 3 (varW16 a)
-  "max" .= max 3 (varW16 a)
-  "sum" .= sum 3 (varW16 a)
+  let minV = varW16 "min"
+  let maxV = varW16 "max"
+  let sumV = varW16 "sum"
+  let a = varW16 "a"
 
+  a .= [0..5] ++ a + 6
+  minV .= min 3 a
+  maxV .= max 3 a
+  sumV .= sum 3 a
+
 tMean :: Streams
 tMean = do
-  a .= [0..5] ++ (varD a) + 6
-  "out" .= mean 4 (varD a)
+  let a = varD "a"
+  let out = varD "out"
+
+  a .= [0..5] ++ a + 6
+  out .= mean 4 a
diff --git a/Language/Copilot/Language.hs b/Language/Copilot/Language.hs
--- a/Language/Copilot/Language.hs
+++ b/Language/Copilot/Language.hs
@@ -16,10 +16,8 @@
         -- * Division
         Fractional((/)),
         mux,
---        CastIntTo(..),
-        -- * The next functions are used only to coerce the type of their argument
-        bool, int8, int16, int32, int64,
-        word8, word16, word32, word64, float, double,
+        varB, varI8, varI16, varI32, varI64,
+        varW8, varW16, varW32, varW64, varF, varD,
         -- * The next functions provide easier access to typed external variables.
         extB, extI8, extI16, extI32, extI64,
         extW8, extW16, extW32, extW64, extF, extD,
@@ -29,21 +27,14 @@
         -- * Set of operators from which to choose during the generation of random streams
         opsF, opsF2, opsF3,
         -- * Constructs of the copilot language
-        var, drop, (++), (.=), (..|), 
-        -- * The next functions are typed variable declarations to help the type-checker.
-        varB, varI8, varI16, varI32, varI64,
-        varW8, varW16, varW32, varW64, varF, varD,
+        drop, (++), (.=), (..|), 
         -- * The next functions help typing the send operations
         -- Warning: there is no typechecking of that yet
         -- sendB, sendI8, sendI16, sendI32, sendI64,
         sendW8, -- , sendW16, sendW32, sendW64, sendF, sendD
-        -- * Typed constant declarations.
-        constB, constI8, constI16, constI32, constI64,
-        constW8, constW16, constW32, constW64, constF, constD,
-        -- * Cast functions (the name tells you what you're casting *into*).
-        castI8, castI16, castI32, castI64,
-        castW8, castW16, castW32, castW64,
-        -- * Constants
+        -- * Safe casting
+        cast,
+        -- * Boolean stream constants
         true, false
     ) where
 
@@ -103,7 +94,8 @@
 
 -- | Cast 'a' into 'b'.  We only allow "safe casts" to larger types.
 class Streamable a => Castable a where
-  cast :: (Streamable b, A.IntegralE b) => Spec a -> Spec b
+  castFrom :: (Streamable b, A.IntegralE b) => Spec a -> Spec b
+  cast :: (Castable b, Streamable b) => Spec b -> Spec a
 
 castErr :: String -> A.Type -> String
 castErr toT fromT = "Error: cannot cast type " P.++ show fromT 
@@ -111,156 +103,84 @@
                     P.++ "not to change sign and to larger types are allowed."
 
 instance Castable Bool where
-  cast = F (\b -> if b then 1 else 0)
+  castFrom = F (\b -> if b then 1 else 0)
            (\b -> A.mux b 1 0)
+  cast x =  error $ castErr "Bool" (getAtomType x)
 
 instance Castable Word8 where
-  cast = F (P.fromInteger . P.toInteger) 
+  castFrom = F (P.fromInteger . P.toInteger) 
            (A.Retype . A.ue)
+  cast x =  case getAtomType x of
+    A.Bool   -> castFrom x
+    t        -> error $ castErr "Word8" t
 
 instance Castable Word16 where
-  cast = F (P.fromInteger . P.toInteger) 
+  castFrom = F (P.fromInteger . P.toInteger) 
            (A.Retype . A.ue)
+  cast x =  case getAtomType x of
+    A.Bool   -> castFrom x
+    A.Word8  -> castFrom x
+    t        -> error $ castErr "Word16" t
 
 instance Castable Word32 where
-  cast = F (P.fromInteger . P.toInteger) 
+  castFrom = F (P.fromInteger . P.toInteger) 
            (A.Retype . A.ue)
+  cast x =  case getAtomType x of
+    A.Bool   -> castFrom x
+    A.Word8  -> castFrom x
+    A.Word16 -> castFrom x
+    t        -> error $ castErr "Word32" t
 
 instance Castable Word64 where
-  cast = F (P.fromInteger . P.toInteger) 
+  castFrom = F (P.fromInteger . P.toInteger) 
            (A.Retype . A.ue)
+  cast x =   case getAtomType x of
+    A.Bool   -> castFrom x
+    A.Word8  -> castFrom x
+    A.Word16 -> castFrom x
+    A.Word32 -> castFrom x
+    t        -> error $ castErr "Word64" t
 
 instance Castable Int8 where
-  cast = F (P.fromInteger . P.toInteger) 
+  castFrom = F (P.fromInteger . P.toInteger) 
            (A.Retype . A.ue)
+  cast x =  case getAtomType x of
+    A.Bool   -> castFrom x
+    t        -> error $ castErr "Int8" t
 
 instance Castable Int16 where
-  cast = F (P.fromInteger . P.toInteger) 
+  castFrom = F (P.fromInteger . P.toInteger) 
            (A.Retype . A.ue)
+  cast x = case getAtomType x of
+    A.Bool   -> castFrom x
+    A.Int8   -> castFrom x
+    A.Word8  -> castFrom x
+    t        -> error $ castErr "Int16" t
 
 instance Castable Int32 where
-  cast = F (P.fromInteger . P.toInteger) 
+  castFrom = F (P.fromInteger . P.toInteger) 
            (A.Retype . A.ue)
+  cast x =  case getAtomType x of
+    A.Bool   -> castFrom x
+    A.Int8  -> castFrom x
+    A.Int16 -> castFrom x
+    A.Word8  -> castFrom x
+    A.Word16  -> castFrom x
+    t        -> error $ castErr "Int32" t
 
 instance Castable Int64 where
-  cast = F (P.fromInteger . P.toInteger) 
+  castFrom = F (P.fromInteger . P.toInteger) 
            (A.Retype . A.ue)
-
-castW8 :: (Streamable a, Castable a) => Spec a -> Spec Word8
-castW8 x = 
-  case getAtomType x of
-    A.Bool   -> cast x
-    t        -> error $ castErr "Word8" t
-
-castW16 :: (Streamable a, Castable a) => Spec a -> Spec Word16
-castW16 x = 
-  case getAtomType x of
-    A.Bool   -> cast x
-    A.Word8  -> cast x
-    t        -> error $ castErr "Word16" t
-
-castW32 :: (Streamable a, Castable a) => Spec a -> Spec Word32
-castW32 x = 
-  case getAtomType x of
-    A.Bool   -> cast x
-    A.Word8  -> cast x
-    A.Word16 -> cast x
-    t        -> error $ castErr "Word32" t
-
-castW64 :: (Streamable a, Castable a) => Spec a -> Spec Word64
-castW64 x = 
-  case getAtomType x of
-    A.Bool   -> cast x
-    A.Word8  -> cast x
-    A.Word16 -> cast x
-    A.Word32 -> cast x
-    t        -> error $ castErr "Word64" t
-
-castI8 :: (Streamable a, Castable a) => Spec a -> Spec Int8
-castI8 x = 
-  case getAtomType x of
-    A.Bool   -> cast x
-    t        -> error $ castErr "Int8" t
-
-castI16 :: (Streamable a, Castable a) => Spec a -> Spec Int16
-castI16 x = 
-  case getAtomType x of
-    A.Bool   -> cast x
-    A.Int8   -> cast x
-    A.Word8  -> cast x
-    t        -> error $ castErr "Int16" t
-
-castI32 :: (Streamable a, Castable a) => Spec a -> Spec Int32
-castI32 x = 
-  case getAtomType x of
-    A.Bool   -> cast x
-    A.Int8  -> cast x
-    A.Int16 -> cast x
-    A.Word8  -> cast x
-    A.Word16  -> cast x
-    t        -> error $ castErr "Int32" t
-
-castI64 :: (Streamable a, Castable a) => Spec a -> Spec Int64
-castI64 x = 
-  case getAtomType x of
-    A.Bool   -> cast x
-    A.Int8  -> cast x
-    A.Int16 -> cast x
-    A.Int32 -> cast x
-    A.Word8  -> cast x
-    A.Word16  -> cast x
-    A.Word32  -> cast x
+  cast x =  case getAtomType x of
+    A.Bool   -> castFrom x
+    A.Int8  -> castFrom x
+    A.Int16 -> castFrom x
+    A.Int32 -> castFrom x
+    A.Word8  -> castFrom x
+    A.Word16  -> castFrom x
+    A.Word32  -> castFrom x
     t        -> error $ castErr "Int64" t
 
--- F (P.fromInteger . P.toInteger) 
---             (A.Retype . A.ue . (`A.mod_` (size 16))
---                . A.Retype . A.ue)
-
-
--- instance CastIntTo Word8 where
---     cast = F (P.fromInteger . P.toInteger) 
---              (A.Retype . A.ue . (`A.mod_` (size 8))
---                  . A.Retype . A.ue)
--- instance CastIntTo Word16 where
---     cast = F (P.fromInteger . P.toInteger) 
---              (A.Retype . A.ue . (`A.mod_` (size 16))
---                  . A.Retype . A.ue)
--- instance CastIntTo Word32 where
---     cast = F (P.fromInteger . P.toInteger) 
---              (A.Retype . A.ue . (`A.mod_` (size 32))
---                  . A.Retype . A.ue)
--- instance CastIntTo Word64 where
---     cast = F (P.fromInteger . P.toInteger) 
---              (A.Retype . A.ue . (`A.mod_` (size 64))
---                  . A.Retype . A.ue)
-
--- Ints
-
--- XXX this is how Robin had casts.  Can't we do it more simply?
--- instance CastIntTo Int8 where
---     cast = F (P.fromInteger . P.toInteger) 
---              (A.Retype . A.ue . 
---                  (\x -> ((x P.+ sMinOne) `A.mod_` s) P.-  s)
---                    . A.Retype . A.ue)
---       where s = size 8
---             sMinOne = size 7
--- instance CastIntTo Int8 where
---     cast = F (P.fromInteger . P.toInteger) 
---              (A.Retype . A.ue . (`A.mod_` (size 7)) 
---                    . A.Retype . A.ue)
--- instance CastIntTo Int16 where
---     cast = F (P.fromInteger . P.toInteger) 
---              (A.Retype . A.ue . (`A.mod_` (size 15)) 
---                    . A.Retype . A.ue)
--- instance CastIntTo Int32 where
---     cast = F (P.fromInteger . P.toInteger) 
---              (A.Retype . A.ue . (`A.mod_` (size 31)) 
---                    . A.Retype . A.ue)
--- instance CastIntTo Int64 where
---     cast = F (P.fromInteger . P.toInteger) 
---              (A.Retype . A.ue . (`A.mod_` (size 63))
---                    . A.Retype . A.ue)
-
 -- | Beware : both sides are executed, even if the result of one is later discarded
 mux :: (Streamable a) => Spec Bool -> Spec a -> Spec a -> Spec a
 mux = F3 (\ b x y -> if b then x else y) A.mux
@@ -268,29 +188,6 @@
 infix 5 ==, /=, <, <=, >=, >
 infixr 4 ||, &&, ^, ==>
 
--- Used for helping ghc in infering the type of the streams
-bool :: Spec Bool -> Spec Bool
-int8 :: Spec Int8 -> Spec Int8
-int16 :: Spec Int16 -> Spec Int16
-int32 :: Spec Int32 -> Spec Int32
-int64 :: Spec Int64 -> Spec Int64
-word8 :: Spec Word8 -> Spec Word8
-word16 :: Spec Word16 -> Spec Word16
-word32 :: Spec Word32 -> Spec Word32
-word64 :: Spec Word64 -> Spec Word64
-float :: Spec Float -> Spec Float
-double :: Spec Double -> Spec Double
-bool = P.id
-int8 = P.id
-int16 = P.id
-int32 = P.id
-int64 = P.id
-word8 = P.id
-word16 = P.id
-word32 = P.id
-word64 = P.id
-float = P.id
-double = P.id
 
 -- Used for easily producing, and coercing PVars
 
@@ -319,28 +216,28 @@
 extD = PVar A.Double
 
 -- for arrays 
-extArrB :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Bool
-extArrB = \(v, idx) ph -> PArr A.Bool (v, idx) ph
-extArrI8 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int8
-extArrI8 = \(v, idx) ph -> PArr A.Int8 (v, idx) ph
-extArrI16 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int16
-extArrI16 = \(v, idx) ph -> PArr A.Int16 (v, idx) ph
-extArrI32 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int32
-extArrI32 = \(v, idx) ph -> PArr A.Int32 (v, idx) ph
-extArrI64 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int64
-extArrI64 = \(v, idx) ph -> PArr A.Int64 (v, idx) ph
-extArrW8 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word8
-extArrW8 = \(v, idx) ph -> PArr A.Word8 (v, idx) ph
-extArrW16 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word16
-extArrW16 = \(v, idx) ph -> PArr A.Word16 (v, idx) ph
-extArrW32 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word32
-extArrW32 = \(v, idx) ph -> PArr A.Word32 (v, idx) ph
-extArrW64 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word64
-extArrW64 = \(v, idx) ph -> PArr A.Word64 (v, idx) ph
-extArrF :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Float
-extArrF = \(v, idx) ph -> PArr A.Float (v, idx) ph
-extArrD :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Double
-extArrD = \(v, idx) ph -> PArr A.Double (v, idx) ph
+extArrB ::  (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Bool
+extArrB = \v idx ph -> PArr A.Bool (v, idx) ph
+extArrI8 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int8
+extArrI8 = \v idx ph -> PArr A.Int8 (v, idx) ph
+extArrI16 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int16
+extArrI16 = \v idx ph -> PArr A.Int16 (v, idx) ph
+extArrI32 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int32
+extArrI32 = \v idx ph -> PArr A.Int32 (v, idx) ph
+extArrI64 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int64
+extArrI64 = \v idx ph -> PArr A.Int64 (v, idx) ph
+extArrW8 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word8
+extArrW8 = \v idx ph -> PArr A.Word8 (v, idx) ph
+extArrW16 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word16
+extArrW16 = \v idx ph -> PArr A.Word16 (v, idx) ph
+extArrW32 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word32
+extArrW32 = \v idx ph -> PArr A.Word32 (v, idx) ph
+extArrW64 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word64
+extArrW64 = \v idx ph -> PArr A.Word64 (v, idx) ph
+extArrF :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Float
+extArrF = \v idx ph -> PArr A.Float (v, idx) ph
+extArrD :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Double
+extArrD = \v idx ph -> PArr A.Double (v, idx) ph
 
 
 ---- Sets of operators for Tests.Random.hs -------------------------------------
@@ -532,11 +429,9 @@
 
 ---- Constructs of the language ------------------------------------------------
 
--- | Stream variable reference
-var :: Streamable a => Var -> Spec a
-var v = Var v
 
--- If a generic 'var' declaration is insufficient for the type-checker to determine the type, a monomorphic var operator can be used
+-- If a generic 'var' declaration is insufficient for the type-checker to
+-- determine the type, a monomorphic var operator can be used.
 varB :: Var -> Spec Bool
 varB = Var
 varI8 :: Var -> Spec Int8
@@ -571,8 +466,12 @@
 sendI32 v (ph, port) = Send (v, ph, port)
 sendI64 :: Var -> (Phase, Port) -> Send Int64
 sendI64 v (ph, port) = Send (v, ph, port) -}
-sendW8 :: Var -> (Phase, Port) -> Send Word8
-sendW8 v (ph, port) = Send (v, ph, port)
+sendW8 :: Spec Word8 -> (Phase, Port) -> Send Word8
+sendW8 s (ph, port) = 
+  case s of
+    Var v -> Send (v, ph, port)
+    _     -> error $ "You provided spec " P.++ show s 
+                P.++ " where you needed to give a variable."
 {- sendW16 :: Var -> (Phase, Port) -> Send Word16
 sendW16 v (ph, port) = Send (v, ph, port)
 sendW32 :: Var -> (Phase, Port) -> Send Word32
@@ -585,36 +484,9 @@
 sendD v (ph, port) = Send (v, ph, port) -}
 
 
-
-constB :: Bool -> Spec Bool
-constB = Const
-
 true, false :: Spec Bool
-true = constB True
-false = constB False
-
--- | Constant streams
-constI8 :: Int8 -> Spec Int8
-constI8 = Const
-constI16 :: Int16 -> Spec Int16
-constI16 = Const
-constI32 :: Int32 -> Spec Int32
-constI32 = Const
-constI64 :: Int64 -> Spec Int64
-constI64 = Const
-constW8 :: Word8 -> Spec Word8
-constW8 = Const 
-constW16 :: Word16 -> Spec Word16
-constW16 = Const
-constW32 :: Word32 -> Spec Word32
-constW32 = Const
-constW64 :: Word64 -> Spec Word64
-constW64 = Const
-constF :: Float -> Spec Float
-constF = Const
-constD :: Double -> Spec Double
-constD = Const
-
+true = Const True
+false = Const False
 
 -- | Drop @i@ elements from a stream.
 drop :: Streamable a => Int -> Spec a -> Spec a
@@ -625,8 +497,12 @@
 ls ++ s = Append ls s
 
 -- | Define a stream variable.
-(.=) :: Streamable a => Var -> Spec a -> Streams
-v .= s = tell (updateSubMap (M.insert v s) emptySM) 
+(.=) :: Streamable a => Spec a -> Spec a -> Streams
+v .= s = 
+  case v of
+    Var var -> tell (updateSubMap (M.insert var s) emptySM) 
+    _       -> error $ "Copilot error: you tried to use specification " P.++ show v 
+                 P.++ " where you need to use a variable."
 
 -- | Allows to build a @'Sends'@ from specification
 (..|) :: Sendable a => Send a -> Sends -> Sends
diff --git a/Language/Copilot/Libs/LTL.hs b/Language/Copilot/Libs/LTL.hs
--- a/Language/Copilot/Libs/LTL.hs
+++ b/Language/Copilot/Libs/LTL.hs
@@ -27,7 +27,7 @@
   ) 
   where
 
-import Prelude (Int, ($), String)
+import Prelude (Int, ($), String, error)
 import qualified Prelude as P
 import Data.List (foldl1)
 
@@ -36,11 +36,14 @@
 import Language.Copilot.Libs.Indexes
 import Language.Copilot.Libs.ErrorChks
 
-ltl :: Var -> (Var -> Streams) -> Streams
+ltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams
 ltl v f = f v
 
-tmpName :: Var -> String -> Var
-tmpName v name = v P.++ "_" P.++ name
+tmpName :: Spec Bool -> String -> Spec Bool
+tmpName v name = 
+  case v of 
+    Var var -> varB (var P.++ "_" P.++ name)
+    _       -> error $ "Copilot: " P.++ "error in tmpName in LTL.hs."
 
 -- | Property @s@ holds for the next @n@ periods.  We require @n >= 0@. If @n ==
 -- 0@, then @s@ holds in the current period.  E.g., if @p = always 2 s@, then we
@@ -50,9 +53,9 @@
 -- s => T T T F T T T T ...
 -- p => T F F F T T ...
 -- @
-always :: Int -> Spec Bool -> Var -> Streams
+always :: Int -> Spec Bool -> Spec Bool -> Streams
 always n s v = do
-  v .= (nPosChk "always" n $ foldl1 (&&) [drop x (varB s') | x <- [0..n]])
+  v .= (nPosChk "always" n $ foldl1 (&&) [drop x s' | x <- [0..n]])
   s' .= s
   where s' = tmpName v "always"
 
@@ -63,9 +66,9 @@
 -- next s => F F T F F T F ...
 -- @
 -- Note: s must have sufficient history to drop a value from it.
-next :: Spec Bool -> Var -> Streams
+next :: Spec Bool -> Spec Bool -> Streams
 next s v = do 
-  v  .= drop 1 (varB s')
+  v  .= drop 1 s'
   s' .= s
   where s' = tmpName v "next"
 
@@ -77,21 +80,21 @@
 -- s => F F F T F F F T ...
 -- p => F T T T F T T T ...
 -- @
-eventually :: Int -> Spec Bool -> Var -> Streams
+eventually :: Int -> Spec Bool -> Spec Bool -> Streams
 eventually n s v = do
-  v .= (nPosChk "eventually" n $ foldl1 (||) [drop x (varB s') | x <- [0..n]])
+  v .= (nPosChk "eventually" n $ foldl1 (||) [drop x s' | x <- [0..n]])
   s' .= s
   where s' = tmpName v "eventually"
 
 -- | @until n s0 s1@ means that @eventually n s1@, and up until at least the
 -- period before @s1@ holds, @s0@ continuously holds.
-until :: Int -> Spec Bool -> Spec Bool -> Var -> Streams
+until :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams
 until n s0 s1 v = do
   v'  .= (nPosChk "until" n $ 
             (   (whenS0 < 0) -- s0 didn't fail within n periods.
-             || (soonest n (varB s1') <= whenS0))) -- s0 failed at some point before n.
-  v'' `ltl` eventually n (varB s1') -- guarantees that soonest n s1 >= 0
-  v   .= (varB v') && (varB v'')
+             || (soonest n s1' <= whenS0))) -- s0 failed at some point before n.
+  v'' `ltl` eventually n s1' -- guarantees that soonest n s1 >= 0
+  v   .= v' && v''
   s0' .= s0
   s1' .= s1
   where 
@@ -99,18 +102,18 @@
     s1' = tmpName v "until_1"
     v''  = tmpName v "until_2"
     v' = tmpName v "until3"
-    whenS0 = soonestFail n (varB s0')
+    whenS0 = soonestFail n s0'
 
 -- | @release n s0 s1@ means that either @always n s1@, or @s1@ holds up to and
 -- including the period at which @s0@ becomes true.
-release :: Int -> Spec Bool -> Spec Bool -> Var -> Streams
+release :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams
 release n s0 s1 v = do
   v' .= (nPosChk "release" n $ (   (whenS0 >= 0) -- s0 becomes true at some point
                                 && (whenS0 < whenS1))) -- and when s0 becomes true,
                                                        -- is strictly sooner than
                                                        -- when s1 fails.
-  v'' `ltl` always n (varB s1') -- s1 never fails
-  v   .= (varB v') || (varB v'')
+  v'' `ltl` always n s1' -- s1 never fails
+  v   .= v' || v''
   s0' .= s0
   s1' .= s1
   where 
@@ -118,5 +121,5 @@
     s1' = tmpName v "release1"
     v''  = tmpName v "release2"
     v' = tmpName v "release3"
-    whenS1 = soonestFail n (varB s1')
-    whenS0 = soonest n (varB s0')
+    whenS1 = soonestFail n s1'
+    whenS0 = soonest n s0'
diff --git a/Language/Copilot/Libs/PTLTL.hs b/Language/Copilot/Libs/PTLTL.hs
--- a/Language/Copilot/Libs/PTLTL.hs
+++ b/Language/Copilot/Libs/PTLTL.hs
@@ -13,47 +13,50 @@
   ( ptltl, since, alwaysBeen, eventuallyPrev, previous ) 
   where
 
-import Prelude (String, ($))
+import Prelude (String, ($), error)
 import qualified Prelude as P
 
 import Language.Copilot.Core
 import Language.Copilot.Language
 
-tmpName :: Var -> String -> Var
-tmpName v name = v P.++ "_" P.++ name
+tmpName :: Spec Bool -> String -> Spec Bool
+tmpName v name = 
+  case v of
+    Var var -> varB (var P.++ "_" P.++ name)
+    _       -> error "Copilot error in tmpName in PTLTL.hs."
 
-ptltl :: Var -> (Var -> Streams) -> Streams
+ptltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams
 ptltl v f = f v
 
 -- | Did @s@ hold in the previous period?
-previous :: Spec Bool -> Var -> Streams
+previous :: Spec Bool -> Spec Bool -> Streams
 previous s v = v .= [False] ++ s  
 
 -- | Has @s@ always held (up to and including the current state)?
-alwaysBeen :: Spec Bool -> Var -> Streams
+alwaysBeen :: Spec Bool -> Spec Bool -> Streams
 alwaysBeen s v = do
-     tmp .= [True] ++ varB v
-     v   .= varB tmp && varB s'
+     tmp .= [True] ++ v
+     v   .= tmp && s'
      s'  .= s
   where 
     tmp = tmpName v "ab_tmp"
     s'  = tmpName v "ab"
     
 -- | Did @s@ hold at some time in the past (including the current state)?
-eventuallyPrev :: Spec Bool -> Var -> Streams
+eventuallyPrev :: Spec Bool -> Spec Bool -> Streams
 eventuallyPrev s v = do
-     tmp .= [False] ++ (var tmp) || varB s'
-     v   .= varB s' || varB tmp
+     tmp .= [False] ++ tmp || s'
+     v   .= s' || tmp
      s'  .= s
   where 
     tmp = tmpName v "ep_tmp"
     s'  = tmpName v "ep"
 
 -- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold? 
-since ::  Spec Bool -> Spec Bool -> Var -> Streams
+since ::  Spec Bool -> Spec Bool -> Spec Bool -> Streams
 since s1 s2 v = do
     tmp `ptltl` (eventuallyPrev $ [False] ++ s2) -- has s2 been true at some point?
-    v   `ptltl` (alwaysBeen $ varB tmp ==> varB s1')
+    v   `ptltl` (alwaysBeen $ tmp ==> s1')
     s1' .= s1
     s2' .= s2
   where 
diff --git a/Language/Copilot/Variables.hs b/Language/Copilot/Variables.hs
deleted file mode 100644
--- a/Language/Copilot/Variables.hs
+++ /dev/null
@@ -1,32 +0,0 @@
--- | Variable names
-
-module Language.Copilot.Variables where
-
-a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z :: String
-
-a = "a"
-b = "b"
-c = "c"
-d = "d"
-e = "e"
-f = "f"
-g = "g"
-h = "h"
-i = "i"
-j = "j"
-k = "k"
-l = "l"
-m = "m"
-n = "n"
-o = "o"
-p = "p"
-q = "q"
-r = "r"
-s = "s"
-t = "t"
-u = "u"
-v = "v"
-w = "w"
-x = "x"
-y = "y"
-z = "z"
diff --git a/README b/README
--- a/README
+++ b/README
@@ -4,13 +4,14 @@
 Copilot. Here's a Copilot program that computes the Fibonacci sequence (over
 Word 64s) and tests for even numbers:
 
-
 fib :: Streams
 fib = do
-  "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")
-  "t" .= even (var "fib")
+  let f = varW64 "f"
+  let t   = varB "t"
+  f .= [0,1] ++ f + (drop 1 f)
+  t .= even f
     where even :: Spec Word64 -> Spec Bool
-          even w = w `mod` const 2 == const 0    
+          even w' = w' `mod` 2 == 0
 
 Copilot contains an interpreter, a compiler, and uses a model-checker to check
 the correctness of your program. The compiler generates constant time and
@@ -34,6 +35,11 @@
 
 *******************************************************************************
 Release notes
+
+* Copilot-0.26
+  * Variables are now specs, not strings.  This gives stream expressions a type,
+    so no need for constant functions, monomorphic cast functions, or var
+    annotations in expressions.  Examples updated to reflect the change.
 
 * Copilot-0.25
 
diff --git a/copilot.cabal b/copilot.cabal
--- a/copilot.cabal
+++ b/copilot.cabal
@@ -1,5 +1,5 @@
 name:                copilot
-version:             0.25
+version:             0.26
 cabal-version:       >= 1.2
 license:             BSD3
 license-file:        LICENSE
@@ -15,10 +15,12 @@
                      .
                      > fib :: Streams
                      > fib = do
-                     >  "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")
-                     >  "t" .= even (var "fib")
-                     >    where even :: Spec Word64 -> Spec Bool
-                     >          even w = w `mod` const 2 == const 0    
+                     >  let f = varW64 "fib"
+                     >  let t = varB "t"
+                     >  f .= [0,1] ++ f + (drop 1 f)
+                     >  t .= even f
+                     >    where even :: Spaec Word64 -> Spec Bool
+                     >          even w' = w' `mod` 2 == 0
                      .
                      Copilot contains an interpreter, a compiler, and uses a model-checker to check
                      the correctness of your program. The compiler generates constant time and
@@ -56,7 +58,6 @@
                      Language.Copilot.Tests.Random
                      Language.Copilot.Dispatch
                      Language.Copilot.Interface
-                     Language.Copilot.Variables
                      Language.Copilot.Libs.ErrorChks
                      Language.Copilot.Libs.PTLTL
                      Language.Copilot.Libs.LTL