`getDefinition` gives wrong constructor for record from applied parameterised module

[UlfNorell]

module _ where

open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat hiding (_==_)
open import Agda.Builtin.List
open import Agda.Builtin.Equality

Tactic = Term → TC ⊤

macro
  -- Get the (first) constructor of a data or record type
  `con : Name → Tactic
  `con x hole = getDefinition x >>= λ where
    (data-type _ (c ∷ _)) → unify hole (lit (name c))
    (record-type c fs)    → unify hole (lit (name c))
    _                     → typeError (strErr "bad" ∷ [])

  -- Look up the name of a name
  `typeOf : Name → Tactic
  `typeOf x hole = getType x >>= unify hole

-- Some convenience function
data ⊥ : Set where

infix 0 _∋_
_∋_ : ∀ {a} (A : Set a) → A → A
A ∋ x = x

_≢_ : ∀ {a} {A : Set a} → A → A → Set a
x ≢ y = x ≡ y → ⊥

-- If we put a data type and a record type in a parameterised module
module Param (A : Set) where

  data Data : Set where
    mkData : A → Data

  record Record : Set where
    constructor mkRecord
    field getField : A

-- and then apply the module to some argument
open Param Nat

-- getDefinition Data behaves as expected, returning a definition with a constructor
-- Data.mkData : Nat → Data
_ = `con Data           ≡ quote Data.mkData ∋ refl
_ = `typeOf Data.mkData ≡ (Nat → Data)      ∋ refl

-- Although it's interesting that we get Data.mkData and not mkData (and that these are
-- not the same).
_ = quote Data.mkData ≢ quote mkData ∋ λ ()

-- But, we don't get `Param.mkData : {A : Set} → A → Param.Data A`
_ = `con Data            ≢ quote Param.mkData             ∋ λ ()
_ = `typeOf Param.mkData ≡ ({A : Set} → A → Param.Data A) ∋ refl

-- For the record type, however, that is exactly what we get
_ = `con Record            ≡ quote Param.mkRecord             ∋ refl
_ = `typeOf Param.mkRecord ≡ ({A : Set} → A → Param.Record A) ∋ refl

-- What we should get is `mkRecord`
_ = `con Record      ≢ quote mkRecord ∋ λ ()
_ = `typeOf mkRecord ≡ (Nat → Record) ∋ refl

-- The fact that we get `Data.mkData` and not `mkData` is a clue to the problem. There
-- is no equivalent of `Data.mkData` for the record type: record constructors are not
-- part of the record module.