Products don't work for subshapes

[TashiWalde]

shape-prod takes two shapes \phi and \chi and returns their product \ (t,s) -> \phi t \and \chi s.
This does not seem to work properly when \phi is introduced as a subshape of some other shape \psi.

Example:

#def bad-product --does not typecheck
  ( I J : CUBE)
  ( ψ : I → TOPE)
  ( ϕ : ψ → TOPE)
  ( χ : J → TOPE)
  ( A : U)
  : U
  := shape-prod I J ϕ χ → A

It works correctly if the definition of shape-prod is expanded to { (t,s) : I × J | ϕ t ∧ χ s }

[TashiWalde]

As a temporary fix, I have found that most of these issues can be circumvented by eta-expanding the offending shapes; for example := shape-prod I J ( \ t -> \phi t) \chi.