re. 7250: copy instanceinfo (#7251)

src/full/Agda/TypeChecking/InstanceArguments.hs

@@ -1054,15 +1054,16 @@ addTypedInstance ::
      QName  -- ^ Name of instance.
   -> Type   -- ^ Type of instance.
   -> TCM ()
-addTypedInstance = addTypedInstance' True
+addTypedInstance = addTypedInstance' True Nothing
 
 -- | Register the definition with the given type as an instance.
-addTypedInstance' ::
-     Bool   -- ^ Should we print warnings for unusable instance declarations?
-  -> QName  -- ^ Name of instance.
-  -> Type   -- ^ Type of instance.
+addTypedInstance'
+  :: Bool               -- ^ Should we print warnings for unusable instance declarations?
+  -> Maybe InstanceInfo -- ^ Is this instance a copy?
+  -> QName              -- ^ Name of instance.
+  -> Type               -- ^ Type of instance.
   -> TCM ()
-addTypedInstance' w x t = do
+addTypedInstance' w orig x t = do
   reportSDoc "tc.instance.add" 30 $ vcat
     [ "adding typed instance" <+> prettyTCM x <+> "with type"
     , prettyTCM =<< flip abstract t <$> getContextTelescope
@@ -1084,7 +1085,7 @@ addTypedInstance' w x t = do
         Map.insertWith (+) n 1
 
       let
-        info = InstanceInfo
+        info = flip fromMaybe orig InstanceInfo
           { instanceClass   = n
           , instanceOverlap = DefaultOverlap
           }
@@ -1116,7 +1117,7 @@ resolveInstanceHead q = do
   clearUnknownInstance q
   -- Andreas, 2022-12-04, issue #6380:
   -- Do not warn about unusable instances here.
-  addTypedInstance' False q =<< typeOfConst q
+  addTypedInstance' False Nothing q =<< typeOfConst q
 
 -- | Try to solve the instance definitions whose type is not yet known, report
 --   an error if it doesn't work and return the instance table otherwise.

src/full/Agda/TypeChecking/InstanceArguments.hs-boot

@@ -1,7 +1,7 @@
 module Agda.TypeChecking.InstanceArguments where
 
-import Agda.TypeChecking.Monad.Base (TCM)
+import Agda.TypeChecking.Monad.Base (TCM, InstanceInfo)
 
 import Agda.Syntax.Internal (QName, Type)
 
-addTypedInstance' :: Bool -> QName -> Type -> TCM ()
+addTypedInstance' :: Bool -> Maybe InstanceInfo -> QName -> Type -> TCM ()

src/full/Agda/TypeChecking/Monad/Signature.hs

@@ -550,7 +550,7 @@ applySection' new ptel old ts ScopeCopyInfo{ renNames = rd, renModules = rm } =
           -- Issue5583: Don't skip constructures, because the original constructor doesn't always
           -- work. For instance if it's only available in an anonymous module generated by
           -- `open import M args`.
-          whenJust inst $ \_ -> addTypedInstance' False y t
+          whenJust inst $ \_ -> addTypedInstance' False inst y t
           -- Set display form for the old name if it's not a constructor.
 {- BREAKS fail/Issue478
           -- Andreas, 2012-10-20 and if we are not an anonymous module

test/Succeed/Issue7250.agda

@@ -0,0 +1,32 @@
+module Issue7250 where
+
+open import Agda.Primitive
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Equality
+
+open import Issue7250.B
+
+-- 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

test/Succeed/Issue7250/A.agda

@@ -0,0 +1,30 @@
+module Issue7250.A 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

test/Succeed/Issue7250/B.agda

@@ -0,0 +1,9 @@
+module Issue7250.B where
+
+import Issue7250.A
+open module A′ = Issue7250.A public
+
+-- module One′ = One
+-- open One′ public
+-- open One
+-- ^ no combination helps