Internal error at Agda/TypeChecking/Sort.hs:224:21

[MatthewDaggitt]

Internal error at Agda/TypeChecking/Sort.hs:224:21

[UlfNorell]

Looks like a bad interaction between module application and generalised variables.

open import Agda.Primitive

module P {l} (A : Set l) where
  postulate f : A → A

record _∋_ {l} (A : Set l) (x : A) : Set where

variable l : Level

works : (X : Set l) (open P X) → (X → X) ∋ f
works = _

module _ (X : Set l) (open P X) where
  fails : (X → X) ∋ f
  fails = _
  -- X !=< Issue6916.GeneralizeTel
  -- when checking that the expression f has type X → X

Inside the module we think f has type (genTel : Issue6916.GeneralizeTel) (X₁ : Set l₁) → X₁ → X₁. Interestingly it works fine when in a type signature instead of a module telescope.

And this example fails also in 2.6.1 so the sort comparison is a red herring.

[UlfNorell]

Briefly, the way generalisation works is that we type check the type or telescope to be generalised in the context of a single variable genTel of type GeneralizeTel, a freshly generated as yet undetermined record type. When generalisation is complete we fill in the record type with the variables being generalised over and compute a substitution from the context with genTel to the "real" context containing the generalised variables. When generalising a module telescope we apply this substitution to let bindings from the telescope to make sure they live in the correct context when checking the module body. This part is missing for modules created in the telescope.

For let bindings, this is easy because they are ephemeral local things, but for modules it's a bit trickier. What we need to do is create new modules applying the genTel substitution to the modules created inside the telescope, and make sure the scope checker is pointing to these modules instead of the ones from the telescope when checking the body.

Given that this is a nontrivial fix and it hasn't ever worked I think it's best to not hold up 2.6.4.1 over it.

[jespercockx]

Seems to be some bad interaction between generalization and sort inference. Debug output with -v tc.sort:60:

sortOf Issue6916.GeneralizeTel
sortOfE
  a  =  {A = A₁ : Set} → Set
  hd =  Issue6916.GeneralizeTel
  e  =  $ {_}
sortOf Level
sortOf Level
sortOf Issue6916.GeneralizeTel
sortOfE
  a  =  {A = A₁ : Set} → Set
  hd =  Issue6916.GeneralizeTel
  e  =  $ {_}
sortOf Level
sortOf Level
sortOf Level
sortOf Level
sortOf Rec _13
sortOfE
  a  =  {A = A₁ : Set} (ℓ₄ : _3) → Set₁
  hd =  Rec
  e  =  $ {_}
sortOfE
  a  =  (ℓ₄ : _3) → Set₁
  hd =  Rec
  e  =  $ _13
sortOf Rec _13
sortOfE
  a  =  {A = A₁ : Set} (ℓ₄ : _3) → Set₁
  hd =  Rec
  e  =  $ {_}
sortOfE
  a  =  (ℓ₄ : _3) → Set₁
  hd =  Rec
  e  =  $ _13
sortOf {a : record { .generalizedField-ℓ₃ = _ }} → IsS _22 a → Set
sortOf record { .generalizedField-ℓ₃ = _ }

So somehow the sortOf function is getting a pi type where the type of the domain is a record value, which is not a valid type.

[jespercockx]

Running the test with -v tc:50 -v tc.sig.param:90 the first suspicious part of the output is this:

checkApplication
  hd   =  extract
  args =  f ?
  e    =  extract (f ?)
  t    =  ?1
computing module parameters of  Issue6916._._
  cxt  =  {A = A₁ : Set} {ℓ₃ = ℓ₄ : Level} (r₁ : Rec _13)
  sub  =  emptyS, @2, Issue6916._.mkGeneralizeTel {@1}
  n    =  1
  tel  =  [{(A, Set)}]
  args =  {Issue6916._.mkGeneralizeTel {@1}}
instDef in Issue6916._.Test._: Issue6916._._.extract {A}
inferDef extract
  absolute type:     {A : Set} {genTel : Issue6916.GeneralizeTel}
                     (r : Rec _13) {a : A} →
                     r .Rec.IsS a → Set
  instantiated type: {genTel : Issue6916.GeneralizeTel}
                     (r₁ : Rec _13) {a : record { .generalizedField-ℓ₃ = _ }} →
                     r₁ .Rec.IsS a → Set

In the last line, there is the domain {a : record { .generalizedField-ℓ₃ = _ }} which is ill-formed because a record expression is not a type.

I'm not familiar enough with the generalization code (or perhaps my brain is just too tired because it's Friday afternoon) so I don't really see exactly what's going wrong. Perhaps @UlfNorell could take a look?

[andreasabel]

Still works in 2.6.1 (producing unsolved metas).

[andreasabel]

Bisection says: d867f57 is the first bad commit (ping @jespercockx)

Date: Tue Aug 25 12:38:04 2020 +0200
[ fix #4615 ] Enable --no-sort-comparison by default

The option --no-sort-comparison has been removed, so there is no --sort-comparison to turn on to try to recover the old behavior.

[plt-amy]

Is #6770 a duplicate of this?