boundaries of nested splits

[dlicata335]

Should I be able to do the circles to torus map with nested splits?

module torustest where

data S1 = base
        | loop  [ (i=0) -> base
                   , (i=1) -> base]

data Torus = ptT
           | pathOneT  [ (i=0) -> ptT, (i=1) -> ptT ]
           | pathTwoT  [ (i=0) -> ptT, (i=1) -> ptT ]
           | squareT  [ (i=0) -> pathOneT {Torus} @ j
                           , (i=1) -> pathOneT {Torus} @ j
                           , (j=0) -> pathTwoT {Torus} @ i
                           , (j=1) -> pathTwoT {Torus} @ i ]

c2t' : S1 -> S1 -> Torus = split
  base -> split@(S1 -> Torus) with
            base -> ptT
            loop @ x -> pathTwoT{Torus} @ x
  loop @ y -> split@(S1 -> Torus) with
                base -> pathOneT{Torus} @ y
                loop @ x -> squareT{Torus} @ x @ y

I get this error, which seems like it doesn't know that the boundaries of the anonymous functions are the same?

Type checking failed: Faces in branch for "loop" don't match:
got
[ (y = 0) -> torustest_L20_C17 0, (y = 1) -> torustest_L20_C17 1 ]
but expected
[ (y = 0) -> torustest_L17_C13, (y = 1) -> torustest_L17_C13 ]

This happened in both pi4s3 and pi4s3_dimclosures.

[mortberg]

This is the expected behavior. When comparing splits in the conversion checker we only look at the name+location and in this case the computation rule for paths isn't even triggered as the boundary of the second split isn't known. So you have to do what you did before by introducing auxiliary definitions annotated with the types. I'm not sure if we can get this to work without either more annotations or type inference, so in conclusion I don't think that the nested splits are really useful for HITs in cubicaltt and I would just make auxiliary definitions (or switch to cubical Agda...).