+-- 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_unflatten ::
+ forall g x y.
+ 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 x y ->
+ PGArrow g x y
+pga_flattened_id x = x
+
+
+-- FIXME: move these and the three above to "prim" or something like that.
+
+-- Technically these functions ought to be invoked *during
+-- compilation*; in the future I would like to use Template Haskell to
+-- do that.