diff --git a/copilot-core.cabal b/copilot-core.cabal
--- a/copilot-core.cabal
+++ b/copilot-core.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-core
-version:             0.2.1
+version:             0.2.2
 synopsis:            An intermediate representation for Copilot.
 description:         Intermediate representation for Copilot.
                      Strictly follows Haskell 2010 except for universal
@@ -62,7 +62,8 @@
     Copilot.Core.Type
     Copilot.Core.Type.Dynamic
     Copilot.Core.Type.Equality
+    Copilot.Core.Type.Eq
     Copilot.Core.Type.Show
+    Copilot.Core.Type.Read
     Copilot.Core.Type.Uninitialized
     Copilot.Core.PrettyPrint
-    Copilot.Core.Version
diff --git a/src/Copilot/Compile/Header/C99.hs b/src/Copilot/Compile/Header/C99.hs
--- a/src/Copilot/Compile/Header/C99.hs
+++ b/src/Copilot/Compile/Header/C99.hs
@@ -13,7 +13,6 @@
   ) where
 
 import Copilot.Core
-import Copilot.Core.Version
 import Data.List (intersperse, nubBy)
 import Text.PrettyPrint.HughesPJ
 import Prelude hiding (unlines)
@@ -36,7 +35,7 @@
 
 c99Header :: String -> Spec -> String
 c99Header prefix spec = render $ vcat $
