Reexported instances lose overlap flags
cmcmA20 opened this issue · 0 comments
cmcmA20 commented
Agda master (761869c).
Reproducer is naturally split into three files:
{-# OPTIONS --safe #-}
module One where
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
record Whatever {a} (A : Set a) : Set a where
no-eta-equality
field go : A → A
open Whatever ⦃ ... ⦄ public
instance
Whatever-generic : {a : Level} {A : Set a} → Whatever A
Whatever-generic .go = λ x → x
{-# INCOHERENT Whatever-generic #-}
private
test₁ : Bool
test₁ = go true
_ : test₁ ≡ true
_ = refl
test₂ : Nat
test₂ = go 42
_ : test₂ ≡ 42
_ = refl
{-# OPTIONS --safe #-}
module Two where
import One
open module One′ = One public
-- module One′ = One
-- open One′ public
-- open One
-- ^ no combination helps
{-# OPTIONS --safe #-}
module Three where
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Two
-- open One′
-- ^ no luck again
instance
Whatever-Bool : Whatever Bool
Whatever-Bool .go false = true
Whatever-Bool .go true = false
{-# OVERLAPPABLE Whatever-Bool #-}
-- ^ practically wrong annotation but it's good to trigger the bug
-- {-# OVERLAPPING Whatever-Bool #-}
private
test₁ : Bool
test₁ = go false
_ : test₁ ≡ true
_ = refl
test₂ : Nat
test₂ = go 42
_ : test₂ ≡ 42
_ = refl
Observe the error, local instance is correctly displayed as [overlappable]
but imported one has no [incoherent]
flag and instance resolution fails:
_r_5 : Whatever Bool [ at /home/turyansky/Projects/InstanceBug/Three.agda:24,11-13 ]
———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
Resolve instance argument _r_5 : Whatever Bool
Candidates
Whatever-generic : {a : Level} {A : Set a} → Whatever A
[overlappable] Whatever-Bool : Whatever Bool
(stuck)
One.Whatever.go _r_5 false = true : Bool (blocked on _r_5)
cc: @plt-amy