search

statebox / idris-stbx-core

Category theoretic semantics of glued open Petri nets in Idris
https://statebox.org/
1 stars 1 forks source link

unable to use general definition of graph #47

Open marcosh opened 4 years ago

marcosh commented 4 years ago

Using the generalize-graph branch for the idris-ct repo and the generalize-graph branch in idris-stbx-core repo, trying to compile the Computer/ComputerC module the following error is reported

./Computer/ComputerC.lidr:84:75-79:
   |
84 | > compute graph {initialVertex} {finalVertex} functor path initialValue = ?asdf
   |                                                                           ~~~~~
When checking deferred type of ComputerC.ComputerC.asdf:
Type mismatch between
        extCompose (Ty [] a9) (IO (Ty [] b10)) (IO (Ty [] b10)) f11 (MkExtensionalTypeMorphism id) = extCompose (Ty [] a9) (IO (Ty [] b10)) (IO (Ty [] b10)) f11 (MkExtensionalTypeMorphism id)
and
        extCompose (Ty [] a9) (IO (Ty [] b10)) (IO (Ty [] b10)) f11 (MkExtensionalTypeMorphism (\x => io_bind (io_pure x) id)) =
        extCompose (Ty [] a9) (IO (Ty [] b10)) (IO (Ty [] b10)) f11 (MkExtensionalTypeMorphism id)

trying to debug this, it probably has something to do with the definition of the left identity of the Kleisli category: https://github.com/statebox/idris-ct/blob/1efb34427f9d664288055234de84b6d548292806/src/Monad/KleisliCategoryHelpers.lidr#L32