[Agda] Overloaded constructor trouble

[G. Allais]

Hi Thorsten,

Each inductive type declares its own module so you could manually
disambiguate one of the `suc` to `ℕ.suc`. Alternatively, knowing
that overloaded constructors are disambiguated in a type-directed
way you could add a type annotation using `_∋_`. Finally you could
wait until this feature request gets added to Agda:
https://github.com/agda/agda/issues/3227

=================================================================
open import Data.Nat.Base
open import Data.Fin.Base
open import Function.Base
open import Relation.Binary.PropositionalEquality

inj-suc₁ : {m n : ℕ} → ℕ.suc m ≡ suc n → m ≡ n
inj-suc₁ = {!!}

inj-suc₂ : {m n : ℕ} → (ℕ ∋ suc m) ≡ suc n → m ≡ n
inj-suc₂ = {!!}
=================================================================

Best,
gallais

On 28/08/2020 10:22, Thorsten Altenkirch wrote:
> Ok, let’s say I want to show that suc is injective:
> 
> open import Relation.Binary.PropositionalEquality
> open import Data.Nat
> 
> inj-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n
> inj-suc = {!!}
> 
> So far so good but at some point I decide to use Fin as well.
> 
> open import Relation.Binary.PropositionalEquality
> open import Data.Nat
> open import Data.Fin
> 
> inj-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n
> inj-suc = {!!}
> 
> But now things get yellow ☹ Ok agda cannot infer which suc I want to use, even though only one actually works.
> 
> This is annoying, especially if you are writing a book and are reluctant to write
> 
> inj-suc : {m n : ℕ} → _≡_ {A = ℕ} (suc m) (suc n) → m ≡ n
> inj-suc = {!!}
> 
> instead (this is ugly).
> 
> I have two questions: are there any good workarounds? And is there a way to fix it?
> 
> Cheers,
> Thorsten
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7C057a1b476fa84199c4c008d84b33de71%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637342033433943838&sdata=kxkKQRwF50ix%2F8UdgoBjn8I00eDqR%2BZ3NH0v7bJftOc%3D&reserved=0
>