Type checker hangs and errors

[marcosh]

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

[wires]

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!

[marcosh]

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

[wires]

You can also try it out on https://glot.io/snippets/fbmhggly7t

[jfdm]

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.

[marcosh]

@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.

[wires]

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.

[Jake-Gillberg]

Any updates on this?