+fixTvCoEnv in_scope env
+ = fixpt
+ where
+ fixpt = mapVarEnv step env
+
+ step (co, ty) = (co', ty')
+ -- Apply fixpt one step:
+ -- Use refineType to get a substituted type, ty', and a coercion, co_fn,
+ -- which justifies the substitution. If the coercion is not the identity
+ -- then use transitivity with the original coercion
+ where
+ (co_fn, ty') = refineType (Reft in_scope fixpt) ty
+ co' | ExprCoFn co'' <- co_fn = mkTransCoercion co co''
+ | otherwise = ASSERT( isIdCoercion co_fn ) co
+
+-----------------------------
+fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv