[Agda] StringOrInt function

[Philippe de Rochambeau]

Hello,

I am trying to write a function that returns either a String or a Nat depending on the first argument:

module fctypes where

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.String

StringOrInt : ∀ {ℓ} {A : Set ℓ} → Bool → A
StringOrInt True  = Nat
StringOrInt False = String

When I load the .agda file in emacs, I get the following error message:

Set !=< A
when checking that the expression Nat has type A

Is there a way in Agda to make the A Set include both Nats and Strings?

Many thanks.

Philippe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200415/4e7b1ea4/attachment.html>