Better error for ambiguous BUILTIN [FROMNAT no longer working]

[dylanede]

I have returned to an older piece of Agda code that looks like the following:

{-# OPTIONS --cubical #-}

module scratch where

open import Cubical.Data.Nat
open import Agda.Primitive

private
  variable
    ℓ ℓ' : Level

record FromNat (A : Set ℓ) : Set (lsuc ℓ) where
  field
    Constraint : ℕ → Set ℓ
    fromNat : (n : ℕ) ⦃ _ : Constraint n ⦄ → A
open FromNat ⦃ ... ⦄ public using (fromNat)

{-# BUILTIN FROMNAT fromNat #-}

Here, I now get the following error on master:

The argument to BUILTIN FROMNAT must be a defined unambiguous name
when scope checking the declaration
  {-# BUILTIN FROMNAT fromNat #-}

Am I missing something obvious?

[andreasabel]

Importing Cubical.Data.Nat already imports the BUILTIN FROMNAT via the following builtin module. Also Cubical.Data.Nat exports fromNat, thus you are creating an ambiguous name by the open statement.

module Agda.Builtin.FromNat where

open import Agda.Primitive
open import Agda.Builtin.Nat

record Number {a} (A : Set a) : Set (lsuc a) where
  field
    Constraint : Nat → Set a
    fromNat : ∀ n → {{_ : Constraint n}} → A

open Number {{...}} public using (fromNat)

{-# BUILTIN FROMNAT fromNat #-}
{-# DISPLAY Number.fromNat _ n = fromNat n #-}

The error message is misleading, though.

[dylanede]

Ah gotcha. Should this issue stay open with the aim of improving the error message then?

[andreasabel]

New error is:

Name  fromNat  is ambiguous
when scope checking the declaration
  {-# BUILTIN FROMNAT fromNat #-}