[Agda] on `data' syntax

[Serge D. Mechveliani]

People,
can you, please, explain the issues about the following program?
(using Agda--2.3.0.1 + Standard library lib-0.6 + Prelude)

--------------------------------------------
module MyLib where
open import Foreign.Haskell
open import IO.Primitive
open import Relation.Nullary.Core
open import Data.Bool as Bool
open import Data.Nat as Nat
open import Data.String as String
open import Data.Fin 
open import Prelude using (toCostring)  -- 

PositiveNat? : Б└∙ -> Set             -- Nat -> Set
PositiveNat? 0       = T false
PositiveNat? (suc _) = T true

data IntResidue (g : Б└∙) (p : PositiveNat? g) : Set      -- definition 1
                  -- Nat
     where
     intRes : Fin g -> IntResidue g p
             
{- 
data IntResidue (g : Б└∙) : (p : PositiveNat? g) -> Set   -- definition 2
                  -- Nat
     where
     intRes : Fin g -> IntResidue g p
-}
main : IO Unit
main = putStrLn (toCostring "done")
----------------------------------------------

The intention of  IntResidue  is  
    the domain of integer residues modulo  g,  for  g > 0  only,
    represented by the set  {0, ..., g - 1}.

definition 1  is compiled,  
and  definition 2   is not compiled: 
                    "p not in scope"  in the line of  `intRes ...'

Must not  definition 2  be equivalent to  definition 1  ?
How to improve  definition 2  ?

Thank you in advance for explanation,

------
Sergei