[Agda] Removing a deducible Size constrain leads to error.

[Andreas Abel]

Indeed, this is a bug.  --Andreas

On 28.01.2017 18:46, Apostolis Xekoukoulotakis wrote:
> If anyone wants to typecheck the code, it is in the 54th commit of
> https://github.com/xekoukou/sparrow
> <https://github.com/xekoukou/sparrow> , in the agda folder.
>
>
> This is the piece of code that I am trying to change and that creates
> the error:
>
> "
> _⊂_ : {i : Size} → {j : Size< ↑ i} → {k : Size< ↑ j} → ∀{pll ll ell rll}
> → {ind : IndexLL {i} pll ll} → (elf : LFun {_} {i} {j} {ell} {pll})
> → {{prf : usesInput elf}} → LFun {_} {j} {k} {rll} {(replLL ll ind ell)}
>
> → LFun {_} {i} {k} {rll} {ll}
> "
>
> Removing "i" from "elf" results into error into a piece of code that
> uses the constructor.
>
> "
> _⊂_ : {i : Size} → {j : Size< ↑ i} → {k : Size< ↑ j} → ∀{pll ll ell rll}
> → {ind : IndexLL {i} pll ll} → (elf : LFun {_} {_} {j} {ell} {pll})
> → {{prf : usesInput elf}} → LFun {_} {j} {k} {rll} {(replLL ll ind ell)}
>
> → LFun {_} {i} {k} {rll} {ll}
> "
>
> It seems to me though that the size of pll is deducible from "ind". ind
> is annotated to have size i which means that both "pll" and "ll" have
> size "i".
>
> The error that I see is that it considers the size of "pll" to be "j"
> and not "i".
>
>
>
>
> _______________________________________________
> 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://www.cse.chalmers.se/~abela/