Wrong substitution in expandRecordVar

[sattlerc]

Tested with the master branch Agda version 2.5.3-153e1c8.

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:89

The trace message is:
conApp: constructor F.recCon-NOT-PRINTED with fields [F.S.A,F.S.B,F.S.z] projected by F.Σ.fst

module F where

postulate
  Path : (A : Set) → A → A → Set
  path : (A : Set) → Path _ _ _

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ public

record S : Set₁ where
  field
    A : Set
    B : (a : A) → Set
    z : (a : A) → B a

record T : Set₁ where
  field
    A : Set
    B : (a : A) → Set
    z : (a : A) → B a
    s : (a : A) → B a → B a
    p : (a : A) (f : B a) → Path _ f (s _ (z _))

f : S → T
f X = record { A = Σ _ _
             ; B = λ { (_ , _) → Σ _ _ }
             ; z = λ _ → (S.z X _ , _)
             ; s = λ _ _ → _
             ; p = λ _ _ → path _
             }

[andreasabel]

This is a regression introduced in 2.4.2.4.

[andreasabel]

Mmh, agda-bisect does not work out of the box here. My compiles seem all to fail with:

[ 68 of 287] Compiling Agda.Utils.HashMap ( src/full/Agda/Utils/HashMap.hs, dist/dist-sandbox-85104ef/build/Agda/Utils/HashMap.o )

src/full/Agda/Utils/HashMap.hs:3:5:
    Ambiguous occurrence ‘mapMaybe’
    It could refer to either ‘Agda.Utils.HashMap.mapMaybe’,
                             defined at src/full/Agda/Utils/HashMap.hs:17:1
                          or ‘HashMap.mapMaybe’,
                             imported from ‘Data.HashMap.Strict’ at src/full/Agda/Utils/HashMap.hs:8:1-37

src/full/Agda/Utils/HashMap.hs:3:5:
    Conflicting exports for ‘mapMaybe’:
       ‘module HashMap’ exports ‘HashMap.mapMaybe’
         imported from ‘Data.HashMap.Strict’ at src/full/Agda/Utils/HashMap.hs:8:1-37
       ‘mapMaybe’ exports ‘Agda.Utils.HashMap.mapMaybe’
         defined at src/full/Agda/Utils/HashMap.hs:17:1

Probably I would need a bisect-script that lowers the upper-bound for the unordered-containers package.

[nad]

Mmh, agda-bisect does not work out of the box here. [...] Probably I would need a bisect-script that lowers the upper-bound for the unordered-containers package.

You could perhaps use --cabal-option --constraint=unordered-containers==X.Y.Z (untested). However, I suggest simply using GHC 7.8.4 to build the code:

$ agda-bisect --must-fail --no-internal-error --bad 2.4.2.4 --good 2.4.2.3 --compiler <ghc-7.8.4> --log log Bug.agda
[...]
39eca6bf4a7f3c69e84f275df7c8ec4a808e14a6 is the first bad commit
commit 39eca6bf4a7f3c69e84f275df7c8ec4a808e14a6
Author: Andreas Abel <andreas.abel@ifi.lmu.de>
Date:   Sat Sep 12 18:22:29 2015 +0200

    Fixed #1316 by expanding projected vars also inside record constructors.

[...]

[andreasabel]

Thanks! I should have a look at 39eca6b of issue #1316.

[andreasabel]

The patch found by agda-bisect triggered a dormant issue: a wrong use of substitution in expandRecordVar.
After many hours of bug hunting, the fix is trivial: convert the ListTel into a Telescope before substituting!
How we all love de Bruijn indices!

[sattlerc]

Amazing work hunting that down, thanks!

[andreasabel]

Thanks for finding a bug that has been sleeping for years.