[Agda] problem with `abstract'

[Andreas Abel]

Yes, but `a` is not used in the *type* of `s`, that is the difference.

But anyhow, I am doing some work on issue #2101.  Then your original 
example should check.

There is a third rule, which I was not aware of

(1') abstract definitions are not abstract in private type signatures

If declarations in a where-block are considered private, your original 
example would pass.

On 17.07.2016 16:36, Sergei Meshveliani wrote:
> On Sun, 2016-07-17 at 12:51 +0200, Andreas Abel wrote:
>> 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.
>>
>
> I doubt of whether I understand the rule. The program
>
>    abstract
>      h : ℕ → ℕ
>      h n = s a
>          where
>          a : ℕ
>          a = 0
>
>     	s : ℕ → ℕ
>         	s 0 = 0
>         	s _ = 1
>
> is type-checked, despite that `a' has a local definition.
> (?)
>
>
>> 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).
>>
>
> Call the first solution (I), the second -- (II).
>
> Suppose that you choose (II).
> Then
> a) the below program for  f  will be correct,
> b) in other modules any call for  f  will be type-checked as abstract
>     (without looking into the implementation of f).
>
> Will this be so?
>
> And what about the scheme
>
>      G x =  g (h x)
>             where
>             h1 : ...
>             ...
>
>             abstract
>               h2 : ...
>               h2 = ...
>
>             h : ...
>             ...
>             g : ...
> ?
>
> I write this when abstracting the whole  G  leads to that some of its
> calls are not type-checked, for some reason. Then, I abstract its part
> -- a large piece of a proof implemented by  h2.
> And I hope that in type-checking any call of  G,  the implementation of
> h2  will not be considered, so that the type check will be cheaper
> (I do not know of whether this works).
>
> What it will be with  G  under (I) and under (II) ?
>
> Regards,
>
> ------
> Sergei
>
>
>
>> 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
>>>
>>
>>
>
>
> _______________________________________________
> 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/