[Agda] problem with `abstract'

[Andreas Abel]

Thanks, I filed it as

   https://github.com/agda/agda/issues/2101

Currently,

(1) abstract definitions are abstract in type signatures always, and

(2) local definitions in an abstract definition are abstract as well.

Together this means, that Agda cannot see in the type signatures of 
seconds>0[] and g that Pair is a product type.

However, I think something is wrong with the current treatment of 
abstract in where blocks.

Either, `abstract` should not be propagated to where blocks 
automatically (the user can then decide which parts of the where block 
should be abstract).

Or, `where` blocks should get a special status (IgnoreAbstractMode).

Cheers,
Andreas

On 17.07.2016 11:28, Sergei Meshveliani wrote:
> On Sat, 2016-07-16 at 23:55 +0200, Andreas Abel wrote:
>> Sorry, I cannot see off-hand where the problem is.  Please provide
>> some self-contained test (does not have to be minimal for now).
>>
>
> -----------------------------------------------------------------
> open import Data.Product  using (_×_; proj₂)
> open import Data.List     using (List; []; map)
> open import Data.List.All using (All) renaming ([] to []a)
> open import Data.Nat      using (ℕ; _<_)
>
> abstract
>   f :  (A : Set) → A → ℕ
>   f A a =  g nil seconds>0[]
>     where
>     Pair : Set
>     Pair = A × ℕ
>
>     nil : List Pair
>     nil = []
>
>     seconds>0[] :  All (_<_ 0) (map proj₂ nil)
>     seconds>0[] =  []a
>
>     g :  (pairs : List Pair) → All (_<_ 0) (map proj₂ pairs) → ℕ
>     g _ _  =  0
> --------------------------------------------------------------------
>
> Agda 2.5.1.1 reports
>
> home/mechvel/agda/tosave/bugs/july15-2016/Last.agda:16,42-45
> Pair !=< (Data.Product.Σ (_A_16 A a) (λ _ → _B_13 A a))
> of type Set
> when checking that the expression nil has type
> List (Data.Product.Σ (_A_16 A a) (λ _ → _B_13 A a))
>
> With removed `abstract', it is type-checked.
>
> Regards,
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/