20070603-1

Try agda on this file

module TermHO where

data List (A : Set) : Set where
    []   : List A
    _::_ : A -> List A -> List A

data Rose (A : Set) : Set where
    Rose : List (Rose A) -> Rose A
-- the bug disappears if we name the constructor "rose" instead

map : forall {A B} -> (A -> B) -> List A -> List B
map f [] = []
map f (a :: as) = f a :: map f as

roseMap : forall {A B} -> (A -> B) -> Rose A -> Rose B
roseMap f (Rose l) = map (roseMap f) l

Then try again, replacing constructor Rose by rose (leave the data type name unchanged).

Notes

• This bug is somewhat related to 20070530-2 in that the problem is that declarations are allowed to shadow each other in a bad way.
• The silent exiting is an __IMPOSSIBLE__ which for some reason isn't printed.
• Fixed.