<div dir="ltr">You should also try to print the types with implicit arguments shown. Types may look simple to a human but Agda has to worry about all the things that you would leave out of your text book.<div><div><br></div><div>You can turns this on with C-c C-x C-h or put {-# OPTIONS --show-implicit #-} at the top of the file.<div><br></div><div>/ Ulf</div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 12, 2017 at 7:35 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On Wed, 2017-01-11 at 14:21 -0500, Wolfram Kahl wrote:<br>
> On Wed, Jan 11, 2017 at 09:46:00PM +0300, Sergei Meshveliani wrote:<br>
> > And my case is different. I define standard classical algebraic<br>
> > structures: Semigroup, Group, Ring, EuclideanRing, and such, and prove<br>
> > in Agda certain well-known properties of their operations. There cannot<br>
> > appear such type expressions like above for  id id ... id.<br>
> ><br>
> > And still its type check needs 7Gb RAM and 60 minutes of time (on a 3<br>
> > GHz computer).<br>
> ><br>
> > [...]<br>
> ><br>
> > There is something strange in these 60 minutes and 7 Gb minimum.<br>
> > For example,  EuclideanRing  is far enough in the hierarchy.<br>
> > And I ask to print the type (C-c C-d)  of the function (lemma)<br>
> ><br>
> >   remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#<br>
> ><br>
> > in the module parameterized by an instance of  EuclideanRing.<br>
> > It shows<br>
> ><br>
> > (a b : UpIntegralRing.Carrier upIR) →<br>
> > (UpIntegralRing.*upMonoid upIR UpMonoid.∣ b) a →<br>
> > (upIR UpIntegralRing.≈ EuclideanRing.eucRem upIR∣? E a b)<br>
> > (UpIntegralRing.0# upIR)<br>
> ><br>
> > This does not look like a large expression<br>
> > (though it contains several parts that may need to be replaced with<br>
> > their expanded definitions, depending on situation).<br>
><br>
> Can you go to the top-level of the file module in which this is defined,<br>
> and ask for the type  (C-c C-d) of the qualified name of remByDivisor,<br>
> qualified as necessary to be able to refer to it from the top-level<br>
> of the file module?<br>
><br>
> And also do that for each of  ∣  ,  eucRem ,  ≈ , and  0# ?<br>
><br>
> If my understanding is correct, then at least in some circumstances<br>
> and to a certain degree, these are the types that Agda is really dealing with.<br>
><br>
<br>
</div></div>I have there<br>
<br>
------------------------------<wbr>--------------<br>
open import Level using (_⊔_)<br>
...<br>
...<br>
module OfEuclideanRing {α α=} (upIR∣? : UpIntegralRing-with∣? α α=)<br>
                 (open OverIntegralRing-0 upIR∣? using (EuclideanRing))<br>
                 E : EuclideanRing)<br>
  where<br>
  upIR = proj₁ upIR∣?<br>
  _∣?_ = proj₂ upIR∣?<br>
<br>
  open UpIntegralRing upIR using<br>
                           (setoid; ... _≈_;  ... 0#; ... *upMonoid)<br>
                           renaming (Carrier to C)<br>
<br>
  open UpMonoid *upMonoid using (_∣_; _∤_; ∣cong; ... ∣trans)<br>
                          renaming (∣∙ to ∣*; _~asd_ to _~_)<br>
  ...<br>
  open EuclideanRing E using (eucRem; ...)<br>
  ...<br>
<span class=""><br>
  remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#<br>
</span>  ...<br>
------------------------------<wbr>--------------<br>
<br>
I go to the beginning of this file and command<br>
<br>
  C-c C-d<br>
  remByDivisor<br>
<br>
And it prints its type.<br>
Now, try with the _∣_.<br>
<br>
This _∣_ instance is opened from   open UpMonoid *upMonoid,<br>
<br>
and  *upMonoid  is opened from  open UpIntegralRing upIR.<br>
<br>
What expression need I to put to the   C-c C-d   input window?<br>
I try<br>
  let *UM = UpIntegralRing.*upMonoid upIR in UpMonoid._∣_ *UM<br>
<br>
It reports<br>
<br>
---------------<br>
Structures0.DSet.Carrier<br>
(.Structures0.Magma.dS (Structures0.UpMagma.magma<br>
  (.Structures0a.UpSemigroup.<wbr>upMagma<br>
   (UpMonoid.upSemigroup (UpIntegralRing.*upMonoid upIR))))) →<br>
Structures0.DSet.Carrier<br>
(.Structures0.Magma.dS (Structures0.UpMagma.magma<br>
  (.Structures0a.UpSemigroup.<wbr>upMagma<br>
   (UpMonoid.upSemigroup (UpIntegralRing.*upMonoid upIR))))) →<br>
Set (α= ⊔ α)<br>
------------------<br>
<br>
It searches down:<br>
   UpIntegralRing --> UpMonoid --> UpSemigroup --> UpMagma --> DSet --><br>
   Carrier<br>
<br>
for each argument in the signature of  _∣_  -- as it was intended.<br>
<br>
Further:<br>
  C-c C-d<br>
  EuclideanRing.eucRem E<br>
<br>
leads to an error:<br>
------------------<br>
(OverIntegralRing-0.<wbr>EuclideanRing upIR∣?) !=<<br>
(Data.Product.Σ (UpIntegralRing (_α_0 upIR∣? E) (_α=_1 upIR∣? E))<br>
 (λ upR → Decidable₂ (Magma._∣_ (UpIntegralRing.*magma upR))))<br>
of type (Set (α= ⊔ α))<br>
when checking that the expression E has type<br>
UpIntegralRing-with∣? (_α_0 upIR∣? E) (_α=_1 upIR∣? E)<br>
------------------<br>
<br>
E  is a parameter in the head module, and  eucRem  is opened in<br>
open EuclideanRing E ...<br>
as shown above.<br>
I wonder, why does this C-c C-d fail.<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>