-- type-inference/checking:
pga_flatten ::
forall g x y.
- <[ y ]>@g ->
- PGArrow g (GArrowUnit g) y
+ <[ x -> y ]>@g ->
+ PGArrow g x y
pga_flatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
pga_unflatten ::
forall g x y.
- PGArrow g (GArrowUnit g) y ->
- <[ y ]>@g
+ PGArrow g x y ->
+ <[ x -> y ]>@g
pga_unflatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
pga_flattened_id ::
forall g x y.
- PGArrow g (GArrowUnit g) y ->
- PGArrow g (GArrowUnit g) y
+ PGArrow g x y ->
+ PGArrow g x y
pga_flattened_id x = x