+hetmet_flatten x = unG (pga_flatten x)
+
+-- After the flattening pass the argument and result types of this
+-- function are identical (for any instantiation), so the flattener
+-- simply turns it into the identity function (pga_flattened_id).
+-- Its only purpose is to act as a "safe type cast" during pre-flattening
+-- type-inference/checking:
+pga_flatten ::
+ forall g x 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_flattened_id ::
+ forall g x y.
+ PGArrow g x y ->
+ PGArrow g x y
+pga_flattened_id x = x