- forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
- flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
- HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
+ forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+ flatten_type (HaskTApp (weakF_ σ) (FreshHaskTyVar_ κ)) =
+ HaskTApp (weakF_ (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar_(n:=n) κ).