Internal error at CheckInternal.hs:335:10 when intentionally misusing --irrelevant-projections

[jamestmartin]

Error using Agda built from commit 6b13364:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/CheckInternal.hs:335:10 in Agda-2.6.3-02e954972546b31cab2f0a4b789f611a77557ed4bb482714a7a490bc800f52b5:Agda.TypeChecking.CheckInternal

Error using Agda 2.6.2.1 (the same error):

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/CheckInternal.hs:335:10 in Agda-2.6.2.1-088cae70c9c3b9b21f34992384e419410769fcf4698fd75fcc2f8d2fe15fce7d:Agda.TypeChecking.CheckInternal

Example:

{-# OPTIONS --irrelevant-projections #-}

open import Agda.Builtin.Equality

record Squash {ℓ} (A : Set ℓ) : Set ℓ where
  constructor squash
  field
    .unsquash : A
open Squash

.foo' : ∀ {ℓ} {A : Set ℓ} (x : A) (y : Squash A) → {!!}
foo' x y = {!!}
  where
    help : unsquash (squash x) ≡ unsquash y
    help = refl

I was intentionally using irrelevance incorrectly while trying to find an example of the sort of thing --irrelevant-projections can't prove. But I was hoping for a type error, not an internal error!

[andreasabel]

This "worked" up to Agda 2.6.0 in the sense that you got a proper error:

.(x) != unsquash y of type .A
when checking that the expression refl has type .(x) ≡ unsquash y

I'll run a bisect.

$ agda-bisect --with-cabal cabal-3.2 -w ghc-8.6.5 --good v2.6.0 --bad v2.6.1 --no-internal-error Issue5809.agda

[andreasabel]

Bisection blames commit 73ac151 (ping @jespercockx).
Date: Thu Oct 17 15:13:17 2019 +0200

[ irrelevance ] Don't reduce irrelevant definitions or projections

This is confirming my hunch/analysis that the problem is that Agda is trying to infer the type of the beta-redex unsquash (squash x) which is not supported (as it is not possible in general).

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

Lines 407 to 409 in 6b13364

	reportSDoc "tc.conv.infer" 30 $
	"inferring type of internal arg: " <+> prettyTCM arg
	targ <- infer $ unArg arg

[andreasabel]

@jespercockx: Isn't "Don't reduce irrelevant projections" an impossibility in our design of Agda's internal syntax?

1. Projections do not carry the parameter arguments.
2. They need to infer them from the object (principal argument) from which they are projecting.
3. Thus, the principal argument needs to be inferable.
4. Unreduced terms are in general not inferable. Even constructors are not inferable (because overloaded).

Though, I can relate to the wish to get rid of the DontCare printing (e.g., .(true) != true).

One way to solve this dilemma is to consider irrelevant projections as neither projections nor projection-like. So they would be Defs carrying all the parameters.