20070618-1

The module Bug for some reason yields the following error message:

 Bug.agda:17,7-10
 No binding for builtin thing ZERO, use {-# BUILTIN ZERO name #-} to
 bind it to 'name'
 when checking that the expression bar has type 0 ≡ 0

If a BUILTIN ZERO pragma is added (see Bug2), then Agda panics:

 Bug2.agda:25,7-10
 Panic: Pattern match failure in do expression at
 src/full/TypeChecking/Conversion.hs:119:6-29
 when checking that the expression bar has type 0 ≡ 0

The modules are defined as follows:

 module Bug where

 postulate
   ℤ   : Set
   Float : Set
   _≡_ : ℤ -> ℤ -> Set

 {-# BUILTIN INTEGER ℤ     #-}
 {-# BUILTIN FLOAT   Float #-}

 primitive primRound : Float -> ℤ

 ℤ-0 : ℤ
 ℤ-0 = primRound 0.0

 foo : ℤ-0 ≡ ℤ-0
 foo = bar
   where postulate bar : ℤ-0 ≡ ℤ-0

 module Bug2 where

 data ℕ : Set where
   zero : ℕ
   suc  : ℕ -> ℕ

 {-# BUILTIN NATURAL ℕ    #-}
 {-# BUILTIN ZERO    zero #-}
 {-# BUILTIN SUC     suc  #-}

 postulate
   ℤ   : Set
   Float : Set
   _≡_ : ℤ -> ℤ -> Set

 {-# BUILTIN INTEGER ℤ     #-}
 {-# BUILTIN FLOAT   Float #-}

 primitive primRound : Float -> ℤ

 ℤ-0 : ℤ
 ℤ-0 = primRound 0.0

 foo : ℤ-0 ≡ ℤ-0
 foo = bar
   where postulate bar : ℤ-0 ≡ ℤ-0