Closed UlfNorell closed 10 years ago
UlfNorell
commented
10 years ago From mech...@botik.ru on September 19, 2013 07:40:09
Please use the second attachement. Because the first has *agdai files (that make the archive large).
(I would like to replace the attachement).
Attachment: sep19-2013.zip
UlfNorell
commented
10 years ago From andreas....@gmail.com on September 23, 2013 09:24:07
I do not find the error message surprising. You want to construct an UpDSet, but M.dReducIdeal' constructs an M.ReductionIdeal, so you get an error. I cannot see a bug in Agda here, so I am closing this issue. If there is really a bug, please reopen this issue, providing a sensible example.
Status: Invalid
UlfNorell
commented
10 years ago From mech...@botik.ru on September 23, 2013 10:05:15
Indeed, it needs to be upDSet′ rather than M.dReducIdeal′. This is my attention fail. I am sorry for disturbance.
From mech...@botik.ru on September 19, 2013 16:32:43
This is on Agda of dracs of August ~20 20013, MAlonzo.
The checker treats a record constructor M.dReducIdeal′ in a strange way.
The precise code is attached.
Here is a brief description. ResDSet.agda has
... open import AlgClasses3 using (module IdealPack)
module ResidueI-set-pack (α α= ℓp : Level) (upR1 : UpRingWithOne α α=) where ... module M = IdealPack α α= ℓp upR1
residueUpDSet : M.DReductionIdeal → UpDSet α ℓp residueUpDSet rdI = M.dReducIdeal′ rDecSetoid rDSet -- record{ decSetoid = rDecSetoid; dSet = rDSet }
where
...
dReducIdeal′ is the constructor for record DreductionIdeal defined in a parameterized module IdealPack
The type checker reports
/home/mechvel/doconA/0.03/reports/sep19-2013/ResDSet.agda:104,39-49 (DecSetoid α ℓp) !=< M.UpIdeal of type (Set (Level.suc ℓp ⊔ Level.suc α)) when checking that the expression rDecSetoid has type M.UpIdeal
If we avoid the record constructor usage by replacing the RHS of this line with = record{ decSetoid = rDecSetoid; dSet = rDSet } , then it is type-checked.
The impression is that the checker misunderstans the type of this constructor, when it is imported between parametric modules.
On the other hand, I tried to model the effect by a simple example of
module ParamModuleTest0 where
module Pack1 (A : Set) where record Foo (B : Set) : Set where constructor fooCons
module ParamModuleTest where open import Data.Nat using (ℕ) open import ParamModuleTest0 using (module Pack1)
module Pack2 (A : Set) where module M = Pack1 A
f : M.Foo ℕ
f = M.fooCons (\ _ → 0)
And it is type-checked.
The attached code is reduced by setting `postulate' in many places, but it can be reduced further many times, because probably only the way of import matters.
Can you, please, tell: is it an error in the checker or of my own?
Attachment: sep19-2013.zip
Original issue: http://code.google.com/p/agda/issues/detail?id=909