Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Build error with idris 1.3.2 #84

Open
dwarfmaster opened this issue May 11, 2020 · 2 comments
Open

Build error with idris 1.3.2 #84

dwarfmaster opened this issue May 11, 2020 · 2 comments

Comments

@dwarfmaster
Copy link

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 idris-lang/Idris-dev#4254 which seems to be related to the second error.

@marcosh
Copy link
Contributor

marcosh commented May 11, 2020

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
Copy link
Author

dwarfmaster commented May 11, 2020

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants