Behaviour of Idris' pretty-printing in the REPL

[Dominic Mulligan]

Hi,

I have a heap data type with the following Show instance:

instance Show a => Show (MaxiphobicHeap a) where
show Empty = "Empty"
show (Node s l e r) = "Node (" ++ show l ++ " " ++ show e ++ " " ++
show r ++ " )"

I'm trying to debug the insertion of elements into the heap, but
coming across an annoying problem, namely that Idris suddenly changes
how it prints out the result of evaluation for all but the simplest of
heaps. Namely:

show $ prelude.heap.fromList [1]

causes Idris to spit out:

"Node (Empty 1 Empty)" : String

which is good, but the slightly more complex call:

show $ prelude.heap.fromList [1, 2]

causes Idris to produce:

show $ (prelude.heap.fromList (prelude.list.:: O (prelude.list.:: (S
(S O)) (prelude.list.Nil)))) : String

as if the Show instance is being ignored, or something is not being
fully evaluated behind the scenes. This behaviour's a major
impediment. Is it intentional? Is there some way to change it?

Thanks,
Dom

[Edwin Brady]

Hi Dom,
Is this with the latest git version? It's possible that some of the tinkering I've been doing today has caused this... I'll investigate properly tomorrow, but it's not impossible that today's experiment with the evaluator has had an unfortunate side effect...

(Normally the git version is quite safe, but only because I never commit without rebuilding the prelude, running the tests, and building the tutorial examples - experience suggests this saves a lot more time than it takes. If anything odd happens, my rule of thumb is that it should become a test.)

Edwin.

[Dominic Mulligan]

Hi Edwin,

Yeah, it's the latest Git version.

For what it's worth, type checking the following simple file takes a
surprisingly large amount of time, even more if the file grows with
extra definitions (I'm not sure if this is related to your changes ---
however, removing the call to "show l" speeds type checking up about
3x):

module test

import builtins
import prelude.nat

%access public

abstract data MaxiphobicHeap : Set -> Set where
Empty : MaxiphobicHeap a
Node : Nat -> MaxiphobicHeap a -> a -> MaxiphobicHeap a ->
MaxiphobicHeap a

instance Show a => Show (MaxiphobicHeap a) where
show Empty = "Empty"
show (Node s l e r) = "Node (" ++ show l ++ " " ++ show e ++ " " ++
show r ++ " )"

Thanks,
Dom