It should be possible to have pragmas inside record definitions

[lukaszcz]

The following

instance
functorMaybeI : Functor Maybe :=
  mkFunctor@{
    {-# specialize: [1] #-}
    map {A B} (f : A -> B) : Maybe A -> Maybe B
      | nothing := nothing
      | (just a) := just (f a)
  };

currently gives an error

   |
43 |     {-# specialize: [1] #-}
   |     ^
unexpected '{'
expecting <function definition>, <identifier>, or }

Instead, the pragma should be accepted and associated with the function map.

This is needed to be able to control the optimizations for instances.