-
Notifications
You must be signed in to change notification settings - Fork 24
Open
Description
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.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels