"forwardHIT: neutral b" error in hit branch, but not master

[PaulGustafson]

Type checking the "alpha" function below with the hit branch of cubicaltt gives a "forwardHIT: neutral b" error. When using the master branch, it type checks without any errors.

module broken where

data Bool =  true | false

data Join (A : U) (B : U) = joinl (a : A)
                          | joinr (b : B)
                          | join (a:A) (b : B) <i> [(i=0) -> joinl a, (i=1) -> joinr b]

Path (A : U) (a0 a1 : A) : U = PathP (<i> A) a0 a1

S1 : U = Join Bool Bool
S2 : U = Join Bool S1

compPath (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c =
  <i> comp (<j>A) (p @ i) [ (i = 1) -> q, (i=0) -> <j> a ]

merid (A : U) (a : A) : (Path (Join Bool A) (joinl true) (joinl false)) =
  <i> compPath (Join Bool A) (joinl true) (joinr a) (joinl false)
                       (<i> join {Join Bool A} true a @ i)
                       (<i> (join {Join Bool A} false a) @-i) 
  		       @ i

-- A modified version of the main map alpha from 8, which is equal to the
-- other one (to be checked) but pointed by reflexivity
alpha : Join S1 S1 -> S2 = split
  joinl x   -> (joinl true)
  joinr y   -> (joinl true)
  join x y @ i -> (compPath S2 (joinl true) (joinl false) (joinl true) (merid S1 x) (<j>merid S1 y@-j))@i

[mortberg]

The problem is that our test whether a parameter is recursive or not is not smart enough. We evaluate the type of x and get Join Bool Bool and because this is a constructor of Join itself forwardsHIT believes Join is recursive... Maybe we should tag the recursive arguments somehow instead of trying to figure it out on the fly?