Seemingly incorrect warning for abstract definition without type signature

[endobson]

I recently upgraded from 2.6.1 to 2.6.2 and am working through fixing my code base to make it work with the changed treatment of abstract.

One of the new warnings about abstract definitions without type signatures still happens to me when there is a type signature.

https://gist.github.com/endobson/7d4949309e36a5a3bcec07770bcae488

{-# OPTIONS --cubical --safe --exact-split #-}

module broken where

open import Level public
  using    ( Level )
  renaming ( zero to ℓ-zero
           ; suc  to ℓ-suc
           ; _⊔_  to ℓ-max
           )

Type : (ℓ : Level) → Set (ℓ-suc ℓ)
Type ℓ = Set ℓ

private
  variable
    ℓD ℓ< : Level

record LinearOrderStr (D : Type ℓD) (ℓ< : Level) : Type (ℓ-max (ℓ-suc ℓ<) ℓD) where
  no-eta-equality
  field
    _<_ : D -> D -> Type ℓ<

module _ {D : Type ℓD} {{S : LinearOrderStr D ℓ<}} where
  open LinearOrderStr S public


module _ {D : Type ℓD} {O : LinearOrderStr D ℓ<}
          where
  private
    module O = LinearOrderStr O
    instance
      IO = O

  abstract
    broken : {b c : D} -> (b < c) -> b < c
    broken {b} {c} b<c = b<c
      where
      b<c2 : b < c
      b<c2 = b<c

With Agda version 2.6.2 I get the following error:

———— All done; warnings encountered ————————————————————————

/Users/endobson/proj/agda/broken.agda:40,7-17
Missing type signature for abstract definition b<c2.
Types of abstract definitions are never inferred since this would
leak information that should be abstract.
when checking that the clause
broken {b} {c} b<c = b<c
  where
    abstract
      syntax b<c2 ...
      postulate b<c2 : b < c
    abstract b<c2 = b<c
has type {b c : D} → b O.< c → b O.< c

But b<c2 has a type signature. I have a workaround by rearranging the code, which usually involves a child module.

[UlfNorell]

@endobson Nothing to do with the issue, but do you know that instead of

module _ {D : Type ℓD} {{S : LinearOrderStr D ℓ<}} where
  open LinearOrderStr S public

you can say

open LinearOrderStr {{...}}

and instead of

module _ {D : Type ℓD} {O : LinearOrderStr D ℓ<}
          where
  private
    module O = LinearOrderStr O
    instance
      IO = O

you can make O an instance argument

module _ {D : Type ℓD} {{O : LinearOrderStr D ℓ<}} where

[endobson]

I did not know about the first one. But the second one does a slightly different thing in my experience, when used with multiple chained arguments it requires that all such ones have visible instance at the call site instead of just the most complicated one. I also found that performance of instance search for the call sites was noticeably slower if I did it that way.

Here is what my less minimal code looks like:
https://github.com/endobson/agda/blob/df803c313ae83603eb8943b724d3b1039eebc711/order.agda#L90

[andreasabel]

Picked onto maint-2.6.2, scheduled for 2.6.2.1.