Issue 777 [Re: [Agda] Semigroup.Carrier in 2.3.2]

[Andreas Abel]

Your example below works under Agda 2.3.2 if we bring H into scope with 
{H = H}:

   powerToPositive {H = H} x e e>0 =  pow e e e>0
        where
        open Semigroup {{...}}
        pow : Nat -> (e : Nat) -> e > 0 -> Carrier

However, this should not be necessary, I filed this as bug 777.

Cheers,
Andreas

On 30.12.12 5:14 PM, Serge D. Mechveliani wrote:
> On Tue, Dec 25, 2012 at 09:26:00AM +0100, Andreas Abel wrote:
>> Instance search is experimental, so it is likely not all things work
>> the same.
>>
>> Could you please attach a test case I can try directly without have
>> to do imports, renaming etc.?
>
>
> See the attachment to this letter:   Main.agda.zip.
>
> The first variant there works under  Agda-2.3.0.1
> but not under                        Agda-2.3.2.
>
> The second variant is commented out,
> it "fixes" the code for 2.3.2 by making the argument explicit.
>
> Which Agda version is more correct at this point?
>
> Regards,
>
> ------
> Sergei
>
>
>> On 23.12.12 12:09 PM, Serge D. Mechveliani wrote:
>>> People,
>>> this program is accepted in by Agda-2.3.0.1
>>> and rejected by                Agda-2.3.2 :
>>>
>>> ---------------------------------------------------------------
>>> powerToPositive : {c l : Level} -> {H : Semigroup c l} ->
>>>              let C = Semigroup.Carrier H in  C -> (e : Nat) -> e > 0 -> C
>>> --
>>> -- Power  x  to a positive degree  e.  The binary method.
>>>
>>> powerToPositive x e e>0 =  pow e e e>0
>>>       where
>>>       open Semigroup {{...}}
>>>       pow : Nat -> (e : Nat) -> e > 0 -> Carrier
>>>          -- cnt  is the counter used in termination proof
>>>
>>>       pow 0         _             _  = x
>>>       pow _         0             ()
>>>       pow _         (suc 0)       _  = x
>>>       pow (suc cnt) (suc (suc e)) _  =
>>>                                (if even? e then  p * p  else (p * p) * x)
>>>                                where
>>>                                half = suc $ quot2 e
>>>                                p    = pow cnt half $ positiveHalf? e
>>> ---------------------------------------------------------------
>>>
> [..]
>

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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