WIP: fix warnings

copilot-c99/src/Copilot/Compile/C99/CodeGen.hs

@@ -75,12 +75,14 @@ mkStructDecln (Struct x) = C.TypeDecln struct
 
     mkField :: Value a -> C.FieldDecln
     mkField (Value ty field) = C.FieldDecln (transType ty) (fieldName field)
+mkStructDecln _ = error "Unhandled case"
 
 -- | Write a forward struct declaration.
 mkStructForwDecln :: Struct a => Type a -> C.Decln
 mkStructForwDecln (Struct x) = C.TypeDecln struct
   where
     struct = C.TypeSpec $ C.Struct (typeName x)
+mkStructForwDecln _ = error "Unhandled case"
 
 -- * Ring buffers
 

copilot-c99/src/Copilot/Compile/C99/Expr.hs

@@ -61,8 +61,8 @@ transExpr (Op2 (UpdateField ty1@(Struct _) ty2 f) e1 e2) = do
   e2' <- transExpr e2
 
   -- Variable to hold the updated struct
-  (i, _, _) <- get
-  let varName = "_v" ++ show i
+  (i', _, _) <- get
+  let varName = "_v" ++ show i'
   modify (\(i, x, y) -> (i + 1, x, y))
 
   -- Add new var decl
@@ -101,14 +101,14 @@ transExpr (Op2 op e1 e2) = do
   e2' <- transExpr e2
   return $ transOp2 op e1' e2'
 
-transExpr e@(Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do
+transExpr (Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do
   e1' <- transExpr e1
   e2' <- transExpr e2
   e3' <- transExpr e3
 
   -- Variable to hold the updated array
-  (i, _, _) <- get
-  let varName = "_v" ++ show i
+  (i', _, _) <- get
+  let varName = "_v" ++ show i'
   modify (\(i, x, y) -> (i + 1, x, y))
 
   -- Add new var decl
@@ -117,18 +117,19 @@ transExpr e@(Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do
   modify (\(i, x, y) -> (i, x ++ [initDecl], y))
 
   let size :: Type (Array n t) -> C.Expr
-      size arrTy@(Array ty) = C.LitInt (fromIntegral $ typeLength arrTy)
+      size arrTy'@(Array ty) = C.LitInt (fromIntegral $ typeLength arrTy')
                          C..* C.SizeOfType (C.TypeName $ transType ty)
+      size _ = error "Unhandled case"
 
   -- Initialize the var to the same value as the original array
   let initStmt = C.Expr $ memcpy (C.Ident varName) e1' (size arrTy)
 
   -- Update element of array
   let updateStmt = case ty2 of
-        Array _ -> C.Expr $ memcpy dest e3' size
+        Array _ -> C.Expr $ memcpy dest e3' size'
           where
             dest = C.Index (C.Ident varName) e2'
-            size = C.LitInt
+            size' = C.LitInt
                        (fromIntegral $ typeSize ty2)
                        C..* C.SizeOfType (C.TypeName (tyElemName ty2))
 
@@ -183,6 +184,7 @@ transOp1 op e =
     BwNot    _    -> (C..~) e
     Cast     _ ty -> C.Cast (transTypeName ty) e
     GetField (Struct _)  _ f -> C.Dot e (accessorName f)
+    _             -> error "Unhandled case"
 
 -- | Translates a Copilot binary operator and its arguments into a C99
 -- expression.

copilot-c99/src/Copilot/Compile/C99/Representation.hs

@@ -16,6 +16,6 @@ data UniqueTrigger = UniqueTrigger UniqueTriggerId Trigger
 
 -- | Given a list of triggers, make their names unique.
 mkUniqueTriggers :: [Trigger] -> [UniqueTrigger]
-mkUniqueTriggers ts = zipWith mkUnique ts [0..]
+mkUniqueTriggers ts = zipWith mkUnique ts [0 :: Integer ..]
   where
     mkUnique t@(Trigger name _ _) n = UniqueTrigger (name ++ "_" ++ show n) t

copilot-c99/tests/Test/Copilot/Compile/C99.hs

@@ -34,8 +34,6 @@ import Test.QuickCheck.Gen                  (chooseAny, chooseBoundedIntegral)
 
 -- External imports: Copilot
 import Copilot.Core            hiding (Property)
-import Copilot.Core.Type.Array (array)
-
 -- External imports: Modules being tested
 import Copilot.Compile.C99 (cSettingsOutputDirectory, compile, compileWith,
                             mkDefaultCSettings)
@@ -434,15 +432,15 @@ funCompose2 (f1, g1) (f2, g2) (f3, g3) =
 
 -- | Test case specification for specs with one input variable and one output.
 data TestCase1 a b = TestCase1
-  { wrapTC1Expr :: Spec
+  Spec
     -- ^ Specification containing a trigger an extern of type 'a' and a trigger
     -- with an argument of type 'b'.
 
-  , wrapTC1Fun :: [a] -> [b]
+  ([a] -> [b])
     -- ^ Function expected to function in the same way as the Spec being
     -- tested.
 
-  , wrapTC1CopInp :: (String -> String, String, String, Gen a)
+  (String -> String, String, String, Gen a)
     -- ^ Input specification.
     --
     -- - The first element is a function that prints the variable declaration
@@ -456,26 +454,26 @@ data TestCase1 a b = TestCase1
     -- - The latter contains a randomized generator for values of the given
     -- type.
 
-  , wrapTC1CopOut :: (String, String)
+  (String, String)
     -- ^ Output specification.
     --
     -- The first element of the tuple contains the type of the output in C.
     --
     -- The second element of the tuple is the formatting string when printing
     -- values of the given kind.
-  }
+
 
 -- | Test case specification for specs with two input variables and one output.
 data TestCase2 a b c = TestCase2
-  { wrapTC2Expr :: Spec
+  Spec
     -- ^ Specification containing a trigger an extern of type 'a' and a trigger
     -- with an argument of type 'b'.
 
-  , wrapTC2Fun :: [a] -> [b] -> [c]
+  ([a] -> [b] -> [c])
     -- ^ Function expected to function in the same way as the Spec being
     -- tested.
 
-  , wrapTC2CopInp1 :: (String -> String, String, String, Gen a)
+  (String -> String, String, String, Gen a)
     -- ^ Input specification for the first input.
     --
     -- - The first element is a function that prints the variable declaration
@@ -489,7 +487,7 @@ data TestCase2 a b c = TestCase2
     -- - The latter contains a randomized generator for values of the given
     -- type.
 
-  , wrapTC2CopInp2 :: (String -> String, String, String, Gen b)
+  (String -> String, String, String, Gen b)
     -- ^ Input specification for the second input.
     --
     -- - The first element is a function that prints the variable declaration
@@ -503,14 +501,14 @@ data TestCase2 a b c = TestCase2
     -- - The latter contains a randomized generator for values of the given
     -- type.
 
-  , wrapTC2CopOut :: (String, String)
+  (String, String)
     -- ^ Output specification.
     --
     -- The first element of the tuple contains the type of the output in C.
     --
     -- The second element of the tuple is the formatting string when printing
     -- values of the given kind.
-  }
+
 
 -- | Generate test cases for expressions that behave like unary functions.
 mkTestCase1 :: (Typed a, Typed b)

copilot-core/copilot-core.cabal

@@ -39,7 +39,6 @@ library
 
   ghc-options:
     -Wall
-    -fno-warn-orphans
 
   build-depends:
     base >= 4.9 && < 5

copilot-core/src/Copilot/Core/Type.hs

@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# LANGUAGE DataKinds                 #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleContexts          #-}
@@ -48,6 +49,7 @@ module Copilot.Core.Type
 import Data.Char          (isLower, isUpper, toLower)
 import Data.Coerce        (coerce)
 import Data.Int           (Int16, Int32, Int64, Int8)
+import qualified Data.Kind  as DK
 import Data.List          (intercalate)
 import Data.Proxy         (Proxy (..))
 import Data.Type.Equality as DE
@@ -139,7 +141,7 @@ instance {-# OVERLAPPABLE #-} (Typed t, Struct t) => Show t where
 -- Note that both arrays and structs use dependently typed features. In the
 -- former, the length of the array is part of the type. In the latter, the
 -- names of the fields are part of the type.
-data Type :: * -> * where
+data Type :: DK.Type -> DK.Type where
   Bool   :: Type Bool
   Int8   :: Type Int8
   Int16  :: Type Int16
@@ -165,6 +167,7 @@ typeLength _ = fromIntegral $ natVal (Proxy :: Proxy n)
 typeSize :: forall n t . KnownNat n => Type (Array n t) -> Int
 typeSize ty@(Array ty'@(Array _)) = typeLength ty * typeSize ty'
 typeSize ty@(Array _            ) = typeLength ty
+typeSize ty = error $ "There is a bug in the type checker " ++ show ty
 
 instance TestEquality Type where
   testEquality Bool   Bool   = Just DE.Refl
@@ -286,7 +289,9 @@ instance Typed Double where
 
 instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where
   typeOf               = Array typeOf
-  simpleType (Array t) = SArray t
+  simpleType t         = case t of
+    Array t' -> SArray t'
+    o -> error $ "There is a bug in the type checker " ++ show o
 
 -- | A untyped type (no phantom type).
 data UType = forall a . Typeable a => UType (Type a)

copilot-core/src/Copilot/Core/Type/Array.hs

@@ -53,12 +53,12 @@ arrayUpdate (Array []) _ _ = error errMsg
   where
     errMsg = "copilot-core: arrayUpdate: Attempt to update empty array"
 
-arrayUpdate (Array (x:xs)) 0 y = Array (y:xs)
+arrayUpdate (Array (_x:xs)) 0 y = Array (y:xs)
 
 arrayUpdate (Array (x:xs)) n y =
     arrayAppend x (arrayUpdate (Array xs) (n - 1) y)
   where
     -- | Append to an array while preserving length information at the type
     -- level.
     arrayAppend :: a -> Array (n - 1) a -> Array n a
-    arrayAppend x (Array xs) = Array (x:xs)
+    arrayAppend x' (Array xs') = Array (x':xs')

copilot-core/tests/Test/Copilot/Core/Type.hs

@@ -7,7 +7,6 @@ module Test.Copilot.Core.Type where
 
 -- External imports
 import Data.Int                             (Int16, Int32, Int64, Int8)
-import Data.Maybe                           (isJust)
 import Data.Proxy                           (Proxy (..))
 import Data.Type.Equality                   (TestEquality (..), testEquality,
                                              (:~:) (..))
@@ -136,8 +135,7 @@ testSimpleTypesEqualityTransitive =
 -- | Test that each type is only equal to itself.
 testSimpleTypesEqualityUniqueness :: Property
 testSimpleTypesEqualityUniqueness =
-  forAllBlind (shuffle simpleTypes) $ \(t:ts) ->
-    notElem t ts
+  forAllBlind (shuffle simpleTypes) $ \x -> case x of [] -> False; (t:ts) ->  notElem t ts
 
 -- | Simple types tested.
 simpleTypes :: [SimpleType]

copilot-core/tests/Test/Copilot/Core/Type/Array.hs

@@ -141,13 +141,13 @@ testArrayUpdateWrong len =
 testArrayMakeWrongLength :: forall n . KnownNat n => Proxy n -> Property
 testArrayMakeWrongLength len =
     expectFailure           $
-    forAll wrongLength      $ \length ->
-    forAll (xsInt64 length) $ \ls ->
+    forAll wrongLength      $ \length' ->
+    forAll (xsInt64 length') $ \ls ->
       let array' :: Array n Int64
           array' = array ls
       in arrayElems array' == ls
   where
-    xsInt64 length = vectorOf length arbitrary
+    xsInt64 length' = vectorOf length' arbitrary
     expectedLength = fromIntegral (natVal len)
     wrongLength    = (expectedLength +) . getNonNegative <$> arbitrary
 
@@ -157,7 +157,7 @@ testArrayUpdateElems :: forall n . KnownNat n => Proxy n -> Property
 testArrayUpdateElems len =
     forAll xsInt64  $ \ls ->
     forAll position $ \p ->
-    forAll xInt64   $ \v ->
+    forAll xInt64   $ \_v ->
       let -- Original array
           array' :: Array n Int64
           array' = array ls

copilot-interpreter/src/Copilot/Interpret/Eval.hs

@@ -19,7 +19,7 @@ module Copilot.Interpret.Eval
 import Copilot.Core            (Expr (..), Field (..), Id, Name, Observer (..),
                                 Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),
                                 Trigger (..), Type (..), UExpr (..), Value (..),
-				arrayElems, arrayUpdate, specObservers,
+                                arrayElems, arrayUpdate, specObservers,
                                 specStreams, specTriggers, updateField)
 import Copilot.Interpret.Error (badUsage)
 
@@ -32,7 +32,6 @@ import Data.Dynamic      (Dynamic, fromDynamic, toDyn)
 import Data.List         (transpose)
 import Data.Maybe        (fromJust)
 import Data.Typeable     (Typeable)
-import GHC.TypeLits      (KnownNat, Nat, natVal)
 
 -- | Exceptions that may be thrown during interpretation of a Copilot
 -- specification.
@@ -142,14 +141,15 @@ type LocalEnv = [(Name, Dynamic)]
 evalExpr_ :: Typeable a => Int -> Expr a -> LocalEnv -> Env Id -> a
 evalExpr_ k e0 locs strms = case e0 of
   Const _ x                          -> x
-  Drop t i id                        ->
-    let Just buff = lookup id strms >>= fromDynamic in
-    reverse buff !! (fromIntegral i + k)
-  Local t1 _ name e1 e2              ->
+  Drop _t i id                        ->
+    case lookup id strms >>= fromDynamic of
+      Just buff -> reverse buff !! (fromIntegral i + k)
+      Nothing -> error $ "No id " ++ show id ++ " in " ++ show strms
+  Local _t1 _ name e1 e2              ->
     let x     = evalExpr_ k e1 locs strms in
     let locs' = (name, toDyn x) : locs  in
     x `seq` locs' `seq` evalExpr_ k e2  locs' strms
-  Var t name                         -> fromJust $ lookup name locs >>= fromDynamic
+  Var _t name                         -> fromJust $ lookup name locs >>= fromDynamic
   ExternVar _ name xs                -> evalExternVar k name xs
   Op1 op e1                          ->
     let ev1 = evalExpr_ k e1 locs strms in
@@ -210,6 +210,7 @@ evalOp1 op = case op of
     BwNot _    -> complement
     Cast _ _   -> P.fromIntegral
     GetField (Struct _) _ f -> unfield . f
+    GetField {} -> error "There is a bug in the type checker"
   where
     -- Used to help GHC pick a return type for ceiling/floor
     idI :: Integer -> Integer
@@ -247,11 +248,12 @@ evalOp2 op = case op of
   BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )
   Index    _   -> \xs n -> (arrayElems xs) !! (fromIntegral n)
 
-  UpdateField (Struct _) ty (fieldAccessor :: a -> Field s b) ->
+  UpdateField (Struct _) ty (_fieldAccessor :: a -> Field s b) ->
     \stream fieldValue ->
       let newField :: Field s b
           newField = Field fieldValue
       in updateField stream (Value ty newField)
+  UpdateField {} -> error "There is a bug in the type checker"
 
 -- | Apply a function to two numbers, so long as the second one is
 -- not zero.
@@ -267,14 +269,14 @@ catchZero f x y = f x y
 -- 'Copilot.Core.Operators.Op3'.
 evalOp3 :: Op3 a b c d -> (a -> b -> c -> d)
 evalOp3 (Mux         _)  = \ !v !x !y -> if v then x else y
-evalOp3 (UpdateArray ty) = \xs n x -> arrayUpdate xs (fromIntegral n) x
+evalOp3 (UpdateArray _ty) = \xs n x -> arrayUpdate xs (fromIntegral n) x
 
 -- | Turn a stream into a key-value pair that can be added to an 'Env' for
 -- simulation.
 initStrm :: Stream -> (Id, Dynamic)
 initStrm Stream { streamId       = id
                 , streamBuffer   = buffer
-                , streamExprType = t } =
+                } =
   (id, toDyn (reverse buffer))
 
 -- | Evaluate several streams for a number of steps, producing the environment
@@ -293,7 +295,7 @@ evalStreams top specStrms initStrms =
     strms_ = map evalStream specStrms
     evalStream Stream { streamId       = id
                       , streamExpr     = e
-                      , streamExprType = t } =
+                      } =
       let xs = fromJust $ lookup id strms >>= fromDynamic      in
       let x  = evalExpr_ k e [] strms                          in
       let ls = x `seq` (x:xs)                                  in
@@ -402,5 +404,5 @@ showWit t =
     Word64 -> ShowWit
     Float  -> ShowWit
     Double -> ShowWit
-    Array t -> ShowWit
-    Struct t -> ShowWit
+    Array _ -> ShowWit
+    Struct _ -> ShowWit