Occurs check does not properly handle singleton type

[jespercockx]

trafficstars

I encountered this issue while working on a possible solution for https://github.com/agda/agda/issues/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: https://github.com/agda/agda/issues/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 https://github.com/agda/agda/issues/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 :sweat_smile: 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.

[plt-amy]

@jespercockx I filed my fix at #6515; sorry about the merge conflict, but this time I can say it works. Or, at least, it doesn't not-work because of transp for PathP: checking the cubical library in-order (make cubical-test) goes normally until it hits Cubical.Homotopy.EilenbergMacLane.GradedCommTensor, which seemingly gets stuck on the definition of PP2 (going from -vtc.def.fun:10). I was hoping a more generic verbosity flag might give me something to pick through in the logs, but after half an hour of waiting for -vtc:10 to get to PP2, I gave up (at comm⨂-EM').

I wanted to make sure none of the other touchy Kan operations had similar issues, so I decided to check the benchmark module instead. Unfortunately:

Checking Cubical.Experiments.ZCohomology.Benchmarks (/home/amelia/default/Projects/agda/cubical/Cubical/Experiments/ZCohomology/Benchmarks.agda).
 Checking Cubical.ZCohomology.Groups.Torus (/home/amelia/default/Projects/agda/cubical/Cubical/ZCohomology/Groups/Torus.agda).
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/MetaVars/Occurs.hs:516:35 in Agda-2.6.4-inplace:Agda.TypeChecking.MetaVars.Occurs

From having changed the report, I can tell you that this is what exploded. I can't yet be sure how it exploded: I ran that module with the full -vtc.meta.occurs:45 to try to piece together the context in which the problematic subterm happened. There's 11 megs of log to sift through, so this is mostly conjecture, but from the larger pieces of shrapnel, I think this is what happened.

• Lots of Kan operations evaluate to primPOr, which is the internal implementation of "pattern matching" partial elements. In particular the ones for Glue and hcomp {_} {Type}.

• In primPOr φ ψ a b, a : Partial φ T and b : Partial ψ T. The type-checking side-condition isn't relevant: what is relevant is that, in a and b, the cubical primitives freely assume φ = i1 and ψ = i1. For a user to do this, they have to write extended lambdas: primPOr φ ψ (λ { (φ = i1) → ... }) .... The normaliser can't (easily?) make up extended lambdas, but it acts like it did.

• Abstracting very far away, we have something like primPOr φ ... (λ .o → the T zero) ..., where T : Type satisfies φ = i1 → T = Nat. But from a term traversal, all we see is primPOr, φ, the other formula, and the constructor zero pretending like it belongs to T instead of Nat.

The term I believe is guilty is massive; there's 3 thousand lines of log between it and the end. But on the very last line, we have the constructor expression ∣ ptSn 1 ∣ appearing in a context which I'm willing to bet evaluates to hcomp {_} {Type} {i ∨ ~ i} [another massive thing].

[jespercockx]

Ok thanks for investigating! I'll see if I can change the __IMPOSSIBLE__ to a softer failure for now, so my work here does not have to be blocked on cubical issues.

[jespercockx]

That did work for the cubical library, but it seems my changes made thing extremely slow:

real    64m12,737s
user    63m58,220s
sys     0m5,516s

(this is w/o aggressive optimization but I'm still pretty sure it didn't use to take this long).

[nad]

That did work for the cubical library, but it seems my changes made thing extremely slow:

Were these changes part of the changes that you committed?

[jespercockx]

No, the version that I merged has much improved the performance wrt to the initial draft, there should hopefully not be a noticeable slowdown.

[andreasabel]

there should hopefully not be a noticeable slowdown.

Famous last words :-D

• #6535

[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.