fix warnings in copilot-core

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

@@ -45,21 +45,22 @@ module Copilot.Core.Type
   where
 
 -- External imports
-import Data.Char          (isLower, isUpper, toLower)
-import Data.Coerce        (coerce)
-import Data.Int           (Int16, Int32, Int64, Int8)
-import Data.List          (intercalate)
-import Data.Proxy         (Proxy (..))
-import Data.Type.Equality as DE
-import Data.Typeable      (Typeable, eqT, typeRep)
-import Data.Word          (Word16, Word32, Word64, Word8)
-import GHC.Generics       (Datatype (..), D1, Generic (..), K1 (..), M1 (..),
-                           U1 (..), (:*:) (..))
-import GHC.TypeLits       (KnownNat, KnownSymbol, Symbol, natVal, sameNat,
-                           sameSymbol, symbolVal)
+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
+import           Data.Typeable           (Typeable, eqT, typeRep)
+import           Data.Word               (Word16, Word32, Word64, Word8)
+import           GHC.Generics            (D1, Datatype (..), Generic (..),
+                                          K1 (..), M1 (..), U1 (..), (:*:) (..))
+import           GHC.TypeLits            (KnownNat, KnownSymbol, Symbol, natVal,
+                                          sameNat, sameSymbol, symbolVal)
 
 -- Internal imports
-import Copilot.Core.Type.Array (Array)
+import           Copilot.Core.Type.Array (Array)
 
 -- | The value of that is a product or struct, defined as a constructor with
 -- several fields.
@@ -139,7 +140,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 +166,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 +288,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 (_: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,10 @@ 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      $ \lengt' ->
+    forAll (xsInt64 lengt') $ \ls ->
       let array' :: Array n Int64
           array' = array ls
       in arrayElems array' == ls
   where
-    xsInt64 length = vectorOf length arbitrary
+    xsInt64 lengt' = vectorOf lengt' 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   $ \_ ->
       let -- Original array
           array' :: Array n Int64
           array' = array ls