Unsolved constraints when --no-syntactic-equality is used

[nad]

Agda does not accept the following code:

{-# OPTIONS --no-syntactic-equality #-}

open import Agda.Primitive

variable
  a : Level

postulate
  A : Set a

Unsolved constraints:

Failed to solve the following constraints:
  univSort Setω = univSort Setω

[jespercockx]

It would be easy to add this rule to the conversion algorithm, but it's unexpected that it is needed at all. This calls for some further investigation...

[nad]

The problem does not seem to have been fully solved:

{-# OPTIONS --no-syntactic-equality #-}

open import Agda.Primitive

variable
  ℓ : Level
  A : Set ℓ
  P : A → Set ℓ

Failed to solve the following constraints:
  lsuc _A.ℓ_9 = lsuc _A.ℓ_9

[nad]

{-# OPTIONS --no-syntactic-equality #-}

module _ where

module M where

_ : let open M in ∀ {a} {A : Set a} → A → A
_ = λ x → x

Failed to solve the following constraints:
  univSort Agda.Primitive.Setω = univSort Agda.Primitive.Setω

[jespercockx]

The problem here is another missing case in the isType_ function, which means Agda falls back to creating a fresh sort meta and calling checkExpr. However, the sort meta is used as a type in this function, which is not valid because it should be instantiated to Setω. Hence you get this currently unsolvable constraint. Three possible ways to fix this:

• Add the missing case to isType_
• Use the --no-sort-comparison flag
• Finish Add support for Setω+n #4609 so univSort becomes a total function

The first solution could work but there are probably many other missing cases. I'd rather remove the current implementation of isType_ and just rely on checkExpr for everything. The second solution might work (I haven't tried yet) but it is not yet clear what are the performance implications of always enabling this flag. The third solution seems best but will have to wait until the issue of syntax is sorted out.