Occurs check does not properly handle singleton type

[jespercockx]

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.

[jespercockx]

Here another variant of this issue that involves a variable rather than a postulate:

open import Agda.Builtin.Bool
open import Agda.Builtin.Unit
open import Agda.Builtin.Equality

data ⊥ : Set where

T : Bool → Set
T true  = ⊤
T false = ⊥

postulate
  F : ⊤ → Set

mutual
  X : Set
  X = _

  solve : {Y : (b : Bool) → T b} → X ≡ F (Y true)
  solve = refl

{- ERROR:
Cannot instantiate the metavariable _8 to solution F (Y true)
since it contains the variable Y
which is not in scope of the metavariable
when checking that the expression refl has type X ≡ F (Y true)
-}

Here the problem is that the occurs check currently only looks at the type of the variable Y (which is not a singleton type), but not at the type of the application Y true (which is a singleton type).

[jespercockx]

I've been slowly getting convinced that in order to deal correctly with eta-equality for the unit type, the occurs checker needs to become type-aware. Below is the example that convinced me that a purely syntactic check will never be fully satisfactory.

open import Agda.Builtin.Unit
open import Agda.Builtin.Equality

data D (A : Set) : Set₁ where
  c : ((Set → A) → A) → D A

mutual
  x : D ⊤
  x = _

  solve : {Y : Set} → x ≡ c (λ G → G Y)
  solve = refl
{-
Cannot instantiate the metavariable _8 to solution c (λ G → G Y)
since it contains the variable Y
which is not in scope of the metavariable
when checking that the expression refl has type x ≡ c (λ G → G Y)
-}

Note that in the internal representation of the solution term c (λ G → G Y), there is no trace left of the type parameter of D, since parameter arguments to constructors are erased. But if the parameter were not a singleton type, then the error would be entirely justified! So this shows that we do really need the type of the term in the occurs check.

I guess this means that we should make the occurs check type-directed. However, I am a bit scared of the potential negative impact on performance this could have. Perhaps we should instead have a way of caching the current type and context computed by the main typechecker for each term in internal syntax, so we can avoid having to recompute them each time they are needed. OTOH the memory cost of that might actually be worse.

[jespercockx]

Possible duplicate/sister issue: #2625

[jespercockx]

Slowly making progress on this at https://github.com/jespercockx/agda/tree/issue5837

[jespercockx]

I now have a version that is mostly working (it checks all of Succeed and Fail as well as the standard library), however I am stuck on a very mysterious error in the cubical library:

/home/jesper/agda/cubical/Cubical/Homotopy/Connected.agda:490,11-43
Level should be a function type, but it isn't
when checking that the expression transportRefl (cong F (merid a))
has type _f_2937 (a , _2946) ≡ _z_2931

I tried inserting additional calls to checkInternal in my typed version of the occurs checker, but these don't give me anything useful because the cubical implementation is a bit sloppy with distinguishing between Path types and function types (perhaps related to #4455?). I will continue to try to find a way around this, but perhaps @plt-amy has an idea of what else I could do here.

[plt-amy]

I'm not in a situation where I can easily compile Agda today, but I believe this is my fault. Check out the normal form of transportRefl (cong F (merid a) in that context:

