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

[Apostolis Xekoukoulotakis]

If anyone wants to typecheck the code, it is in the 54th commit of
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".
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170128/e079c99c/attachment.html>