From e063db110a3f40e0e6c9c32bed64b8b21e7befa1 Mon Sep 17 00:00:00 2001 From: Daniil Iaitskov Date: Thu, 20 Nov 2025 11:56:17 +0300 Subject: [PATCH] warns-in-core fix warnings in copilot-core --- copilot-core/src/Copilot/Core/Type.hs | 34 +++++++++++-------- copilot-core/src/Copilot/Core/Type/Array.hs | 4 +-- copilot-core/tests/Test/Copilot/Core/Type.hs | 7 ++-- .../tests/Test/Copilot/Core/Type/Array.hs | 8 ++--- 4 files changed, 29 insertions(+), 24 deletions(-) diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs index b290810c2..d5b81a5d0 100644 --- a/copilot-core/src/Copilot/Core/Type.hs +++ b/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) diff --git a/copilot-core/src/Copilot/Core/Type/Array.hs b/copilot-core/src/Copilot/Core/Type/Array.hs index b11e8949b..63e25fb5b 100644 --- a/copilot-core/src/Copilot/Core/Type/Array.hs +++ b/copilot-core/src/Copilot/Core/Type/Array.hs @@ -53,7 +53,7 @@ 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) @@ -61,4 +61,4 @@ arrayUpdate (Array (x:xs)) n y = -- | 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') diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs index 9f9cb6d5e..bb202e5d1 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type.hs +++ b/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] diff --git a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs index e070f138b..a8119f5ea 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs +++ b/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