Skip to content

Commit 60c4484

Browse files
Merge branch 'develop-language-test-typeError'. Close #469.
**Description** `copilot-language`'s tests fail to compile with GHC 9.4. Prior versions sometimes made arbitrary decisions during type inference, whereas the new type checker will simply reject such programs. For example, compiling `copilot-language`'s tests with GHC 9.4.7 results in the following error message: ``` Build profile: -w ghc-9.4.7 -O1 In order, the following will be built (use -v for more details): - copilot-language-3.17 (test:unit-tests) (first run) Preprocessing test suite 'unit-tests' for copilot-language-3.17.. Building test suite 'unit-tests' for copilot-language-3.17.. [2 of 3] Compiling Test.Copilot.Language.Reify ( tests/Test/Copilot/Language/Reify.hs, /root/copilot/dist-newstyle/build/x86_64-linux/ghc-9.4.7/copilot-language-3.17/t/unit-tests/build/unit-tests/unit-tests-tmp/Test/Copilot/Language/Reify.o ) tests/Test/Copilot/Language/Reify.hs:737:16: error: * Could not deduce (Copilot.Core.Type.Struct t) arising from a superclass required to satisfy `Typed t', arising from a use of `observer' from the context: (Read t, Eq t, Typed t, Arbitrary t) bound by a pattern with constructor: SemanticsP :: forall t. (Typeable t, Read t, Eq t, Show t, Typed t, Arbitrary t) => ((Typeable t, Read t, Eq t, Show t, Typed t, Arbitrary t) => (Stream t, [t])) -> SemanticsP, in an equation for `checkSemanticsP' at tests/Test/Copilot/Language/Reify.hs:734:33-59 Possible fix: add (Copilot.Core.Type.Struct t) to the context of the data constructor `SemanticsP' * In the expression: observer testObserverName expr In an equation for `spec': spec = observer testObserverName expr In the expression: do let spec = observer testObserverName expr llSpec <- reify spec let trace = eval Haskell steps llSpec let expectation = take steps exprList .... | 737 | spec = observer testObserverName expr ``` **Type** - Bug: test fails to compile. **Additional context** None. **Requester** - Scott Talbert (Debian Developer & Debian Haskell Group) **Method to check presence of bug** The following Dockerfile checks that copilot-language compiles with GHC 9.4, in which case it prints the message Success: ```Dockerfile FROM ubuntu:focal RUN apt-get update RUN apt-get install --yes libz-dev RUN apt-get install --yes git RUN apt-get install --yes wget RUN mkdir -p $HOME/.ghcup/bin RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup RUN chmod a+x $HOME/.ghcup/bin/ghcup ENV PATH=$PATH:/root/.ghcup/bin/ ENV PATH=$PATH:/root/.cabal/bin/ RUN apt-get install --yes curl RUN apt-get install --yes gcc make libgmp3-dev g++ SHELL ["/bin/bash", "-c"] RUN ghcup install ghc 9.4.7 RUN ghcup install cabal 3.8 RUN ghcup set ghc 9.4.7 RUN cabal update CMD git clone $REPO && \ cd $NAME && \ git checkout $COMMIT && \ cd copilot-language && \ cabal test . && \ echo Success ``` Command (substitute variables based on new path after merge): ``` $ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-469 ``` **Expected result** Running the above docker image should print the message success, indicating that the tests can be compiled without errors (the image also checks that they run successfully, although for this case we only really care about the fact that it compiles). **Proposed solution** Add type annotation to `spec` in `checkSemanticsP`, to help GHC's type inference engine. Comment the change to make sure that future changes do not remove the signature. **Further notes** None.
2 parents 7cb9a4e + e25c7af commit 60c4484

File tree

2 files changed

+9
-2
lines changed

2 files changed

+9
-2
lines changed

copilot-language/CHANGELOG

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
2023-12-17
2+
* Add type annotation to help type inference engine. (#469)
3+
14
2023-11-07
25
* Version bump (3.17). (#466)
36

copilot-language/tests/Test/Copilot/Language/Reify.hs

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ import qualified Copilot.Language.Operators.Integral as Copilot
3131
import qualified Copilot.Language.Operators.Mux as Copilot
3232
import qualified Copilot.Language.Operators.Ord as Copilot
3333
import Copilot.Language.Reify (reify)
34-
import Copilot.Language.Spec (observer)
34+
import Copilot.Language.Spec (Spec, observer)
3535
import Copilot.Language.Stream (Stream)
3636
import qualified Copilot.Language.Stream as Copilot
3737

@@ -732,7 +732,11 @@ semanticsShowK steps (SemanticsP (expr, exprList)) =
732732
checkSemanticsP :: Int -> [a] -> SemanticsP -> IO Bool
733733
checkSemanticsP steps _streams (SemanticsP (expr, exprList)) = do
734734
-- Spec with just one observer of one expression.
735-
let spec = observer testObserverName expr
735+
--
736+
-- Because SemanticsP is an existential type, we need to help GHC figure
737+
-- out the type of spec.
738+
let spec :: Spec
739+
spec = observer testObserverName expr
736740

737741
-- Reified stream (low-level)
738742
llSpec <- reify spec

0 commit comments

Comments
 (0)