-  [ text "/* Generated by Copilot Core v." <+> text version <+> text "*/"
+  [ text "/* Generated by Copilot Core." <+> text "*/"
   , text ""
   , ppHeaders
   , text ""
@@ -104,9 +103,8 @@
           text "(" <> ppArgs args <> text ");"
 
     where
-
     ppArgs :: [UExpr] -> Doc
-    ppArgs = vcat . intersperse (text ",") . map ppArg
+    ppArgs = hcat . intersperse (text ", ") . map ppArg
 
     ppArg :: UExpr -> Doc
     ppArg UExpr { uExprType = t } = text (typeSpec (UType t))
@@ -136,10 +134,13 @@
 ppExternalArray :: ExtArray -> Doc
 ppExternalArray
   ExtArray
-    { externArrayName = name
-    , externArrayElemType = t } =
-        text "extern" <+> text (typeSpec (UType t)) <+> text "*" <+>
-        text name <> text ";"
+    { externArrayName     = name
+    , externArrayElemType = t 
+    , externArraySize     = size } 
+  =
+        text "extern" <+> text (typeSpec (UType t)) 
+        <+> text name <> lbrack <> int size <> rbrack
+        <> text ";"
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Copilot/Core/Error.hs b/src/Copilot/Core/Error.hs
--- a/src/Copilot/Core/Error.hs
+++ b/src/Copilot/Core/Error.hs
@@ -8,9 +8,10 @@
 
 impossible :: String -> String -> a
 impossible function package = 
-  error $ "Impossible error in function " ++ function ++ ", in package " ++ 
-    package ++ ".  Please email Lee Pike at <lee pike @ gmail . com> " ++
-    "(remove spaces) or file a bug report on github.com."
+  error $ "\"Impossible\" error in function " 
+    ++ function ++ ", in package " ++ package 
+    ++ ".  Please email Lee Pike at <lee pike @ gmail . com> " ++
+       "(remove spaces) or file a bug report on github.com."
 
 badUsage :: String -> a
-badUsage msg = error $ "Copilot error: " ++ msg ++ "."
+badUsage msg = error $ "Copilot error: " ++ msg
diff --git a/src/Copilot/Core/Expr.hs b/src/Copilot/Core/Expr.hs
--- a/src/Copilot/Core/Expr.hs
+++ b/src/Copilot/Core/Expr.hs
@@ -40,63 +40,22 @@
 --------------------------------------------------------------------------------
 
 data Expr a where
-  Const
-    :: Type a
-    -> a
-    -> Expr a
-  Drop
-    :: Type a
-    -> DropIdx
-    -> Id
-    -> Expr a
-  Local
-    :: Type a
-    -> Type b
-    -> Name
-    -> Expr a
-    -> Expr b
-    -> Expr b
-  Var
-    :: Type a
-    -> Name
-    -> Expr a
-  ExternVar
-    :: Type a
-    -> Name
-    -> Expr a
-  ExternFun
-    :: Type a
-    -> Name
-    -> [UExpr]
-    -> Maybe Tag
-    -> Expr a
-  ExternArray
-    :: Integral a
-    => Type a
-    -> Type b
-    -> Name
-    -> Expr a
-    -> Maybe Tag
-    -> Expr b
-  Op1
-    :: Op1 a b
-    -> Expr a
-    -> Expr b
-  Op2
-    :: Op2 a b c
-    -> Expr a
-    -> Expr b
-    -> Expr c
-  Op3
-    :: Op3 a b c d
-    -> Expr a
-    -> Expr b
-    -> Expr c
-    -> Expr d
+  Const        :: Type a -> a -> Expr a
+  Drop         :: Type a -> DropIdx -> Id -> Expr a
+  Local        :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b
+  Var          :: Type a -> Name -> Expr a 
+  ExternVar    :: Type a -> Name -> Maybe [a] -> Expr a 
+  ExternFun    :: Type a -> Name -> [UExpr] -> Maybe (Expr a) 
+               -> Maybe Tag -> Expr a
+  ExternArray  :: Integral a => Type a -> Type b -> Name -> Int -> Expr a
+               -> Maybe [[b]] -> Maybe Tag -> Expr b 
+  Op1          :: Op1 a b -> Expr a -> Expr b 
+  Op2          :: Op2 a b c -> Expr a -> Expr b -> Expr c
+  Op3          :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d
 
 --------------------------------------------------------------------------------
 
 -- | A untyped expression (no phantom type).
-data UExpr = forall a . UExpr
+data UExpr = forall a. UExpr
   { uExprType :: Type a
   , uExprExpr :: Expr a }
diff --git a/src/Copilot/Core/External.hs b/src/Copilot/Core/External.hs
--- a/src/Copilot/Core/External.hs
+++ b/src/Copilot/Core/External.hs
@@ -28,6 +28,7 @@
   , externArrayElemType :: Type b
   , externArrayIdx      :: Expr a
   , externArrayIdxType  :: Type a
+  , externArraySize     :: Int
   , externArrayTag      :: Maybe Tag }
 
 data ExtFun = forall a . ExtFun
@@ -49,18 +50,18 @@
 
 externVarsExpr :: Expr a -> DList ExtVar
 externVarsExpr e0 = case e0 of
-  Const  _ _            -> empty
-  Drop   _ _ _          -> empty
-  Local _ _ _ e1 e2     -> externVarsExpr e1 `append` externVarsExpr e2
-  Var _ _               -> empty
-  ExternVar t name      -> singleton (ExtVar name (UType t))
-  ExternArray _ _ _ e _ -> externVarsExpr e
-  ExternFun _ _ ues _   -> concat (map externVarsUExpr ues)
-  Op1 _ e               -> externVarsExpr e
-  Op2 _ e1 e2           -> externVarsExpr e1 `append` externVarsExpr e2
-  Op3 _ e1 e2 e3        -> externVarsExpr e1 `append`
-                           externVarsExpr e2 `append`
-                           externVarsExpr e3
+  Const  _ _                -> empty
+  Drop   _ _ _              -> empty
+  Local _ _ _ e1 e2         -> externVarsExpr e1 `append` externVarsExpr e2
+  Var _ _                   -> empty
+  ExternVar t name _        -> singleton (ExtVar name (UType t))
+  ExternArray _ _ _ _ e _ _ -> externVarsExpr e
+  ExternFun _ _ ues _ _     -> concat (map externVarsUExpr ues)
+  Op1 _ e                   -> externVarsExpr e
+  Op2 _ e1 e2               -> externVarsExpr e1 `append` externVarsExpr e2
+  Op3 _ e1 e2 e3            -> externVarsExpr e1 `append`
+                               externVarsExpr e2 `append`
+                               externVarsExpr e3
 
 externVarsUExpr :: UExpr -> DList ExtVar
 externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e
@@ -76,9 +77,10 @@
   Drop   _ _ _                    -> empty
   Local _ _ _ e1 e2               -> externArraysExpr e1 `append` externArraysExpr e2
   Var _ _                         -> empty
-  ExternVar _ _                   -> empty
-  ExternArray t1 t2  name idx tag -> singleton (ExtArray name t2 idx t1 tag)
-  ExternFun _ _ ues _             -> concat (map externArraysUExpr ues)
+  ExternVar _ _ _                 -> empty
+  ExternArray t1 t2  name 
+              size idx _ tag      -> singleton (ExtArray name t2 idx t1 size tag)
+  ExternFun _ _ ues _ _           -> concat (map externArraysUExpr ues)
   Op1 _ e                         -> externArraysExpr e
   Op2 _ e1 e2                     -> externArraysExpr e1 `append` externArraysExpr e2
   Op3 _ e1 e2 e3                  -> externArraysExpr e1 `append`
@@ -99,9 +101,9 @@
   Drop   _ _ _                -> empty
   Local _ _ _ e1 e2           -> externFunsExpr e1 `append` externFunsExpr e2
   Var _ _                     -> empty
-  ExternVar _ _               -> empty
-  ExternArray _ _ _ idx _     -> externFunsExpr idx
-  ExternFun t name ues tag    -> singleton (ExtFun name t ues tag)
+  ExternVar _ _ _             -> empty
+  ExternArray _ _ _ _ idx _ _ -> externFunsExpr idx
+  ExternFun t name ues _ tag  -> singleton (ExtFun name t ues tag)
   Op1 _ e                     -> externFunsExpr e
   Op2 _ e1 e2                 -> externFunsExpr e1 `append` externFunsExpr e2
   Op3 _ e1 e2 e3              -> externFunsExpr e1 `append`
diff --git a/src/Copilot/Core/Interpret.hs b/src/Copilot/Core/Interpret.hs
--- a/src/Copilot/Core/Interpret.hs
+++ b/src/Copilot/Core/Interpret.hs
@@ -5,8 +5,8 @@
 -- | An interpreter for Copilot specifications.
 
 module Copilot.Core.Interpret
-  ( ExtEnv (..)
-  , Format (..)
+  ( --ExtEnv (..)
+    Format (..)
   , interpret
   ) where
 
@@ -18,10 +18,9 @@
 data Format = Table | CSV
 
 -- | Interprets a Copilot specification.
-interpret :: Format -> Int -> ExtEnv -> Spec -> String
-interpret format k exts spec =
+interpret :: Format -> Int -> Spec -> String
+interpret format k spec =
   case format of
     Table -> renderAsTable e
     CSV   -> renderAsCSV e
-
-  where e = eval Haskell k exts spec
+  where e = eval Haskell k spec
diff --git a/src/Copilot/Core/Interpret/Eval.hs b/src/Copilot/Core/Interpret/Eval.hs
--- a/src/Copilot/Core/Interpret/Eval.hs
+++ b/src/Copilot/Core/Interpret/Eval.hs
@@ -4,11 +4,11 @@
 
 -- | A tagless interpreter for Copilot specifications.
 
-{-# LANGUAGE GADTs, BangPatterns #-}
+{-# LANGUAGE GADTs, BangPatterns, DeriveDataTypeable #-}
 
 module Copilot.Core.Interpret.Eval
-  ( ExtEnv (..)
-  , Env 
+  ( --ExtEnv (..)
+    Env 
   , Output
   , ExecTrace (..)
   , eval
@@ -18,27 +18,81 @@
 import Copilot.Core.Type.Dynamic
 import Copilot.Core.Type.Show (showWithType, ShowType)
 
+import Prelude hiding (id)
+import qualified Prelude as P
+
 import Data.List (transpose)
 import qualified Data.Map as M
 import Data.Map (Map)
-import Data.Maybe (fromJust, catMaybes)
+import Data.Maybe (fromJust)
 import Data.Bits
+import Control.Exception (Exception, throw)
+import Data.Typeable
 
-import Prelude hiding (id)
-import qualified Prelude as P
+--------------------------------------------------------------------------------
 
+data InterpException
+  = -- NoValues Name
+--  | BadType Name
+    ArrayWrongSize Name Int 
+  | ArrayIdxOutofBounds Name Int Int
+  | DivideByZero
+  | NotEnoughValues Name Int
+--  | NoExtFunEval Name
+  | NoExtsInterp Name
+  deriving Typeable
+
+instance Show InterpException where
+  ---------------------------------------
+  -- show (NoValues name)                                                         =
+  --   badUsage $ "you need to supply a list of values for interpreting "
+  --     ++ "external element " ++ name ++ "."
+  ---------------------------------------
+
+  -- -- Should always be caught by Analyze.hs in copilot-language.
+  -- show (BadType name)                                                          =
+  --   badUsage $ "you probably gave the wrong type for external element " 
+  --     ++ name ++ ".  Recheck your types and re-evaluate."
+  ---------------------------------------
+  show (ArrayWrongSize name expectedSize)                                      =
+    badUsage $ "in the environment for external array " ++ name 
+      ++ ", we expect a list of length " ++ show expectedSize 
+      ++ ", but the length of the array you supplied is of a different length."
+  ---------------------------------------
+  show (ArrayIdxOutofBounds name index size)                                   =
+    badUsage $ "in the environment for external array " ++ name 
+      ++ ", you gave an index of " ++ show index 
+      ++ " where the size of the array is " ++ show size ++ "; the size must "
+      ++ " be strictly greater than the index."
+  ---------------------------------------
+  show DivideByZero                                                            =
+    badUsage "divide by zero."
+  ---------------------------------------
+  show (NotEnoughValues name k)                                                =
+    badUsage $ "on the " ++ show k ++ "th iteration, we ran out of "
+      ++ "values for simulating the external element " ++ name ++ "."
+  ---------------------------------------
+  show (NoExtsInterp name)                                                     =
+    badUsage $ "in a call of external symbol " ++ name ++ ", you did not "
+      ++ "provide an expression for interpretation.  In your external "
+      ++ "declaration, you need to provide a 'Just strm', where 'strm' is "
+      ++ "some stream with which to simulate the function."
+  ---------------------------------------
+
+instance Exception InterpException
+
 --------------------------------------------------------------------------------
 
 type Env nm = [(nm, DynamicF [] Type)]
 
--- | External arrays environment.
-type ArrEnv = [(Name, [DynamicF [] Type])] 
+-- -- | External arrays environment.
+-- type ArrEnv = [(Name, [DynamicF [] Type])] 
 
--- | Environment for simulation.
-data ExtEnv = ExtEnv { varEnv  :: Env Name
-                     , arrEnv  :: ArrEnv 
-                     , funcEnv :: [(Name, Spec)] 
-                     }
+-- -- | Environment for simulation.
+-- data ExtEnv = ExtEnv { varEnv  :: Env Name
+--                      , arrEnv  :: ArrEnv 
+-- --                     , funcEnv :: [(Name, Spec)] 
+--                      }
 
 --------------------------------------------------------------------------------
 
@@ -46,8 +100,9 @@
 
 data ExecTrace = ExecTrace
     -- map from trigger names to their maybe output, which is a list of strings
-    -- representing their valus.  (Nothing output if the guard for the trigger
-    -- is false).
+    -- representing their values.  (Nothing output if the guard for the trigger
+    -- is false).  The order is important, since we compare the arg lists
+    -- between the interpreter and backends.
   { interpTriggers  :: Map String [Maybe [Output]]
     -- map from observer names to their outputs.  We also show observer outputs.
   , interpObservers :: Map String [Output] }
@@ -74,18 +129,18 @@
 -- We could write this in a beautiful lazy style like above, but that creates a
 -- space leak in the interpreter that is hard to fix while maintaining laziness.
 -- We take a more brute-force appraoch below.
-eval :: ShowType -> Int -> ExtEnv -> Spec -> ExecTrace
-eval showType k exts spec =
+eval :: ShowType -> Int -> Spec -> ExecTrace
+eval showType k spec =
 --  let exts  = take k $ reverse exts'                          in
 
   let initStrms = map initStrm (specStreams spec)             in
 
-  let strms = evalStreams k exts (specStreams spec) initStrms in
+  let strms = evalStreams k (specStreams spec) initStrms      in
 
-  let trigs = map (evalTrigger showType k exts strms) 
+  let trigs = map (evalTrigger showType k strms) 
                   (specTriggers spec)                         in
 
-  let obsvs = map (evalObserver showType k exts strms) 
+  let obsvs = map (evalObserver showType k strms) 
                   (specObservers spec)                        in 
 
   strms `seq` ExecTrace
@@ -99,87 +154,93 @@
 
 type LocalEnv = [(Name, Dynamic Type)]
 
-evalExpr_ :: Int -> Expr a -> ExtEnv -> LocalEnv -> Env Id -> a
-evalExpr_ k e0 exts locs strms = case e0 of
-  Const _ x              -> x 
-  Drop t i id            -> 
+evalExpr_ :: Int -> Expr a -> LocalEnv -> Env Id -> a
+evalExpr_ k e0 locs strms = case e0 of
+  Const _ x                          -> x 
+  Drop t i id                        -> 
     let Just xs = lookup id strms >>= fromDynF t in
     reverse xs !! (fromIntegral i + k)
-  Local t1 _ name e1 e2 -> 
-    let x     = evalExpr_ k e1 exts locs strms in
+  Local t1 _ name e1 e2              -> 
+    let x     = evalExpr_ k e1 locs strms in
     let locs' = (name, toDyn t1 x) : locs  in
-    x `seq` locs' `seq` evalExpr_ k e2 exts locs' strms
-  Var t name                 -> fromJust $ lookup name locs >>= fromDyn t
-  ExternVar t name           -> evalExtern k t name (varEnv exts)
-  ExternFun t name _ _       -> evalFunc k t name exts
-  ExternArray _ t name idx _ -> evalArray k t name evalIdx (arrEnv exts)
-    where evalIdx = evalExpr_ k idx exts locs strms
-  Op1 op e1              -> 
-    let ev1 = evalExpr_ k e1 exts locs strms in 
-    let op1 = evalOp1 op                     in
+    x `seq` locs' `seq` evalExpr_ k e2  locs' strms
+  Var t name                         -> fromJust $ lookup name locs >>= fromDyn t
+  ExternVar _ name xs                -> evalExternVar k name xs
+  ExternFun _ name _ expr _          -> --evalFunc k t name expr 
+    case expr of
+      Nothing -> throw (NoExtsInterp name)
+      Just e  -> evalExpr_ k e locs strms
+  ExternArray _ _ name size idx xs _ -> evalArray k name evalIdx xs size
+    where evalIdx = evalExpr_ k idx locs strms
+  Op1 op e1                          -> 
+    let ev1 = evalExpr_ k e1 locs strms in 
+    let op1 = evalOp1 op                in
     ev1 `seq` op1 `seq` op1 ev1               
-  Op2 op e1 e2           -> 
-    let ev1 = evalExpr_ k e1 exts locs strms in 
-    let ev2 = evalExpr_ k e2 exts locs strms in 
-    let op2 = evalOp2 op                     in
+  Op2 op e1 e2                       -> 
+    let ev1 = evalExpr_ k e1 locs strms in 
+    let ev2 = evalExpr_ k e2 locs strms in 
+    let op2 = evalOp2 op                in
     ev1 `seq` ev2 `seq` op2 `seq` op2 ev1 ev2
-  Op3 op e1 e2 e3        -> 
-    let ev1 = evalExpr_ k e1 exts locs strms in 
-    let ev2 = evalExpr_ k e2 exts locs strms in 
-    let ev3 = evalExpr_ k e3 exts locs strms in 
-    let op3 = evalOp3 op                     in
+  Op3 op e1 e2 e3                    -> 
+    let ev1 = evalExpr_ k e1 locs strms in 
+    let ev2 = evalExpr_ k e2 locs strms in 
+    let ev3 = evalExpr_ k e3 locs strms in 
+    let op3 = evalOp3 op                in
     ev1 `seq` ev2 `seq` ev3 `seq` op3 `seq` op3 ev1 ev2 ev3
 
 --------------------------------------------------------------------------------
 
-evalExtern :: Int -> Type a -> Name -> Env Name -> a
-evalExtern k t name exts = 
-  case lookup name exts of
-    Nothing -> badUsage $ "you need to supply a list of values for interpreting variable " ++ name
-    Just dyn ->
-      case fromDynF t dyn of
-        Nothing -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."
-        Just xs -> xs !! k
+evalExternVar :: Int -> Name -> Maybe [a] -> a
+evalExternVar k name exts = 
+  case exts of
+    Nothing -> throw (NoExtsInterp name)
+    Just xs -> 
+      case safeIndex k xs of
+        Nothing -> throw (NotEnoughValues name k)
+        Just x  -> x
 
 --------------------------------------------------------------------------------
 
-evalFunc :: Int -> Type a -> Name -> ExtEnv -> a
-evalFunc k t name exts  = 
-  case lookup name (funcEnv exts) of
-    Nothing -> 
-      badUsage $ "to simulate a spec containing the external function "
-                   ++ name ++ ", you need to include a stream to simulate it"
+-- evalFunc :: Int -> Type a -> Name -> Expr a -> ExtEnv -> a
+-- evalFunc k t name expr exts  = 
+--   evalExpr k expr 
 
-    -- We created this spec in Interpreter.hs, copilot-language, so it should
-    -- contain no triggers and exactly one observer.
-    Just Spec { specStreams   = specStrms
-              , specObservers = obsLs }  -> 
-     let initStrms = map initStrm specStrms             in
-     let strms = evalStreams k exts specStrms initStrms in
-     case obsLs of
-       [Observer { observerExpr     = expr_
-                 , observerExprType = t1 }] -> 
-         let dyn = toDynF t1 expr_ in
-           case fromDynF t dyn of
-             Nothing    -> impossible "evalFunc" "copilot-core"
-             Just expr  -> evalExpr_ k expr exts [] strms
-       _ -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."
+--   case lookup name (funcEnv exts) of
+--     Nothing -> throw (NoValues name)
 
+--     -- We created this spec in Interpreter.hs, copilot-language, so it should
+--     -- contain no triggers and exactly one observer.
+--     Just Spec { specStreams   = specStrms
+--               , specObservers = obsLs }  -> 
+--      let initStrms = map initStrm specStrms             in
+--      let strms = evalStreams k exts specStrms initStrms in
+--      case obsLs of
+--        [Observer { observerExpr     = expr_
+--                  , observerExprType = t1 }] -> 
+--          let dyn = toDynF t1 expr_ in
+--            case fromDynF t dyn of
+--              Nothing    -> throw (BadType name)
+--              Just expr  -> evalExpr_ k expr exts [] strms
+--        _ -> throw (BadType name) 
+
 --------------------------------------------------------------------------------
 
-evalArray :: Integral b => Int -> Type a -> Name -> b -> ArrEnv -> a
-evalArray k t name idx exts =
-  case lookup name exts of
-    Nothing -> badUsage $ "you need to supply a list of finite lists " ++ 
-                 "for interpreting array " ++ name
-    Just dyn ->
-      case catMaybes $ map (fromDynF t) dyn of
-        [] -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."
-        xs -> let arr = (xs !! k) in
-              if length arr > fromIntegral idx
-                then arr !! fromIntegral idx
-                else badUsage $ "in the environment for array " ++ name ++ 
-                          ", you tried to index out of bounds"
+evalArray :: Integral b => Int -> Name -> b -> Maybe [[a]] -> Int -> a
+evalArray k name idx exts size =
+  case exts of 
+    Nothing -> throw (NoExtsInterp name)
+    Just xs -> 
+      case safeIndex k xs of
+        Nothing  -> throw (NotEnoughValues name k)
+        Just arr -> -- convoluted form in case the array is env of infinite
+                    -- length.
+                    if    length (take size arr) == size  
+                       && length (take (size+1) arr) == size
+                      then case safeIndex (fromIntegral idx) arr of
+                             Nothing -> throw (ArrayIdxOutofBounds
+                                                 name (fromIntegral idx) size)
+                             Just x  -> x
+                      else throw (ArrayWrongSize name size)
   
 --------------------------------------------------------------------------------
 
@@ -234,7 +295,7 @@
   BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )
 
 catchZero :: Integral a => (a -> a -> a) -> (a -> a -> a)
-catchZero _ _ 0 = badUsage "divide by zero"
+catchZero _ _ 0 = throw DivideByZero
 catchZero f x y = f x y
 
 --------------------------------------------------------------------------------
@@ -252,8 +313,8 @@
 
 -- XXX actually only need to compute until shortest stream is of length k
 -- XXX this should just be a foldl' over [0,1..k]
-evalStreams :: Int -> ExtEnv -> [Stream] -> Env Id -> Env Id
-evalStreams top exts specStrms initStrms = 
+evalStreams :: Int -> [Stream] -> Env Id -> Env Id
+evalStreams top specStrms initStrms = 
   evalStreams_ 0 initStrms 
   where 
   evalStreams_ :: Int -> Env Id -> Env Id
@@ -266,15 +327,15 @@
                       , streamExpr     = e
                       , streamExprType = t } =
       let xs = fromJust $ lookup id strms >>= fromDynF t       in
-      let x  = evalExpr_ k e exts [] strms                     in
+      let x  = evalExpr_ k e [] strms                          in
       let ls = x `seq` (x:xs)                                  in
       (id, toDynF t ls)
 
 --------------------------------------------------------------------------------
 
 evalTrigger :: 
-  ShowType -> Int -> ExtEnv -> Env Id -> Trigger -> [Maybe [Output]]
-evalTrigger showType k exts strms
+  ShowType -> Int -> Env Id -> Trigger -> [Maybe [Output]]
+evalTrigger showType k strms
   Trigger
     { triggerGuard = e
     , triggerArgs  = args
@@ -286,26 +347,36 @@
   tag (False, _) = Nothing
 
   bs :: [Bool]
-  bs = evalExprs_ k e exts strms
+  bs = evalExprs_ k e strms
 
   vs :: [[Output]]
   vs = transpose $ map evalUExpr args 
 
   evalUExpr :: UExpr -> [Output]
   evalUExpr (UExpr t e1) =
-    map (showWithType showType t) (evalExprs_ k e1 exts strms)
+    map (showWithType showType t) (evalExprs_ k e1 strms)
 
 --------------------------------------------------------------------------------
-evalObserver :: ShowType -> Int -> ExtEnv -> Env Id -> Observer -> [Output]
-evalObserver showType k exts strms
+evalObserver :: ShowType -> Int -> Env Id -> Observer -> [Output]
+evalObserver showType k strms
   Observer
     { observerExpr     = e
     , observerExprType = t }
-  = map (showWithType showType t) (evalExprs_ k e exts strms)
+  = map (showWithType showType t) (evalExprs_ k e strms)
 
 --------------------------------------------------------------------------------
 
-evalExprs_ :: Int -> Expr a -> ExtEnv -> Env Id -> [a]
-evalExprs_ k e exts strms = 
-  map (\i -> evalExpr_ i e exts [] strms) [0..(k-1)]
-                                       
+evalExprs_ :: Int -> Expr a -> Env Id -> [a]
+evalExprs_ k e strms = 
+  map (\i -> evalExpr_ i e [] strms) [0..(k-1)]
+
+--------------------------------------------------------------------------------
+
+-- | Safe indexing (!!) on possibly infininite lists.
+safeIndex :: Int -> [a] -> Maybe a
+safeIndex i ls =
+  let ls' = take (i+1) ls in
+  if length ls' > i then Just (ls' !! i)
+    else Nothing
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/MakeTags.hs b/src/Copilot/Core/MakeTags.hs
--- a/src/Copilot/Core/MakeTags.hs
+++ b/src/Copilot/Core/MakeTags.hs
@@ -12,11 +12,10 @@
 import Prelude hiding (id)
 
 next :: State Int Int
-next =
-  do
-    k <- get
-    put (succ k)
-    return k
+next = do
+  k <- get
+  put (succ k)
+  return k
 
 makeTags :: Spec -> Spec
 makeTags spec = evalState (mkTagsSpec spec) 0
@@ -37,7 +36,6 @@
 mkTagsStrms = mapM mkTagsStrm
 
   where
-
     mkTagsStrm Stream
       { streamId         = id
       , streamBuffer     = xs
@@ -57,7 +55,6 @@
 mkTagsObsvs = mapM mkTagsObsv
 
   where
-
     mkTagsObsv Observer
       { observerName     = name
       , observerExpr     = e
@@ -73,7 +70,6 @@
 mkTagsTrigs = mapM mkTagsTrig
 
  where
-
    mkTagsTrig Trigger
      { triggerName      = name
      , triggerGuard     = g
@@ -94,19 +90,18 @@
 
 mkTagsExpr :: Expr a -> State Int (Expr a)
 mkTagsExpr e0 = case e0 of
-  Const t x                     -> return $ Const t x
-  Drop t k id                   -> return $ Drop t k id
-  Local t1 t2 name e1 e2        -> liftM2 (Local t1 t2 name) (mkTagsExpr e1) (mkTagsExpr e2)
-  Var t name                    -> return $ Var t name
-  ExternVar t name              -> return $ ExternVar t name
-  ExternFun t name args _       -> do
-                                     args' <- mapM mkTagsUExpr args
-                                     k <- next
-                                     return $ ExternFun t name args' (Just k)
-  ExternArray t1 t2 name idx _  -> do
-                                     idx' <- mkTagsExpr idx
-                                     k <- next
-                                     return $ ExternArray t1 t2 name idx' (Just k)
-  Op1 op e                      -> liftM  (Op1 op) (mkTagsExpr e)
-  Op2 op e1 e2                  -> liftM2 (Op2 op) (mkTagsExpr e1) (mkTagsExpr e2)
-  Op3 op e1 e2 e3               -> liftM3 (Op3 op) (mkTagsExpr e1) (mkTagsExpr e2) (mkTagsExpr e3)
+  Const t x                      -> return $ Const t x
+  Drop t k id                    -> return $ Drop t k id
+  Local t1 t2 name e1 e2         -> liftM2 (Local t1 t2 name) (mkTagsExpr e1) (mkTagsExpr e2)
+  Var t name                     -> return $ Var t name
+  ExternVar t name e             -> return $ ExternVar t name e
+  ExternFun t name args expr _   -> do args' <- mapM mkTagsUExpr args
+                                       k <- next
+                                       return $ ExternFun t name args' expr (Just k)
+  ExternArray t1 t2 name 
+              size idx e _       -> do idx' <- mkTagsExpr idx
+                                       k <- next
+                                       return $ ExternArray t1 t2 name size idx' e (Just k)
+  Op1 op e                       -> liftM  (Op1 op) (mkTagsExpr e)
+  Op2 op e1 e2                   -> liftM2 (Op2 op) (mkTagsExpr e1) (mkTagsExpr e2)
+  Op3 op e1 e2 e3                -> liftM3 (Op3 op) (mkTagsExpr e1) (mkTagsExpr e2) (mkTagsExpr e3)
diff --git a/src/Copilot/Core/Operators.hs b/src/Copilot/Core/Operators.hs
--- a/src/Copilot/Core/Operators.hs
+++ b/src/Copilot/Core/Operators.hs
@@ -42,7 +42,7 @@
   Acosh    :: Floating a => Type a -> Op1 a a
   -- Bitwise operators.
   BwNot    :: Bits     a => Type a -> Op1 a a
-  -- Casting operaators.
+  -- Casting operator.
   Cast     :: (Integral a, Num b) => Type a -> Type b -> Op1 a b
 
 -- | Binary operators.
diff --git a/src/Copilot/Core/PrettyPrint.hs b/src/Copilot/Core/PrettyPrint.hs
--- a/src/Copilot/Core/PrettyPrint.hs
+++ b/src/Copilot/Core/PrettyPrint.hs
@@ -28,13 +28,14 @@
   Const t x                  -> text (showWithType Haskell t x)
   Drop _ 0 id                -> strmName id
   Drop _ i id                -> text "drop" <+> text (show i) <+> strmName id
-  ExternVar _ name           -> text "extern" <+> doubleQuotes (text name)
-  ExternFun _ name args _    -> 
+  ExternVar _ name _         -> text "extern" <+> doubleQuotes (text name)
+  ExternFun _ name args _ _  -> 
     text "extern" <+> doubleQuotes 
       (text name <> lparen <> 
          hcat (punctuate (comma <> space) (map ppUExpr args))
        <> rparen)
-  ExternArray _ _ name idx _ -> text "extern" <+> doubleQuotes (text name <> lbrack 
+  ExternArray _ _ name 
+              _ idx _ _      -> text "extern" <+> doubleQuotes (text name <> lbrack 
                                   <> ppExpr idx <> rbrack)
   Local _ _ name e1 e2       -> text "local" <+> doubleQuotes (text name) <+> equals
                                           <+> ppExpr e1 $$ text "in" <+> ppExpr e2
diff --git a/src/Copilot/Core/Random.hs b/src/Copilot/Core/Random.hs
--- a/src/Copilot/Core/Random.hs
+++ b/src/Copilot/Core/Random.hs
@@ -2,34 +2,36 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+-- | Random spec generator.
+
 {-# LANGUAGE GADTs, ExistentialQuantification #-}
 
 module Copilot.Core.Random
-  ( randomSpec
-  , randomExtVals ) where
+  ( randomSpec ) where
+--  , randomExtVals 
 
 import Copilot.Core 
-import Copilot.Core.Interpret.Eval (ExtEnv (..), Env)
+--import Copilot.Core.Interpret.Eval (Env)
 import Copilot.Core.Random.Gen
 import Copilot.Core.Random.Weights
 import Copilot.Core.Type.Dynamic
 import Copilot.Core.Type.Equality ((=~=))
 
 import Control.Monad
-import Data.List (foldl', nubBy)
+import Data.List (foldl')
 import Prelude hiding (id)
 import System.Random (StdGen)
 import Control.Monad.Reader
 
 --------------------------------------------------------------------------------
 
-randomSpec :: Weights -> StdGen -> Spec
-randomSpec = runGen genSpec 0
+randomSpec :: Int -> Weights -> StdGen -> Spec
+randomSpec rnds = runGen (genSpec rnds) 0
 
 --------------------------------------------------------------------------------
 
-genSpec :: Gen Spec
-genSpec = do
+genSpec :: Int -> Gen Spec
+genSpec rnds = do
   ws          <- weights
   numTriggers <- choose (1, maxTriggers ws)
   ss          <- genStreamInfo's
@@ -57,19 +59,20 @@
     genExtVar i = do 
       ws <- weights                 
       WrapType t <- genType ws
-      let expr = ExternVar t ("ext" ++ show i)
+      evalExpr <- randomReplicate rnds t
+      let expr = ExternVar t ("ext" ++ show i) (Just evalExpr)
       return $ toDynF t expr
 
 --------------------------------------------------------------------------------
 
-data StreamInfo = forall a . (Eq a, Ord a) => StreamInfo
+data StreamInfo = forall a . (Eq a, Ord a, Typed a) => StreamInfo
   { streamInfoId         :: Id
   , streamInfoType       :: Type a
   , streamInfoBufferSize :: Int }
 
 --------------------------------------------------------------------------------
 
-data WrapType = forall a . (Eq a, Ord a) => WrapType (Type a)
+data WrapType = forall a . (Eq a, Ord a, Typed a) => WrapType (Type a)
 
 genType :: Weights -> Gen WrapType
 genType ws = freq
@@ -86,7 +89,7 @@
   , (floatFreq  ws, return $ WrapType (typeOf :: Type Double)) ]
 
 genTypeFromStreamInfo's :: [StreamInfo] -> Gen WrapType
-genTypeFromStreamInfo's = elements . map (\ (StreamInfo _ t _) -> WrapType t)
+genTypeFromStreamInfo's = elements . map (\(StreamInfo _ t _) -> WrapType t)
 
 --------------------------------------------------------------------------------
 
@@ -209,6 +212,8 @@
                                     _      -> False
       in  elements (filter p ss)
 
+  genOp3 = incDepth (genOp3Mux extVars ss t)    
+
   genOp1 = incDepth $ case t of
     Bool   -> genOp1Bool extVars ss
     Int8   -> genOp1Num  extVars ss t
@@ -223,9 +228,10 @@
     Double -> genOp1Num  extVars ss t
 
   genOp2 = incDepth $ case t of
--- XXX 
---    Bool    -> oneOf [genOp2Bool ss, genOp2Eq ss, genOp2Ord ss]
-    Bool    -> oneOf [genOp2Bool extVars ss, genOp2Eq extVars ss]
+    Bool    -> oneOf [ genOp2Bool extVars ss
+                     , genOp2Eq extVars ss
+                     , genOp2Ord extVars ss 
+                     ]
     Int8    -> intOrWord NumWit IntegralWit
     Int16   -> intOrWord NumWit IntegralWit
     Int32   -> intOrWord NumWit IntegralWit
@@ -238,99 +244,90 @@
     Double  -> floatOrDouble NumWit
 
     where
-
-      intOrWord numWit integralWit = do 
-        ws <- weights 
-        if divModFreq ws 
-          then oneOf $ num ++ [ genOp2Integral extVars ss t integralWit ]
-          else oneOf num
-        where num = [ genOp2Num extVars ss t numWit ]
-
-      floatOrDouble numWit = oneOf
-        [ genOp2Num extVars ss t numWit ]
+    floatOrDouble numWit = oneOf [ genOp2Num extVars ss t numWit ]
 
-  genOp3 = incDepth (genOp3Mux extVars ss t)    
+    intOrWord numWit integralWit = do 
+      ws <- weights 
+      if divModFreq ws 
+        then oneOf $ num ++ [ genOp2Integral extVars ss t integralWit ]
+        else oneOf num
+      where 
+      num = [ genOp2Num extVars ss t numWit ]
+      
 
 --------------------------------------------------------------------------------
 
 genOp1Bool :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)
-genOp1Bool extVars ss =
-  do
-    ew <- genExpr extVars ss (typeOf :: Type Bool)
-    return $ Op1 Not ew
+genOp1Bool extVars ss = do
+  ew <- genExpr extVars ss (typeOf :: Type Bool)
+  return $ Op1 Not ew
 
 genOp1Num :: Num a => [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a)
-genOp1Num extVars ss t =
-  do
-    ew  <- genExpr extVars ss t
-    opw <- elements [Abs t, Sign t]
-    return $ Op1 opw ew
+genOp1Num extVars ss t = do
+  ew  <- genExpr extVars ss t
+  opw <- elements [Abs t, Sign t]
+  return $ Op1 opw ew
 
 genOp2Bool :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)
-genOp2Bool extVars ss =
-  do
-    ew1 <- genExpr extVars ss (typeOf :: Type Bool)
-    ew2 <- genExpr extVars ss (typeOf :: Type Bool)
-    opw <- elements [And, Or]
-    return $ Op2 opw ew1 ew2
+genOp2Bool extVars ss = do
+  ew1 <- genExpr extVars ss (typeOf :: Type Bool)
+  ew2 <- genExpr extVars ss (typeOf :: Type Bool)
+  opw <- elements [And, Or]
+  return $ Op2 opw ew1 ew2
 
 genOp2Eq :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)
-genOp2Eq extVars ss =
-  do
-    WrapType t <- genTypeFromStreamInfo's ss
-    ew1 <- genExpr extVars ss t
-    ew2 <- genExpr extVars ss t
-    opw <- elements [Eq t, Ne t]
-    return $ Op2 opw ew1 ew2
+genOp2Eq extVars ss = do
+  WrapType t <- genTypeFromStreamInfo's ss
+  ew1 <- genExpr extVars ss t
+  ew2 <- genExpr extVars ss t
+  opw <- elements [Eq t, Ne t]
+  return $ Op2 opw ew1 ew2
 
--- XXX
--- Figure out how to ensure t comes from a Numeric Class
--- genOp2Ord :: [StreamInfo] -> Gen (Expr Bool)
--- genOp2Ord ss =
---   do
---     WrapType t <- genTypeFromStreamInfo's ss
---     ew1 <- genExpr extVars ss t
---     ew2 <- genExpr extVars ss t
---     opw <- elements
---       [ (Lt t)
---       , (Gt t)
---       , (Le t)
---       , (Ge t) ]
---     return $ Op2 opw ew1 ew2
+genOp2Ord :: [DynExtVar] -> [StreamInfo] -> Gen (Expr Bool)
+genOp2Ord extVars ss = 
+  let ss' = findStreamOmittingType Bool in
+  if (null ss') then genExpr extVars ss Bool 
+    else do
+      WrapType t <- genTypeFromStreamInfo's ss'
+      ew1 <- genExpr extVars ss t
+      ew2 <- genExpr extVars ss t
+      opw <- elements [ (Lt t)
+                      , (Gt t)
+                      , (Le t)
+                      , (Ge t) ]
+      return $ Op2 opw ew1 ew2
+  where
+  findStreamOmittingType :: Type a -> [StreamInfo]
+  findStreamOmittingType t0 = 
+    let p (StreamInfo _ t1 _) = case t0 =~= t1 of
+                                  Just _ -> True
+                                  _      -> False
+    in  filter (not . p) ss
 
 genOp2Num :: [DynExtVar] -> [StreamInfo] -> Type a -> NumWit a -> Gen (Expr a)
-genOp2Num extVars ss t NumWit =
-  do
-    ew1 <- genExpr extVars ss t
-    ew2 <- genExpr extVars ss t
-    opw <- 
-      elements
-        [ (Add t)
-        , (Sub t)
-        , (Mul t) ]
-    return
-      $ Op2 opw ew1 ew2
+genOp2Num extVars ss t NumWit = do
+  ew1 <- genExpr extVars ss t
+  ew2 <- genExpr extVars ss t
+  opw <- elements [ (Add t)
+                  , (Sub t)
+                  , (Mul t) ]
+  return $ Op2 opw ew1 ew2
 
 genOp2Integral :: 
   [DynExtVar] -> [StreamInfo] -> Type a -> IntegralWit a -> Gen (Expr a)
-genOp2Integral extVars ss t IntegralWit =
-  do
-    ew1 <- genExpr extVars ss t
-    ew2 <- genExpr extVars ss t
-    opw <- 
-      elements
-        [ (Div t)
-        , (Mod t) ]
-    return
-      $ Op2 opw ew1 ew2
+genOp2Integral extVars ss t IntegralWit = do
+  ew1 <- genExpr extVars ss t
+  ew2 <- genExpr extVars ss t
+  opw <- elements [ (Div t)
+                  , (Mod t) ]
+  return $ Op2 opw ew1 ew2
 
 genOp3Mux :: [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a)
-genOp3Mux extVars ss t =
-  do
-    ew1 <- genExpr extVars ss (typeOf :: Type Bool)
-    ew2 <- genExpr extVars ss t
-    ew3 <- genExpr extVars ss t
-    return $ Op3 (Mux t) ew1 ew2 ew3
+genOp3Mux extVars ss t = do
+  ew1 <- genExpr extVars ss (typeOf :: Type Bool)
+  ew2 <- genExpr extVars ss t
+  ew3 <- genExpr extVars ss t
+  return $ Op3 (Mux t) ew1 ew2 ew3
 
 data NumWit a = Num a => NumWit
 
@@ -338,53 +335,53 @@
 
 --------------------------------------------------------------------------------
 
-randomExtVals :: Int -> Spec -> Weights -> StdGen -> ExtEnv
-randomExtVals rnds spec = runGen env 0
-  where env = do vars <- extVals rnds spec
-                 return ExtEnv { varEnv = vars
-                               , arrEnv = []
-                               , funcEnv = []
-                               }
+-- randomExtVals :: Int -> Spec -> Weights -> StdGen -> ExtEnv
+-- randomExtVals rnds spec = runGen env 0
+--   where env = do vars <- extVals rnds spec
+--                  return ExtEnv { varEnv = vars
+--                                , arrEnv = []
+-- --                               , funcEnv = []
+--                                }
 
 --------------------------------------------------------------------------------
 
 -- Extract the external variables, returning randomly-generated lists for their
 -- values.
-extVals :: Int -> Spec -> Gen (Env Name)
-extVals rnds Spec { specStreams = strms
-                  , specTriggers = triggers } 
-  = 
-  let vars = nubBy (\a b -> fst a == fst b) $ 
-               concatMap strmExts strms ++ 
-               concatMap triggerExts triggers  in
-  mapM randomLst vars
+-- extVals :: Int -> Spec -> Gen (Env Name)
+-- extVals rnds Spec { specStreams = strms
+--                   , specTriggers = triggers } 
+--   = 
+--   let vars = nubBy (\a b -> fst a == fst b) $ 
+--                concatMap strmExts strms ++ 
+--                concatMap triggerExts triggers  in
+--   mapM randomLst vars
 
-  where 
-  randomLst :: (Name, UType) -> Gen (Name, DynamicF [] Type)
-  randomLst (nm, UType { uTypeType = t }) = do
-    rnd <- randomReplicate rnds t
-    return $ (nm, toDynF t rnd)
+--   where 
+--   randomLst :: (Name, UType) -> Gen (Name, DynamicF [] Type)
+--   randomLst (nm, UType { uTypeType = t }) = do
+--     rnd <- randomReplicate rnds t
+--     return $ (nm, toDynF t rnd)
 
-  strmExts Stream { streamExpr = expr } = extsFromExpr expr
+--   strmExts Stream { streamExpr = expr } = extsFromExpr expr
 
-  triggerExts Trigger { triggerGuard = grd
-                      , triggerArgs = args } = 
-    extsFromExpr grd ++ concatMap getExpr args
-      where getExpr UExpr { uExprExpr = expr } = extsFromExpr expr
+--   triggerExts Trigger { triggerGuard = grd
+--                       , triggerArgs = args } = 
+--     extsFromExpr grd ++ concatMap getExpr args
+--       where getExpr UExpr { uExprExpr = expr } = extsFromExpr expr
   
-  extsFromExpr :: Expr a -> [(Name, UType)]
-  extsFromExpr expr =
-    case expr of
-      Const _ _              -> []
-      Drop _ _ _             -> []
-      Local _ _ _ e1 e2      -> extsFromExpr e1 ++ extsFromExpr e2
-      Var _ _                -> []
-      ExternVar t name       -> [(name, UType { uTypeType = t })]
-      ExternFun _ _ _ _      -> []
-      ExternArray _ _ _ _ _  -> []
-      Op1 _ e                -> extsFromExpr e
-      Op2 _ e1 e2            -> extsFromExpr e1 ++ extsFromExpr e2
-      Op3 _ e1 e2 e3         -> extsFromExpr e1 ++ extsFromExpr e2
-                                  ++ extsFromExpr e3
+--   extsFromExpr :: Expr a -> [(Name, UType)]
+--   extsFromExpr expr =
+--     case expr of
+--       Const _ _                  -> []
+--       Drop _ _ _                 -> []
+--       Local _ _ _ e1 e2          -> extsFromExpr e1 ++ extsFromExpr e2
+--       Var _ _                    -> []
+--       ExternVar t name _         -> [(name, UType { uTypeType = t })]
+--       ExternFun _ _ _ _ _        -> []
+--       ExternArray _ _ _ _ _ _ _  -> []
+--       Op1 _ e                    -> extsFromExpr e
+--       Op2 _ e1 e2                -> extsFromExpr e1 ++ extsFromExpr e2
+--       Op3 _ e1 e2 e3             -> extsFromExpr e1 ++ extsFromExpr e2
+--                                       ++ extsFromExpr e3
 
 --------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Spec.hs b/src/Copilot/Core/Spec.hs
--- a/src/Copilot/Core/Spec.hs
+++ b/src/Copilot/Core/Spec.hs
@@ -12,12 +12,12 @@
   ) where
 
 import Copilot.Core.Expr (Name, Id, Expr, UExpr)
-import Copilot.Core.Type (Type)
+import Copilot.Core.Type (Type, Typed)
 
 --------------------------------------------------------------------------------
 
 -- | A stream.
-data Stream = forall a  . Stream
+data Stream = forall a. Typed a => Stream
   { streamId         :: Id
   , streamBuffer     :: [a]
   , streamGuard      :: Expr Bool
@@ -27,7 +27,7 @@
 --------------------------------------------------------------------------------
 
 -- | An observer.
-data Observer = forall a . Observer
+data Observer = forall a. Observer
   { observerName     :: Name
   , observerExpr     :: Expr a
   , observerExprType :: Type a }
diff --git a/src/Copilot/Core/Spec/Locals.hs b/src/Copilot/Core/Spec/Locals.hs
--- a/src/Copilot/Core/Spec/Locals.hs
+++ b/src/Copilot/Core/Spec/Locals.hs
@@ -74,13 +74,13 @@
   Local t _ name e1 e2   -> singleton (Loc name t)
                                         `append` locsExpr e1
                                         `append` locsExpr e2
-  Var _ _                -> empty
-  ExternVar _ _          -> empty
-  ExternFun _ _ _ _      -> empty
-  ExternArray _ _ _ _ _  -> empty
-  Op1 _ e                -> locsExpr e
-  Op2 _ e1 e2            -> locsExpr e1 `append` locsExpr e2
-  Op3 _ e1 e2 e3         -> locsExpr e1 `append` locsExpr e2
-                                        `append` locsExpr e3
+  Var _ _                    -> empty
+  ExternVar _ _ _            -> empty
+  ExternFun _ _ _ _ _        -> empty
+  ExternArray _ _  _ _ _ _ _ -> empty
+  Op1 _ e                    -> locsExpr e
+  Op2 _ e1 e2                -> locsExpr e1 `append` locsExpr e2
+  Op3 _ e1 e2 e3             -> locsExpr e1 `append` locsExpr e2
+                                            `append` locsExpr e3
 
 --------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs
--- a/src/Copilot/Core/Type.hs
+++ b/src/Copilot/Core/Type.hs
@@ -10,6 +10,7 @@
   ( Type (..)
   , Typed (..)
   , UType (..)
+  , SimpleType(..)
   ) where
 
 import Data.Int
@@ -43,22 +44,66 @@
   (=~=) Double Double = Just Refl
   (=~=) _ _ = Nothing
 
+--------------------------------------------------------------------------------
+
+data SimpleType = SBool
+                | SInt8 
+                | SInt16
+                | SInt32
+                | SInt64
+                | SWord8
+                | SWord16
+                | SWord32
+                | SWord64
+                | SFloat 
+                | SDouble
+  deriving Eq
+
+--------------------------------------------------------------------------------
+
 class Typed a where
   typeOf :: Type a
+  simpleType :: Type a -> SimpleType
 
-instance Typed Bool   where typeOf = Bool
-instance Typed Int8   where typeOf = Int8
-instance Typed Int16  where typeOf = Int16
-instance Typed Int32  where typeOf = Int32
-instance Typed Int64  where typeOf = Int64
-instance Typed Word8  where typeOf = Word8
-instance Typed Word16 where typeOf = Word16
-instance Typed Word32 where typeOf = Word32
-instance Typed Word64 where typeOf = Word64
-instance Typed Float  where typeOf = Float
-instance Typed Double where typeOf = Double
+--------------------------------------------------------------------------------
 
+instance Typed Bool   where 
+  typeOf       = Bool
+  simpleType _ = SBool
+instance Typed Int8   where 
+  typeOf       = Int8
+  simpleType _ = SBool
+instance Typed Int16  where 
+  typeOf       = Int16
+  simpleType _ = SInt16
+instance Typed Int32  where 
+  typeOf       = Int32
+  simpleType _ = SInt32
+instance Typed Int64  where 
+  typeOf       = Int64
+  simpleType _ = SInt64
+instance Typed Word8  where 
+  typeOf       = Word8
+  simpleType _ = SWord8
+instance Typed Word16 where 
+  typeOf       = Word16
+  simpleType _ = SWord16
+instance Typed Word32 where 
+  typeOf       = Word32
+  simpleType _ = SWord32
+instance Typed Word64 where 
+  typeOf       = Word64
+  simpleType _ = SWord64
+instance Typed Float  where 
+  typeOf       = Float
+  simpleType _ = SFloat
+instance Typed Double where 
+  typeOf       = Double
+  simpleType _ = SDouble
+
 --------------------------------------------------------------------------------
 
 -- | A untyped type (no phantom type).
 data UType = forall a . UType { uTypeType :: Type a }
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Type/Eq.hs b/src/Copilot/Core/Type/Eq.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Type/Eq.hs
@@ -0,0 +1,77 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE ExistentialQuantification, GADTs #-}
+
+module Copilot.Core.Type.Eq
+  ( EqWit (..)
+  , eqWit
+  , UVal (..)
+  ) where
+
+import Copilot.Core.Error (impossible)
+import Copilot.Core.Type
+import Copilot.Core.Type.Dynamic (fromDyn, toDyn)
+
+--------------------------------------------------------------------------------
+
+data EqWit a = Eq a => EqWit
+
+--------------------------------------------------------------------------------
+
+eqWit :: Type a -> EqWit a
+eqWit t =
+  case t of
+    Bool   -> EqWit
+    Int8   -> EqWit
+    Int16  -> EqWit
+    Int32  -> EqWit
+    Int64  -> EqWit
+    Word8  -> EqWit
+    Word16 -> EqWit
+    Word32 -> EqWit
+    Word64 -> EqWit
+    Float  -> EqWit
+    Double -> EqWit
+
+--------------------------------------------------------------------------------
+
+data UVal = forall a. UVal
+  { uType :: Type a
+  , uVal  :: a
+  }
+
+--------------------------------------------------------------------------------
+
+instance Eq UVal where
+  (==) UVal { uType = t1
+            , uVal = a } 
+       UVal { uType = t2
+            , uVal = b }
+    = case eqWit t1 of
+        EqWit -> 
+          case eqWit t2 of
+            EqWit -> 
+              let dyn1 = toDyn t1 a in
+              case fromDyn t2 dyn1 of
+                Nothing -> False
+                Just x  -> 
+                  case t1 of 
+                    -- Hacks for QuickChecking between C and Haskell
+                    Float  -> case t2 of
+                                Float -> approx floatErr x b
+                                _     -> impossible "instance Eq UVal"
+                                                    "copilot-core"
+                    Double -> case t2 of
+                                Double -> approx doubleErr x b
+                                _      -> impossible "instance Eq UVal" 
+                                                     "copilot-core"
+                    _      -> x == b
+    where 
+    approx :: (Num a, Ord a) => a -> a -> a -> Bool
+    approx err x y = x - y < err && y - x < err
+    floatErr  = 0.0001 :: Float
+    doubleErr = 0.0001 :: Double
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Type/Read.hs b/src/Copilot/Core/Type/Read.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Type/Read.hs
@@ -0,0 +1,51 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE ExistentialQuantification, GADTs #-}
+
+module Copilot.Core.Type.Read
+  ( ReadWit (..)
+  , readWit
+  , readWithType
+  ) where
+
+import Copilot.Core.Type
+import Copilot.Core.Error (badUsage)
+
+--------------------------------------------------------------------------------
+
+data ReadWit a = Read a => ReadWit
+
+--------------------------------------------------------------------------------
+
+readWit :: Type a -> ReadWit a
+readWit t =
+  case t of
+    Bool   -> ReadWit
+    Int8   -> ReadWit
+    Int16  -> ReadWit
+    Int32  -> ReadWit
+    Int64  -> ReadWit
+    Word8  -> ReadWit
+    Word16 -> ReadWit
+    Word32 -> ReadWit
+    Word64 -> ReadWit
+    Float  -> ReadWit
+    Double -> ReadWit
+
+--------------------------------------------------------------------------------
+
+readWithType :: Type a -> String -> a
+readWithType t str =
+  case t of
+    Bool -> case str of
+              "0" -> False
+              "1" -> True
+              x   -> badUsage $ "in readWithType in copilot-core: expecting a \"0\" or \"1\" when reading a Boolean value " ++ show x ++ "."
+    _    -> rd
+  where
+  rd = case readWit t of
+         ReadWit -> read str
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Version.hs b/src/Copilot/Core/Version.hs
deleted file mode 100644
--- a/src/Copilot/Core/Version.hs
+++ /dev/null
@@ -1,9 +0,0 @@
---------------------------------------------------------------------------------
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
-
-module Copilot.Core.Version (version) where
-
--- | The current version of Copilot Core.
-version :: String
-version = "0.1"