package test1 (X :: Type) (Y:: Type) where
  
  XY  :: Type
      = sig{x :: X;
            y :: Y;
           }

  f   (x' :: X)
      (y' :: Y)
     :: XY
     =    struct {
            x = x';
            y = y';}

  g (xy:: XY)
    :: X
    = xy.x

  {- If one tries in the following goal
     agda-compute-whnf one obtains as result
     that g(f x' y') reduces to x'
  -}

  h (x' :: X)
     (y' :: Y)
     :: X
     = {!g(f x' y')   !}