Internal error in Agda.TypeChecking.MetaVars

[bafain]

Version:

2.6.3-20974a8

Code:

variable
  ℓ : _
  A : Set ℓ

Output:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE_VERBOSE__, called at src/full/Agda/TypeChecking/MetaVars.hs:1640:23

UPDATE (Andreas): This is here:

agda/src/full/Agda/TypeChecking/MetaVars.hs

Line 1640 in 52702c9

Dummy s _ -> __IMPOSSIBLE_VERBOSE__ s

[andreasabel]

Agda 2.6.0 and 2.6.1 give a proper error with a suggestion to work around:

Cannot generalize over unsolved sort metas:
  _1 at /Users/abel/play/agda/bugs/Issue5565.agda:2,7-8
Suggestion: add a `variable Any : Set _` and replace unsolved metas
by Any
Failed to solve the following constraints:
  _1 (genTel = (record { .generalizedField- = _ })) = Set

So it is a regression in 2.6.2.
However, the suggested work-around does not fly in this case.

[andreasabel]

agda-bisect says: d867f57 is the first bad commit
Date: Tue Aug 25 12:38:04 2020 +0200
[ fix #4615 ] Enable --no-sort-comparison by default

Ping @jespercockx.

[jespercockx]

The error location points to the line saying the following:

        Dummy s _  -> __IMPOSSIBLE_VERBOSE__ s

Shouldn't this also print the string with the location where the dummy was created? Or do I not understand how __IMPOSSIBLE_VERBOSE__ works?

[jespercockx]

Ah apparently I need to add -vimpossible:10 to get the location where the dummy was created:

dummyTerm: __DUMMY_TERM__, called at src/full/Agda/TypeChecking/Generalize.hs:655:111 in Agda-2.6.2-9aTC47YEw9o2PRILd34aMQ:Agda.TypeChecking.Generalize

[andreasabel]

Ah apparently I need to add -vimpossible:10 to get the location where the dummy was created:

Yeah, I often fall for this trap, too.

[andreasabel]

@jespercockx : Any chance we get this fixed for 2.6.2.1?

[jespercockx]

I'll give it a look

[jespercockx]

Here is my analysis of the problem:

1. When you write variable ℓ : _, Agda first checks the type _.
2. Since this type (like any other type) is a potential candidate for generalization, Agda does this in the context genTel : GeneralizeTel.
3. The result of elaboration of _ is the new meta _2 : _1, where _1 is a new sort meta. Note that both _1 and _2 are created in context genTel : GeneralizeTel.
4. Next, Agda will generalize over the unsolved metas (except sort metas) in the type of ℓ, for which it creates the record type record GeneralizeTel : Set where field generalizedField : _1 DUMMY
5. Finally, this results in the generalized type ℓ : {_2 : _1 DUMMY} → _2.
6. When trying to use this generalized type somewhere, the DUMMY is exposed (this didn't happen in old versions, but it does since I disabled the sort comparison step of conversion).

So the root cause of the problem is the presence of a dummy in the type of the argument of ℓ. This problem could potentially occur anytime there is a new unsolved sort meta in the type of a generalizable variable, since these depend on the record of generalized arguments in the type of the variable, yet cannot be generalized over themselves.

One reasonably principled way to solve this would be to prune the dependencies on the genTel of all unsolved sort metas in the type of a generalizable variable. This technically does not 100% preserve all possible solutions, but it's the best I can currently think of (and definitely better than turning the current warning into a hard error). So I'll see if I can implement that.

[nad]

This technically does not 100% preserve all possible solutions

This sounds bad to me.

[jespercockx]

Note that this problem only occurs when there are unsolved sort metas in the type of a generalizable variable, in which case you would anyway get a warning. For example, the problem I was thinking of could occur when you write the following:

variable
  T : Set _ → _

Here the sort of the codomain of T is an unsolved sort meta, which is not generalized over. With my patch, it is now assumed that this sort meta does not depend on any generalized arguments of T (in this case, the level of the domain).

The worst that could happen because of this in theory is that you get a hard error where you should only get unsolved constraints. However, even this situation seems hard to engineer, as generalization only happens when there are no unsolved constraints. For example, when we write this:

  postulate
    f : ∀ {ℓ} → (Set ℓ → Set ℓ) → Set
    test : f T

Agda does not throw a hard error, even though the codomain of T is determined to not depend on the level of the domain. Instead, we get the unsolved constraint Set (Agda.Primitive.lsuc _T.1_14) = _4 (blocked on _4) which prevents generalization from happening.

Maybe someone smarter than I can come up with an example where things do go wrong, but even then it would only be when you use a generalizable variable with an unsolved sort meta in its type (and you will also still see the warning "Cannot generalize over unsolved sort metas"), so I do not think this is a very serious problem.

[nad]

The worst that could happen because of this in theory is that you get a hard error where you should only get unsolved constraints.

OK. I would be more concerned if there was a situation in which Agda accepted some code which should contain unsolved metavariables. With a complicated unification algorithm such as Agda's I think it is nice if one can say that, if some code is accepted, and a person reading the code can correctly identify one way to instantiate the meta-variables, then this must be the way in which the meta-variables were instantiated.