Agda Nat exports Unit somehow

[thomas-lamiaux]

I was working on a file and I couldn't get how I was using Unit without importing it. Turned out it was exported by imported Nat. I couldn't figure out where it is imported publicly. I was thinking that this is a bit weird and shouldn't be?

I don't know if there is a link but I have noticed that the Nat Builtin imports the Bool Bultin and I haven't found a reason for that either

{-# OPTIONS --without-K --safe --no-universe-polymorphism
            --no-sized-types --no-guardedness --no-subtyping #-}

module Agda.Builtin.Nat where

**open import Agda.Builtin.Bool**

data Nat : Set where
  zero : Nat
  suc  : (n : Nat) → Nat

{-# BUILTIN NATURAL Nat #-}

[mortberg]

I'm confused, what does Agda.Builtin.Nat exporting Bool have to do with Unit?

No matter what it seems weird that Agda.Builtin.Nat imports Agda.Builtin.Bool if it doesn't have to. Seems like an issue for agda (unless there already is an open such issue)

[thomas-lamiaux]

Yes indeed no link.

I find the Unit. Nat exports Nat.Literals that in turn exports some things publicly. Is that normal :

• Base is not self contained
• The export of unit is public ?

[MatthiasHu]

the Nat Builtin imports the Bool Bultin and I haven't found a reason for that

It does use Bool (for example in _==_ : Nat → Nat → Bool), so this is fine.

[MatthiasHu]

The reason why Nat re-exports Unit is that the constructor tt : Unit has to be available as an instance for the fromNat function whenever a literal like 0 is used. (I just deleted the public re-export and waited for errors to find this out.)

I agree that this can be a little bit unexpected. But do we want to fix it? Use a custom NatFromNatTrivialConstraint type instead of of the Unit?

[MatthiasHu]

And a general "pro tip": C-c C-w tells you why something (e.g. Unit) is in scope. (In emacs.)