Issue with HIT path constructors.

[RafaelBocquet]

This is probably roughly the same bug as #35, but as it does not involve recursive HITs, I am creating a separate issue.

It is possible to create a path p:Path T a b such that p@1 does not reduce to b:

module bug where
import prelude
A:U=undefined
B:U=undefined
f:A->B=undefined
opaque A -- to print #A instead of undefined
opaque B
opaque f

data HIT
  = iA (_:A)
  | iB (_:B)
  | gl (x:A) <i>
    [ (i=0) -> iA x
    , (i=1) -> iB (f x)
    ]

x : A = undefined
opaque x

p1 : HIT = transport (<_> HIT) (gl {HIT} x @ 1)
p : Path HIT
         (transport (<_> HIT) (gl {HIT} x @ 0))
         p1
  = <r> transport (<_> HIT) (gl {HIT} x @ r)

p1 reduces to hComp HIT (iB (comp (<_> B) (f x) [])) [], but p@1 reduces to hComp HIT (iB (f (comp (<_> A) x []))) [].

However, this works:

p : Path HIT
         (transport (<_> HIT) (gl {HIT} x @ 0))
         p1
  = <r> comp (<_> HIT) (gl {HIT} x @ r)
        [(r=0)-><i> fill (<_> HIT) (iA x) [] @ i
        ,(r=1)-><i> fill (<_> HIT) (iB (f x)) [] @ i
        ]

Maybe the definition of composition for a path constructor should depend on its system ?

[tomjack]

Should p1 and p@1 both reduce to just hComp HIT (iB (f x)) []?

I think that for a HIT with no parameters, transps/squeezes should not be applied at all to constructor arguments in transpHIT/squeezeHIT. I have attempted to fix this special case with this hack, provided without warranty of any kind: https://gist.github.com/tomjack/da36301ceb1d97c73aa15731332d0636

[spitters]

@mortberg did you ever review this fix? It would be nice to have a correct implementation of truncation.

[mortberg]

No, but we are currently working on it. It is quite subtle and we want to find a solution without hacks, hopefully we can figure it out soon.