diff --git a/copilot-core.cabal b/copilot-core.cabal
--- a/copilot-core.cabal
+++ b/copilot-core.cabal
@@ -1,10 +1,19 @@
 cabal-version:       >=1.10
 name:                copilot-core
-version:             0.2.3
+version:             0.2.4
 synopsis:            An intermediate representation for Copilot.
-description:         Intermediate representation for Copilot.
-                     Strictly follows Haskell 2010 except for universal
-                     and existential quantification.
+description:         
+  Intermediate representation for Copilot. 
+  . 
+  Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
+  Haskell that compiles into embedded C.  Copilot contains an interpreter,
+  multiple back-end compilers, and other verification tools.  A tutorial, bug
+  reports, and todos are available at
+  <https://github.com/niswegmann/copilot-discussion>.  
+  .  
+  Examples are available at
+  <https://github.com/leepike/Copilot/tree/master/Examples>.
+
 author:              Lee Pike, Robin Morisset, Alwyn Goodloe,
                      Sebastian Niller, Nis Nordby Wegmann
 license:             BSD3
@@ -31,8 +40,15 @@
     -auto-all
     -caf-all
     -fno-warn-orphans
+
     --enable-library-profiling
 
+    -fpackage-trust    
+    -- Trusted packages
+    -trust base
+    -trust random
+    -trust array
+
   build-depends:
     containers >= 0.4 && < 1,
     base >= 4.0 && < 5,
@@ -55,7 +71,7 @@
     Copilot.Core.MakeTags
     Copilot.Core.Operators
     Copilot.Core.Spec
-    Copilot.Core.Spec.Locals
+    Copilot.Core.Locals
     Copilot.Core.Random
     Copilot.Core.Random.Gen
     Copilot.Core.Random.Weights
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
@@ -5,6 +5,7 @@
 -- | Generates a C99 header from a copilot-specification. The functionality
 -- provided by the header must be implemented by back-ends targetting C99.
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs #-}
 
 module Copilot.Compile.Header.C99
@@ -125,9 +126,7 @@
 
 ppExternalArrays :: [ExtArray] -> Doc
 ppExternalArrays = vcat . map ppExternalArray . nubBy eq
-
   where
-
   eq ExtArray { externArrayName = name1 } ExtArray { externArrayName = name2 } =
     name1 == name2
 
@@ -146,9 +145,7 @@
 
 ppExternalFunctions :: [ExtFun] -> Doc
 ppExternalFunctions = vcat . map ppExternalFunction . nubBy eq
-
   where
-
   eq ExtFun { externFunName = name1 } ExtFun { externFunName = name2 } =
     name1 == name2
 
@@ -162,7 +159,6 @@
         text "(" <> ppArgs args <> text ");"
 
   where
-
   ppArgs :: [UExpr] -> Doc
   ppArgs = hcat . intersperse (text ",") . map ppArg
 
@@ -175,7 +171,6 @@
 typeSpec UType { uTypeType = t } = typeSpec' t
 
   where
-
   typeSpec' Bool = "bool"
   typeSpec' Int8   = "int8_t"
   typeSpec' Int16  = "int16_t"
