I encountered this issue while working on a possible solution for #5703. Consider the following example:
open import Agda.Builtin.Unit
open import Agda.Builtin.Equality
postulate
F : Set → ⊤
G : ⊤ → Set
mutual
X : Set
X = _
solve : {Y : Set} → X ≡ G (F Y)
solve = refl
{- ERROR:
Cannot instantiate the metavariable _5 to solution G (F Y)
since it contains the variable Y
which is not in scope of the metavariable
when checking that the expression refl has type X ≡ G (F Y)
-}
Here we get a hard error, even though eta-expanding F Y to tt leads to a valid solution. The problem is that the occurs check currently only considers singleton types for variables, but not for general expressions containing variables such as F Y.
To solve this properly, it seems like we might have to make the occurs check typed, and at every position consider whether the type is actually a singleton type so we can eta-expand the term away. Or perhaps it would be sufficient to do it for Defs and MetaVs, since these are the only ones where there's actually a chance that the type is a singleton type.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4