Build error with idris 1.3.2

[dwarfmaster]

When running idris --build idris-ct.ipkg (or idris --checkpkg idris-ct.pkg), the build fails on CoLimits/CoProduct.lidr with the following error :

Entering directory `./src'
Type checking ./CoLimits/CoProduct.lidr
./CoLimits/CoProduct.lidr:83:5-97:48:
   |
83 | >   let
   |     ~~~ ...
When checking right hand side of composeCoProductMorphisms with expected type
        CommutingMorphism cat l r (carrier a) (carrier a) (inl a) (inr a) (inl a) (inr a)

When checking argument commutativityLeft to constructor CoLimits.CoProduct.MkCommutingMorphism:
        No such variable rewrite__impl

./CoLimits/CoProduct.lidr:119:5-133:66:
    |
119 | >   let
    |     ~~~ ...
When checking right hand side of coProductsAreIsomorphic with expected type
        Isomorphic cat (carrier a) (carrier b)

When checking an application of function Basic.Isomorphism.buildIsomorphic:
        rewriting challenger (composeCoProductMorphisms cat l r a b) to challenger (exists a (carrier a) (inl a) (inr a)) did not change type compose cat
                                                                                                                                                      (carrier a)
                                                                                                                                                      (carrier b)
                                                                                                                                                      (carrier a)
                                                                                                                                                      (challenger (exists a (carrier b) (inl b) (inr b)))
                                                                                                                                                      (challenger (exists b (carrier a) (inl a) (inr a))) =
                                                                                                                                              identity cat (carrier a)

This is on master, on NixOS.

$ idris --version
1.3.2

A quick search lead me to the following issue https://github.com/idris-lang/Idris-dev/issues/4254 which seems to be related to the second error.

[marcosh]

Thanks @dwarfmaster for reporting. I tried building locally and I have no issues. This might be an issue due to stale .ibc files. Could you try running idris --clean idris-ct.ipkg before building?

[dwarfmaster]

Thanks for the quick answer ! Unfortunately, it made no difference, I got the same error again.