λ i →
  transp {λ _ → ℓ-max ℓ ℓ'}
  (λ _ →
     PathP {ℓ-max ℓ ℓ'} (λ i₁ → P (merid (f a) i₁) .fst) (F north)
--          ^^^^^^^^^^ woops!
     (F south))
  i (λ i₁ → F (merid a i₁))

If you change these lines to read

      comp (lam "i" $ \i -> l <@> i <@> j) (lam "i" $ \ i -> bA <@> i <@> j) (phi `imax` (ineg j `imax` j))
        (lam "i'" $ \i -> combineSys (l <@> i <@> j) (bA <@> i <@> j)

does the issue disappear? If not, I'll be back home tomorrow, where I can have a better look. This code is definitely wrong; but I'm not sure whether it's the cause of what you're seeing or not.

[jespercockx]

Well it definitely makes a difference:

      Checking Cubical.Foundations.Pointed.Homogeneous (/home/jesper/agda/cubical/Cubical/Foundations/Pointed/Homogeneous.agda).
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Substitute.hs:88:26 in Agda-2.6.4-Jk6F3dGYcHrEzeqcyru3Ci:Agda.TypeChecking.Substitute

This points to the Level{} case in the applyTermE function, so it seems now a level is being applied as a function somehow.

[plt-amy]

Yeah, that one's still on me — just more recently 😅 PathP does not take a line of levels, and l has to be made into a lambda, so the patch (relative to your branch, not my patch attempt) should be

diff --git a/src/full/Agda/TypeChecking/Primitive/Cubical.hs b/src/full/Agda/TypeChecking/Primitive/Cubical.hs
index 589a2a70c7..4cdfc8be8e 100644
--- a/src/full/Agda/TypeChecking/Primitive/Cubical.hs
+++ b/src/full/Agda/TypeChecking/Primitive/Cubical.hs
@@ -358,12 +358,12 @@ doPathPKanOp (TranspOp phi u0) (IsFam l) (IsFam (bA,x,y)) = do
     -- In reality to avoid a round-trip between primComp we use mkComp
     -- here.
     comp <- mkComp $ "transport for path types"
-    [l, u0, phi] <- traverse (open . unArg) [l, u0, ignoreBlocking phi]
-    [bA, x, y] <- mapM (\ a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [bA, x, y]
+    [u0, phi] <- traverse (open . unArg) [u0, ignoreBlocking phi]
+    [l, bA, x, y] <- mapM (\ a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [l, bA, x, y]
 
     lam "j" $ \ j ->
-      comp l (lam "i" $ \ i -> bA <@> i <@> j) (phi `imax` (ineg j `imax` j))
-        (lam "i'" $ \i -> combineSys l (bA <@> i <@> j)
+      comp (lam "i" $ \i -> l <@> j) (lam "i" $ \ i -> bA <@> i <@> j) (phi `imax` (ineg j `imax` j))
+        (lam "i'" $ \i -> combineSys (l <@> j) (bA <@> i <@> j)
           [ (phi, ilam "o" (\o -> u0 <@@> (x <@> pure iz, y <@> pure iz, j)))

I poked around the modules you mentioned and I don't see anything suspicious in the normal forms anymore. With my previous suggestion, reducing the RHS of →∙Homogeneous≡ messed up the levels in combineSys (which manifested as errors when printing a primPOr subterm: for debugging, I swapped that error for a dummy), but this version is dummy-free.

I think your branch https://github.com/jespercockx/agda/tree/issue5837 is out of date: even without the fix (either version!), neither Connected or Homogeneous fail on my machine. Anyway, glancing through the other Kan operations, no other "level vs. line" confusion jumped out at me, but I'd be happy to investigate if I can reproduce the failures locally.

[jespercockx]

Now I'm getting yet another one:

/home/jesper/agda/cubical/Cubical/Algebra/Ring/Properties.agda:303,15-311,83
λ _ → ℓ-suc A != ℓ-suc ℓ of type Level
when checking that the expression
Σ≡Prop
(λ _ →
   isPropΣ (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
   λ _ →
     isPropΣ (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
     λ _ →
       isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 (λ _ _ → is-set (snd B))) _ _)
       λ _ →
         isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 (λ _ _ → is-set (snd B))) _ _)
         λ _ →
           isPropΣ (isOfHLevelPathP' 1 (isSetΠ (λ _ → is-set (snd B))) _ _)
           λ _ → isOfHLevelPathP 1 (isPropIsRing _ _ _ _ _) _ _)
(transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))
has type
transport (sym (ua (Ring≡ A B))) p ≡
transport (sym (ua (Ring≡ A B))) q

I'll also try to bring my branch up to date with latest master to see if that solves anything.

[jespercockx]

I've rebased on current master (and pushed it to my branch) but I still get the same error from my last message.

[plt-amy]

I've rebased on current master (and pushed it to my branch)

Thanks! I'll investigate.

[nad]

The bug fix breaks code and seems to have caused a massive performance regression. Furthermore the error is not that Agda accepts too much code, but that Agda rejects too much code. I'd like to use the development version of Agda, but because of this bug fix I'm mostly using Agda 2.6.3 at the moment. I suggest that the change is reverted.

[jespercockx]

I agree that the current situation is not good. I will spend the last day at the Agda meeting tomorrow to see if I can find a fix to the performance regression, and otherwise I will roll back (part of) the change to fix the performance regressions until we find a better implementation.

[jespercockx]

After working unsuccessfully on finishing my fix yesterday, we had a discussion over dinner and I conceded that my change should be rolled back for now. I will prepare a PR that rolls back the change without losing all of the work I did on refactoring and improving the old code.

[nad]

I will prepare a PR that rolls back the change without losing all of the work I did on refactoring and improving the old code.

Thanks.

[jespercockx]

Bumping this to 2.6.5, sadly.