problem with inference of levels in records

[UlfNorell]

From sanzhi...@gmail.com on September 16, 2013 16:26:56

In the following "good" is fine while the body and signature of "bad" are marked in yellow. Both are fine if we change the parameter of R to not contain levels.

Tested on darcs Agda.

module TestLvl where

infixl 6 ⊔

postulate Level : Set zero : Level suc : Level → Level ⊔ : Level → Level → Level

{-# BUILTIN LEVEL Level #-} {-# BUILTIN LEVELZERO zero #-} {-# BUILTIN LEVELSUC suc #-} {-# BUILTIN LEVELMAX ⊔ #-}

record Ls : Set where constructor , field fst : Level snd : Level open Ls

record R (ls : Ls) : Set (suc (fst ls ⊔ snd ls)) where field A : Set (fst ls) B : Set (snd ls)

bad : R _ bad = record { A = Set; B = Set₁ }

good : R ( , ) good = record { A = Set; B = Set₁ }

Original issue: http://code.google.com/p/agda/issues/detail?id=901

[UlfNorell]

From nils.anders.danielsson on September 17, 2013 02:46:58

Status: Accepted
Labels: Type-Defect Priority-High UniversePolymorphism

[UlfNorell]

From andreas....@gmail.com on September 18, 2013 00:24:41

The meta 1 in R is never eta-expanded somehow. I think this problem will vanish if we let whnf eta-expand metas that are projected. E.g.

fst _1

will result in

_1 := _2,_3

and then reduce to

_2

(And that would be easier to implement if Internal was a spine syntax (with post-fix projections)).

[UlfNorell]

From andreas....@gmail.com on September 18, 2013 00:25:02

Labels: Eta Meta

[UlfNorell]

From andreas....@gmail.com on October 21, 2013 13:54:07

Fixed by a large refactoring of internal syntax (took only 4 days...). :~}

Status: Fixed
Owner: andreas....@gmail.com