@@ -197,3 +192,5 @@
 
 unlines :: [String] -> Doc
 unlines = vcat . map text
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs
--- a/src/Copilot/Core.hs
+++ b/src/Copilot/Core.hs
@@ -22,6 +22,8 @@
 -- and the pretty-printer
 -- ("Copilot.Core.PrettyPrint").
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Core
   ( module Copilot.Core.Error
   , module Copilot.Core.Expr
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
@@ -2,6 +2,8 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Core.Error 
   ( impossible
   , badUsage ) where
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
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs, ExistentialQuantification #-}
 
 module Copilot.Core.Expr
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
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE Rank2Types #-}
 
@@ -41,9 +42,7 @@
 
 externVars :: Spec -> [ExtVar]
 externVars = nubBy eqExt . toList . all externVarsExpr
-
   where
-
   eqExt :: ExtVar -> ExtVar -> Bool
   eqExt ExtVar { externVarName = name1 } ExtVar { externVarName = name2 } =
     name1 == name2
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
@@ -4,6 +4,8 @@
 
 -- | An interpreter for Copilot specifications.
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Core.Interpret
   ( --ExtEnv (..)
     Format (..)
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,6 +4,7 @@
 
 -- | A tagless interpreter for Copilot specifications.
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs, BangPatterns, DeriveDataTypeable #-}
 
 module Copilot.Core.Interpret.Eval
diff --git a/src/Copilot/Core/Interpret/Render.hs b/src/Copilot/Core/Interpret/Render.hs
--- a/src/Copilot/Core/Interpret/Render.hs
+++ b/src/Copilot/Core/Interpret/Render.hs
@@ -4,6 +4,8 @@
 
 -- | An tagless interpreter for Copilot specifications.
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Core.Interpret.Render
   ( renderAsTable
   , renderAsCSV
diff --git a/src/Copilot/Core/Locals.hs b/src/Copilot/Core/Locals.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Locals.hs
@@ -0,0 +1,87 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Let expressions.
+
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Copilot.Core.Locals
+  ( Loc (..)
+  , locals
+  ) where
+
+import Copilot.Core
+import Data.DList (DList, empty, singleton, append, concat, toList)
+import Data.List (nubBy)
+import Prelude hiding (concat, foldr)
+
+--------------------------------------------------------------------------------
+
+data Loc = forall a . Loc
+  { localName :: Name
+  , localType :: Type a }
+
+instance Show Loc where
+  show Loc { localName = name } = name
+
+--------------------------------------------------------------------------------
+
+locals :: Spec -> [Loc]
+locals
+  Spec
+    { specStreams   = streams
+    , specTriggers  = triggers
+    , specObservers = observers
+    } = nubBy eqLoc . toList $
+          concat (fmap locsStream   streams)  `append`
+          concat (fmap locsTrigger  triggers) `append`
+          concat (fmap locsObserver observers)
+
+  where
+
+  eqLoc :: Loc -> Loc -> Bool
+  eqLoc Loc { localName = name1 } Loc { localName = name2 } =
+    name1 == name2
+
+--------------------------------------------------------------------------------
+
+locsStream :: Stream -> DList Loc
+locsStream Stream { streamExpr = e } = locsExpr e
+
+--------------------------------------------------------------------------------
+
+locsTrigger :: Trigger -> DList Loc
+locsTrigger Trigger { triggerGuard = e, triggerArgs = args } =
+  locsExpr e `append` concat (fmap locsUExpr args)
+
+  where
+
+  locsUExpr :: UExpr -> DList Loc
+  locsUExpr (UExpr _ e1) = locsExpr e1
+
+--------------------------------------------------------------------------------
+
+locsObserver :: Observer -> DList Loc
+locsObserver Observer { observerExpr = e } = locsExpr e
+
+--------------------------------------------------------------------------------
+
+locsExpr :: Expr a -> DList Loc
+locsExpr e0 = case e0 of
+  Const  _ _             -> empty
+  Drop   _ _ _           -> empty
+  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
+
+--------------------------------------------------------------------------------
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
@@ -4,6 +4,8 @@
 
 -- | Sets a unique tags for each external array/function call.
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Core.MakeTags (makeTags) where
 
 import Copilot.Core.Expr
@@ -39,7 +41,6 @@
     mkTagsStrm Stream
       { streamId         = id
       , streamBuffer     = xs
-      , streamGuard      = g
       , streamExpr       = e
       , streamExprType   = t } =
         do
@@ -47,7 +48,6 @@
           return $ Stream
             { streamId         = id
             , streamBuffer     = xs
-            , streamGuard      = g
             , streamExpr       = e'
             , streamExprType   = t }
 
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
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs, Rank2Types #-}
 
 module Copilot.Core.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
@@ -4,6 +4,7 @@
 
 -- | A pretty printer for Copilot specifications.
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs #-}
 
 module Copilot.Core.PrettyPrint
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
@@ -4,6 +4,7 @@
 
 -- | Random spec generator.
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs, ExistentialQuantification #-}
 
 module Copilot.Core.Random
@@ -135,7 +136,6 @@
       Stream
         { streamId       = id
         , streamBuffer   = xs
-        , streamGuard    = Const (typeOf :: Type Bool) True
         , streamExpr     = w
         , streamExprType = t }
 
diff --git a/src/Copilot/Core/Random/Gen.hs b/src/Copilot/Core/Random/Gen.hs
--- a/src/Copilot/Core/Random/Gen.hs
+++ b/src/Copilot/Core/Random/Gen.hs
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs, ExistentialQuantification #-}
 
 module Copilot.Core.Random.Gen
diff --git a/src/Copilot/Core/Random/Weights.hs b/src/Copilot/Core/Random/Weights.hs
--- a/src/Copilot/Core/Random/Weights.hs
+++ b/src/Copilot/Core/Random/Weights.hs
@@ -2,6 +2,8 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Core.Random.Weights
   ( Depth
   , Weights (..)
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
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE ExistentialQuantification, GADTs #-}
 
 module Copilot.Core.Spec
@@ -20,7 +21,6 @@
 data Stream = forall a. Typed a => Stream
   { streamId         :: Id
   , streamBuffer     :: [a]
-  , streamGuard      :: Expr Bool
   , streamExpr       :: Expr a
   , streamExprType   :: Type a }
 
diff --git a/src/Copilot/Core/Spec/Locals.hs b/src/Copilot/Core/Spec/Locals.hs
deleted file mode 100644
--- a/src/Copilot/Core/Spec/Locals.hs
+++ /dev/null
@@ -1,86 +0,0 @@
---------------------------------------------------------------------------------
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
-
-{-# LANGUAGE ExistentialQuantification #-}
-
--- |
-
-module Copilot.Core.Spec.Locals
-  ( Loc (..)
-  , locals
-  ) where
-
-import Copilot.Core
-import Data.DList (DList, empty, singleton, append, concat, toList)
-import Data.List (nubBy)
-import Prelude hiding (concat, foldr)
-
---------------------------------------------------------------------------------
-
-data Loc = forall a . Loc
-  { localName :: Name
-  , localType :: Type a }
-
-instance Show Loc where
-  show Loc { localName = name } = name
-
---------------------------------------------------------------------------------
-
-locals :: Spec -> [Loc]
-locals
-  Spec
-    { specStreams   = streams
-    , specTriggers  = triggers
-    , specObservers = observers
-    } = nubBy eqLoc . toList $
-          concat (fmap locsStream   streams)  `append`
-          concat (fmap locsTrigger  triggers) `append`
-          concat (fmap locsObserver observers)
-
-  where
-
-  eqLoc :: Loc -> Loc -> Bool
-  eqLoc Loc { localName = name1 } Loc { localName = name2 } =
-    name1 == name2
-
---------------------------------------------------------------------------------
-
-locsStream :: Stream -> DList Loc
-locsStream Stream { streamExpr = e } = locsExpr e
-
---------------------------------------------------------------------------------
-
-locsTrigger :: Trigger -> DList Loc
-locsTrigger Trigger { triggerGuard = e, triggerArgs = args } =
-  locsExpr e `append` concat (fmap locsUExpr args)
-
-  where
-
-  locsUExpr :: UExpr -> DList Loc
-  locsUExpr (UExpr _ e1) = locsExpr e1
-
---------------------------------------------------------------------------------
-
-locsObserver :: Observer -> DList Loc
-locsObserver Observer { observerExpr = e } = locsExpr e
-
---------------------------------------------------------------------------------
-
-locsExpr :: Expr a -> DList Loc
-locsExpr e0 = case e0 of
-  Const  _ _             -> empty
-  Drop   _ _ _           -> empty
-  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
-
---------------------------------------------------------------------------------
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
@@ -2,8 +2,9 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
--- | 
+-- | Typing for Core.
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE ExistentialQuantification, GADTs, KindSignatures #-}
 
 module Copilot.Core.Type
diff --git a/src/Copilot/Core/Type/Dynamic.hs b/src/Copilot/Core/Type/Dynamic.hs
--- a/src/Copilot/Core/Type/Dynamic.hs
+++ b/src/Copilot/Core/Type/Dynamic.hs
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE Rank2Types #-}
 
diff --git a/src/Copilot/Core/Type/Eq.hs b/src/Copilot/Core/Type/Eq.hs
--- a/src/Copilot/Core/Type/Eq.hs
+++ b/src/Copilot/Core/Type/Eq.hs
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE ExistentialQuantification, GADTs #-}
 
 module Copilot.Core.Type.Eq
diff --git a/src/Copilot/Core/Type/Equality.hs b/src/Copilot/Core/Type/Equality.hs
--- a/src/Copilot/Core/Type/Equality.hs
+++ b/src/Copilot/Core/Type/Equality.hs
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs, KindSignatures #-}
 
 module Copilot.Core.Type.Equality
diff --git a/src/Copilot/Core/Type/Read.hs b/src/Copilot/Core/Type/Read.hs
--- a/src/Copilot/Core/Type/Read.hs
+++ b/src/Copilot/Core/Type/Read.hs
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE ExistentialQuantification, GADTs #-}
 
 module Copilot.Core.Type.Read
diff --git a/src/Copilot/Core/Type/Show.hs b/src/Copilot/Core/Type/Show.hs
--- a/src/Copilot/Core/Type/Show.hs
+++ b/src/Copilot/Core/Type/Show.hs
@@ -2,6 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE ExistentialQuantification, GADTs #-}
 
 module Copilot.Core.Type.Show
diff --git a/src/Copilot/Core/Type/Uninitialized.hs b/src/Copilot/Core/Type/Uninitialized.hs
--- a/src/Copilot/Core/Type/Uninitialized.hs
+++ b/src/Copilot/Core/Type/Uninitialized.hs
@@ -2,8 +2,9 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
--- | 
+-- | Initial values for give types.
 
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE GADTs #-}
 
 module Copilot.Core.Type.Uninitialized