Idris-dev
Idris-dev copied to clipboard
Type checker hangs and errors
We're working on a library formalising (monoidal) categories and we reached a point where the type checker hangs while elaborating a type and, after more or less an hour without printing anything on the logs, it errors. I'm really at a loss here, because the code really looks correct and I am out of clues on how to proceed on this.
I isolated the issue as much as possible. It is described in an issue of the project itself, where I linked also the output of the compiler logs. In short, the issue emerges while compiling this file. I created a branch where I tried to remove a lot of noise, which could be used to try to debug the problem.
You should be able to reproduce the issue just by trying to compile the above mentioned file.
I tried looking at the logs, but the were not very helpful for me to debug the problem.
I tried compiling with the --nocoverage
flag, but that does not seem to solve the issue.
I am using version 1.3.1 of Idris
Any hint on how to solve this issue would be extremely valuable
Hi, let me add to to this that we looked with a number of people at the problem (cc @FabrizioRomanoGenovese @clayrat @andrevidela @epost and IIRC @fredrikNordvallForsberg) and we cannot seem to get it to terminate.
Please let us know how if we can provide further information or insights. Thanks a lot!
To allow an easier debugging process, I collected all the relevant code in a single file (https://gist.github.com/marcosh/6631e3de6243782bf74838ef0b97fd9c)
I'm also pasting here the whole code
module SymmetricMonoidalCategoryNotCompiling
cong2 : {f : t -> u -> v} -> a = b -> c = d -> f a c = f b d
cong2 Refl Refl = Refl
record Category where
constructor MkCategory
obj : Type
mor : obj -> obj -> Type
identity : (a : obj) -> mor a a
compose : (a, b, c : obj)
-> (f : mor a b)
-> (g : mor b c)
-> mor a c
leftIdentity : (a, b : obj)
-> (f : mor a b)
-> compose a a b (identity a) f = f
rightIdentity : (a, b : obj)
-> (f : mor a b)
-> compose a b b f (identity b) = f
record CFunctor (cat1 : Category) (cat2 : Category) where
constructor MkCFunctor
mapObj : obj cat1 -> obj cat2
mapMor : (a, b : obj cat1)
-> mor cat1 a b
-> mor cat2 (mapObj a) (mapObj b)
record NaturalTransformation
(cat1 : Category)
(cat2 : Category)
(fun1 : CFunctor cat1 cat2)
(fun2 : CFunctor cat1 cat2)
where
constructor MkNaturalTranformation
component : (a : obj cat1) -> mor cat2 (mapObj fun1 a) (mapObj fun2 a)
record Isomorphism (cat : Category) (a : obj cat) (b : obj cat) (morphism : mor cat a b) where
constructor MkIsomorphism
Inverse: mor cat b a
record NaturalIsomorphism
(cat1 : Category)
(cat2 : Category)
(fun1 : CFunctor cat1 cat2)
(fun2 : CFunctor cat1 cat2)
where
constructor MkNaturalIsomorphism
natTrans : NaturalTransformation cat1 cat2 fun1 fun2
record ProductMorphism
(cat1 : Category)
(cat2 : Category)
(a : (obj cat1, obj cat2))
(b : (obj cat1, obj cat2))
where
constructor MkProductMorphism
pi1 : mor cat1 (fst a) (fst b)
pi2 : mor cat2 (snd a) (snd b)
productIdentity :
(a : (obj cat1, obj cat2))
-> ProductMorphism cat1 cat2 a a
productIdentity {cat1} {cat2} a = MkProductMorphism (identity cat1 (fst a)) (identity cat2 (snd a))
productCompose :
(a, b, c : (obj cat1, obj cat2))
-> (f : ProductMorphism cat1 cat2 a b)
-> (g : ProductMorphism cat1 cat2 b c)
-> ProductMorphism cat1 cat2 a c
productCompose {cat1} {cat2} a b c f g = MkProductMorphism
(compose cat1 (fst a) (fst b) (fst c) (pi1 f) (pi1 g))
(compose cat2 (snd a) (snd b) (snd c) (pi2 f) (pi2 g))
productLeftIdentity :
(a, b : (obj cat1, obj cat2))
-> (f : ProductMorphism cat1 cat2 a b)
-> productCompose a a b (productIdentity a) f = f
productLeftIdentity {cat1} {cat2} a b (MkProductMorphism f1 f2)
= cong2 {f = MkProductMorphism} (leftIdentity cat1 (fst a) (fst b) f1) (leftIdentity cat2 (snd a) (snd b) f2)
productRightIdentity :
(a, b : (obj cat1, obj cat2))
-> (f : ProductMorphism cat1 cat2 a b)
-> productCompose a b b f (productIdentity b) = f
productRightIdentity {cat1} {cat2} a b (MkProductMorphism f1 f2)
= cong2 {f = MkProductMorphism} (rightIdentity cat1 (fst a) (fst b) f1) (rightIdentity cat2 (snd a) (snd b) f2)
productCategory : (cat1, cat2 : Category) -> Category
productCategory cat1 cat2 = MkCategory
(obj cat1, obj cat2)
(ProductMorphism cat1 cat2)
(productIdentity {cat1} {cat2})
(productCompose {cat1} {cat2})
(productLeftIdentity {cat1} {cat2})
(productRightIdentity {cat1} {cat2})
postulate
functor3 : (cat : Category) -> CFunctor (productCategory cat (productCategory cat cat)) cat
Associator :
(cat : Category)
-> Type
Associator cat = NaturalIsomorphism (productCategory cat (productCategory cat cat))
cat
(functor3 cat)
(functor3 cat)
data MonoidalCategory : Type where
MkMonoidalCategory :
(cat : Category)
-> (associator : Associator cat)
-> MonoidalCategory
AssociativityCoherence :
(cat : Category)
-> (associator : Associator cat)
-> Type
AssociativityCoherence cat associator = ()
cat : MonoidalCategory -> Category
cat (MkMonoidalCategory innerCat _) = innerCat
associator : (mCat : MonoidalCategory) -> Associator (cat mCat)
associator (MkMonoidalCategory _ associator) = associator
data SymmetricMonoidalCategory : Type where
MkSymmetricMonoidalCategory :
(monoidalCategory : MonoidalCategory)
-> AssociativityCoherence (cat monoidalCategory)
(associator monoidalCategory)
-> SymmetricMonoidalCategory
I noticed that if I comment out some pieces of the code, it actually compiles. Anyway, this issue still remains pretty much a mystery to me. Any hint would be highly appreciated
You can also try it out on https://glot.io/snippets/fbmhggly7t
I noticed that if I comment out some pieces of the code, it actually compiles.
It would be good to know which code being removed makes the issue go away.
@jfdm thanks for your answer
For example the code compiles (in almost 10 seconds) by removing the associator
from AssociativityCoherence
.
Another thing I noticed is that the code compiles (in more or less 50 seconds) if you comment out leftIdentity
and rightIdentity
in the definition of Category
.
Hi @jfdm , you see it in effect if you remove the SymmetricMonoidalCategory
definition, or just the AssociativityCoherence
part of the type:
data SymmetricMonoidalCategory : Type where
MkSymmetricMonoidalCategory :
(monoidalCategory : MonoidalCategory)
-> AssociativityCoherence (cat monoidalCategory)
(associator monoidalCategory)
-> SymmetricMonoidalCategory
The compiler works without this definition, but keeps running if you add it.
Any updates on this?