PrettyTCM TypeError instance has been moved

[UlfNorell]

From j...@stuttard.org on July 07, 2013 15:28:30

What's the problem? Cut-and-pasted program examples are preferred over attachments (if reasonably short). PrettyTCM TypeError appears to have been moved, possibly from Pretty, to Errors.hs but Agda.TypeChecking.Errors in not imported in Serialise.hs or InstanceArguments.hs. What version of Agda are you using? On what operating system (if relevant)?

Original issue: http://code.google.com/p/agda/issues/detail?id=880

[UlfNorell]

From andres.s...@gmail.com on July 08, 2013 08:08:40

Is it a current compilation problem or something else?

Status: InfoNeeded

[UlfNorell]

From j...@stuttard.org on July 08, 2013 13:51:35

I installed Agda-2.3.2.1 from hackage. What version the instance was moved from I haven't tried to bisect. Centos 6.

[UlfNorell]

From andres.s...@gmail.com on July 08, 2013 14:21:25

I installed Agda-2.3.2.1 from hackage.

So, it isn't an installation problem.

Why do you need the PrettyTCM TypeError instance imported in Serialise.hs or InstanceArguments.hs?

[UlfNorell]

From j...@stuttard.org on July 09, 2013 01:14:00

Quoting agda@googlecode.com:

Oh dear. I was *trying to install" not installed. It won't compile without these imports but does with them. Simple.

[UlfNorell]

From andres.s...@gmail.com on July 09, 2013 07:23:50

I just reinstalled Agda 2.3.2.1 from Hackage and I couldn't reproduce the issue. Which is the output of the following commands:

$ cd tmp $ cabal unpack Agda-2.3.2.1 $ cd Agda-2.3.2.1/ $ cabal install

[UlfNorell]

From j...@stuttard.org on July 10, 2013 00:22:56

cabal get Agda worked fine with cabal install (Cabal-1.17.0, ghc-7.6.3 x86-64, Centos-6); so I'd found a fix for the wrong problem which was that I always use cabal-meta --dev (cabal-meta-0.4, cabal-dev-0.9.2, Cabal-1.17.0).

I had no idea that it's dependency analysis could behave differently from plain cabal.

cabal-meta --dev install produced:

"rc/full/Agda/TypeChecking/Serialise.hs:219:17: Could not deduce (PrettyTCM TypeError) arising from a use of `prettyTCM' from the context (EmbPrj a) bound by the type signature for decode :: EmbPrj a => ByteString -> TCM (Maybe a) at src/full/Agda/TypeChecking/Serialise.hs:180:11-49 Possible fix: add an instance declaration for (PrettyTCM TypeError)"

I get the same error with cabal-dev, so I should have a look at that. Sorry for taking up your time.

[UlfNorell]

From andres.s...@gmail.com on July 10, 2013 04:41:36

I get the same error with cabal-dev, so I should have a look at that.

cabal-dev works for me:

$ ghc --version The Glorious Glasgow Haskell Compilation System, version 7.6.3

$ cabal-dev --version cabal-dev 0.9.2 built with Cabal 1.16.0.3

$ cabal-dev update

$ cabal-dev install Agda ... Registering Agda-2.3.2.1... Installed Agda-2.3.2.1

Status: Invalid

[UlfNorell]

From j...@stuttard.org on July 10, 2013 05:56:35

Weird but thanks for letting us know.

[UlfNorell]

From guillaum...@gmail.com on July 10, 2013 06:31:04

When reporting a bug like this one, you should always include the exact command lines needed to reproduce it and the exact error messages you obtain. It’s very hard for other people to help you otherwise.

[UlfNorell]

From andres.s...@gmail.com on July 10, 2013 07:16:23

cabal-meta also works for me:

$ cabal-meta --version cabal-meta 0.4.1.2

$ cat sources.txt Agda-2.3.2.1

$ cabal-meta --dev install ... Registering Agda-2.3.2.1... Installed Agda-2.3.2.1