Nested splits and path constructors

[IanOrton]

There seems to be an issue with using nested splits with HITs. See the example below:

module broken where

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

data Unit = tt

c2t' : S1 -> S1 -> Unit = split
  base -> split@(S1 -> Unit) with
    base -> tt
    loop @ _ -> tt
  loop @ _ -> split@(S1 -> Unit) with
    base -> tt
    loop @ _ -> tt

This produces the following error:

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

I think that broken_L13_C5 0 should reduce to tt, and so should broken_L10_C5 and so these systems should in fact be equal.

[mortberg]

Thanks for testing and reporting the bug! The following code works:

foo : S1 -> Unit = split
    base -> tt
    loop @ _ -> tt

c2t' : S1 -> S1 -> Unit = split
  base -> foo
  loop @ _ -> foo

So the bug seems to be with the local splits. I'll investigate.

[mortberg]

Note that his works:

foo1 : S1 -> Unit = split
  base -> tt
  loop @ _ -> tt

foo2 : S1 -> Unit = split
  base -> tt
  loop @ _ -> tt

c2t' : S1 -> S1 -> Unit = split
  base -> foo1
  loop @ _ -> foo2

But this doesn't:

c2t' : S1 -> S1 -> Unit = split
  base -> foo1
    where
    foo1 : S1 -> Unit = split
      base -> tt
      loop @ _ -> tt
  loop @ _ -> foo2
    where
    foo2 : S1 -> Unit = split
      base -> tt
      loop @ _ -> tt

I don't see what is wrong now, but if you change the conversion test for Ter (Split _ p _ _) e to constantly True all of these go through. :)