agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.4k stars 339 forks source link

Reexported instances lose overlap flags #7250

Closed cmcmA20 closed 1 month ago

cmcmA20 commented 1 month ago

Agda master (761869c5fa).

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