*)
Section HaskFlattener.
-
Ltac eqd_dec_refl' :=
match goal with
| [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
Axiom flatten_commutes_with_HaskTApp :
- 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) κ).
- Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
- flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
+ Axiom flatten_commutes_with_weakLT : forall n (Γ:TypeEnv) κ t,
+ flatten_leveled_type (weakLT_(n:=n)(Γ:=Γ)(κ:=κ) t) = weakLT_(n:=n)(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
flatten_type (g v) = g v.
apply precompose.
Defined.
+
+
+
(* useful for cutting down on the pretty-printed noise
Notation "` x" := (take_lev _ x) (at level 20).
| RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
| RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
| RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
- | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
+ | RAbsT Γ Δ Σ κ σ lev n => let case_RAbsT := tt in _
| RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
| RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
rewrite flatten_commutes_with_HaskTApp.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
simpl.
- set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
- set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
+ set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT_(n:=n)(κ:=κ)) Σ)) as a.
+ set (mapOptionTree (weakLT_(n:=n)(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
assert (a=q').
unfold a.
unfold q'.
| RVoid : ∀ Γ Δ l, Rule [] [Γ > Δ > [] |- [] @l ]
| RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ]@l] [Γ>Δ> Σ |- [substT σ τ]@l]
-| RAbsT : ∀ Γ Δ Σ κ σ l,
- Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)]
+| RAbsT : ∀ Γ Δ Σ κ σ l n,
+ Rule [(list_ins n κ Γ)> (weakCE_ Δ) > mapOptionTree weakLT_ Σ |- [ HaskTApp (weakF_ σ) (FreshHaskTyVar_ _) ]@(weakL_ l)]
[Γ>Δ > Σ |- [HaskTAll κ σ ]@l]
| RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
| Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l)
| Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q )
| Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q )
-| Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q )
+| Flat_RAbsT : ∀ Γ Σ κ σ a q n , Rule_Flat (RAbsT Γ Σ κ σ a q n)
| Flat_RAppT : ∀ Γ Δ Σ κ σ τ q , Rule_Flat (RAppT Γ Δ Σ κ σ τ q )
| Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l)
| Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 )
| RGlobal _ _ _ _ _ => "Global"
| RLam _ _ _ _ _ _ => "Abs"
| RCast _ _ _ _ _ _ _ => "Cast"
- | RAbsT _ _ _ _ _ _ => "AbsT"
+ | RAbsT _ _ _ _ _ _ _ => "AbsT"
| RAppT _ _ _ _ _ _ _ => "AppT"
| RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
| RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
| RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
| RLam Γ Δ Σ tx te x => let case_RLam := tt in _
| RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
- | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
+ | RAbsT Γ Δ Σ κ σ a n => let case_RAbsT := tt in _
| RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
| RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
apply (ileaf X).
destruct case_RAbsT.
- apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply ILeaf; simpl; intros; refine (X_ (weakLT_ ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
rewrite mapOptionTree_compose.
rewrite <- H.
reflexivity.
apply ileaf in X. simpl in *.
- apply ETyLam.
+ apply (ETyLam _ _ _ _ _ _ n).
apply X.
destruct case_RAppCo.
| RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
| RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
| RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
- | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
+ | RAbsT Γ Δ Σ κ σ lev n => let case_RAbsT := tt in _
| RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
| RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
destruct case_RAbsT.
simpl.
- destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
+ destruct lev; simpl.
+ apply nd_rule.
+ apply SFlat.
+ apply (@RAbsT Γ Δ Σ κ σ nil n).
apply (Prelude_error "RAbsT at depth>0").
destruct case_RAppCo.
| ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ) l -> Expr Γ Δ ξ (substT σ τ) l
| ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ) l
| ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l -> Expr Γ Δ ξ σ l
- | ETyLam : ∀ Γ Δ ξ κ σ l,
- Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)) (weakL l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
+ | ETyLam : ∀ Γ Δ ξ κ σ l n,
+ Expr (list_ins n κ Γ) (weakCE_ Δ) (weakLT_○ξ) (HaskTApp (weakF_ σ) (FreshHaskTyVar_ _)) (weakL_ l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
| ECase : forall Γ Δ ξ l tc tbranches atypes,
Expr Γ Δ ξ (caseType tc atypes) l ->
Tree ??{ sac : _
| ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++toString τ+++")"
| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => "("+++exprToString e+++")~(co)"
| ECast Γ Δ ξ t1 t2 γ l e => "cast ("+++exprToString e+++"):t2"
- | ETyLam _ _ _ k _ _ e => "\@_ ->"+++ exprToString e
+ | ETyLam _ _ _ k _ _ _ e => "\@_ ->"+++ exprToString e
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => "\~_ ->"+++ exprToString e
| ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
| ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e
| EBrak Γ Δ ξ ec t lev e => expr2antecedent e
| ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
| ENote Γ Δ ξ t l n e => expr2antecedent e
- | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
+ | ETyLam Γ Δ ξ κ σ l n e => expr2antecedent e
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
| ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
| ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
| EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ENote Γ Δ ξ t _ n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
- | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | ETyLam Γ Δ ξ κ σ l n e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
:= tv::::ite.
+ Definition updateITE_ {Γ:TypeEnv}{TV:Kind->Type}{κ}{n}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ)
+ : InstantiatedTypeEnv TV (list_ins n κ Γ).
+ rewrite list_ins_app.
+ rewrite <- (list_take_drop _ Γ n) in ite.
+ apply ilist_app.
+ apply ilist_chop in ite; auto.
+ apply ICons.
+ apply tv.
+ apply ilist_chop' in ite.
+ apply ite.
+ Defined.
+
Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
: UniqM WeakCoercion
:= bind t1' = @typeToWeakType Γ κ t1 ite
| ECast Γ Δ ξ t1 t2 γ l e => fun ite => bind e' = exprToWeakExpr χ e ite
; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
; return WECast e' c'
- | ETyLam _ _ _ k _ _ e => fun ite => bind tv = mkWeakTypeVar k
- ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
+ | ETyLam _ _ _ k _ _ n e => fun ite => bind tv = mkWeakTypeVar k
+ ; bind e' = exprToWeakExpr χ e (updateITE_ tv ite)
; return WETyLam tv e'
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => bind t1' = typeToWeakType σ₁ ite
; bind t2' = typeToWeakType σ₂ ite
Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
+
Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
:= fun TV env => TAll κ (σ TV env).
Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
unfold InstantiatedCoercionEnv; simpl.
apply vec_cons; auto.
Defined.
+
(* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
-Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
- := ilist_tail ite.
+Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := ilist_tail ite.
+Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
+Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv := fun TV ite => (cv' TV (weakITE ite)).
+Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂ := fun TV ite => lt TV (weakITE ite).
+Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt.
+Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂ := match lt with t @@ l => weakT t @@ weakL l end.
+Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
+ : InstantiatedCoercionEnv TV CV Γ Δ.
+ intros.
+ unfold InstantiatedCoercionEnv; intros.
+ unfold InstantiatedCoercionEnv in ice.
+ unfold weakCE in ice.
+ simpl in ice.
+ rewrite <- map_preserves_length in ice.
+ apply ice.
+ Defined.
+Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
+ unfold HaskCoercionKind in *.
+ intros.
+ apply hck; clear hck.
+ inversion X; subst; auto.
+ Defined.
+Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
+ fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
+Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
+ forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
+ := fun TV ite tv => (f TV (weakITE ite) tv).
+
+
Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
-Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
- := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
-Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
- := fun TV ite => (cv' TV (weakITE ite)).
Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
induction κ; auto. apply weakV; auto. Defined.
-Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
- := fun TV ite => lt TV (weakITE ite).
-Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
- := map weakV lt.
Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
induction κ; auto. apply weakT; auto. Defined.
Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
apply lt.
apply X.
Defined.
-Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
- rewrite <- ass_app in lt.
- exact lt.
- Defined.
Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
induction κ; auto. apply weakL; auto. Defined.
-Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
- := match lt with t @@ l => weakT t @@ weakL l end.
Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
:= match lt with t @@ l => weakT' t @@ weakL' l end.
Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
induction κ; auto. apply weakCE; auto. Defined.
-Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
- : InstantiatedCoercionEnv TV CV Γ Δ.
- intros.
- unfold InstantiatedCoercionEnv; intros.
- unfold InstantiatedCoercionEnv in ice.
- unfold weakCE in ice.
- simpl in ice.
- rewrite <- map_preserves_length in ice.
- apply ice.
- Defined.
-Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
- unfold HaskCoercionKind in *.
- intros.
- apply hck; clear hck.
- inversion X; subst; auto.
- Defined.
Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
induction κ; auto.
apply weakCK.
Defined.
Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
map weakCK' hck.
-Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
- fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
-Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
- forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
- := fun TV ite tv => (f TV (weakITE ite) tv).
+
+Definition weakITE_ {Γ:TypeEnv}{κ}{n}{TV}(ite:InstantiatedTypeEnv TV (list_ins n κ Γ)) : InstantiatedTypeEnv TV Γ.
+ rewrite list_ins_app in ite.
+ set (weakITE' ite) as ite'.
+ set (ilist_chop ite) as a.
+ rewrite <- (list_take_drop _ Γ n).
+ apply ilist_app; auto.
+ inversion ite'; auto.
+ Defined.
+
+Definition weakV_ {Γ:TypeEnv}{κ}{n}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (list_ins n κ Γ) κv.
+ unfold HaskTyVar; intros.
+ unfold HaskTyVar in cv'.
+ apply (cv' TV).
+ apply weakITE_ in env.
+ apply env.
+ Defined.
+
+Definition weakT_ {Γ}{κ}{n}{κ₂}(lt:HaskType Γ κ₂) : HaskType (list_ins n κ Γ) κ₂.
+ unfold HaskType; intros.
+ apply lt.
+ apply weakITE_ in X.
+ apply X.
+ Defined.
+Definition weakL_ {Γ}{κ}{n}(lev:HaskLevel Γ) : HaskLevel (list_ins n κ Γ).
+ unfold HaskLevel; intros.
+ unfold HaskLevel in lev.
+ eapply map.
+ apply weakV_.
+ apply lev.
+ Defined.
+Definition weakLT_ {Γ}{κ}{n}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (list_ins n κ Γ) κ₂ :=
+ match lt with t@@l => weakT_ t @@ weakL_ l end.
+Definition weakCK_ {Γ}{κ}{n}(hck:HaskCoercionKind Γ) : HaskCoercionKind (list_ins n κ Γ).
+ unfold HaskCoercionKind; intros.
+ unfold HaskCoercionKind in hck.
+ apply hck.
+ apply weakITE_ in X.
+ apply X.
+ Defined.
+Definition weakCE_ {Γ:TypeEnv}{κ}{n}(Δ:CoercionEnv Γ) : CoercionEnv (list_ins n κ Γ) := map weakCK_ Δ.
+Definition weakF_ {Γ:TypeEnv}{n}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
+ forall TV (env:@InstantiatedTypeEnv TV (list_ins n κ Γ)), TV κ -> RawHaskType TV κ₂.
+ intros.
+ apply f.
+ apply weakITE_ in env.
+ apply env.
+ apply X.
+ Defined.
+Definition weakCV_ {Γ}{Δ}{κ}{n}(cv':HaskCoVar Γ Δ) : HaskCoVar (list_ins n κ Γ) (weakCE_ Δ).
+ unfold HaskCoVar; intros.
+ unfold HaskCoVar in cv'.
+ apply (cv' TV).
+ apply weakITE_ in env.
+ apply env.
+ unfold InstantiatedCoercionEnv.
+ unfold InstantiatedCoercionEnv in cenv.
+ replace (length (@weakCE_ _ κ n Δ)) with (length Δ) in cenv.
+ apply cenv.
+ unfold weakCE_.
+ rewrite <- map_preserves_length.
+ reflexivity.
+ Defined.
+
+Definition FreshHaskTyVar_ {Γ}(κ:Kind) : forall {n}, HaskTyVar (list_ins n κ Γ) κ.
+ intros.
+ unfold HaskTyVar.
+ intros.
+ rewrite list_ins_app in env.
+ apply weakITE' in env.
+ inversion env; subst; auto.
+ Defined.
+
+
Fixpoint caseType0 {Γ}(lk:list Kind) :
IList _ (HaskType Γ) lk ->
Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
+Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
+ rewrite <- ass_app in lt.
+ exact lt.
+ Defined.
+
Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
unfold TyVarResolver.
refine (fun tv' =>
| WETyLam tv e => let φ2 := upPhi tv φ in
weakTypeOfWeakExpr e >>= fun te =>
weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
- weakExprToStrongExpr _ (weakCE Δ) φ2
- (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
- >>= fun e' => castExpr we "WETyLam2" _ _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
+ weakExprToStrongExpr _ (weakCE_(n:=O) Δ) φ2
+ (fun x => (ψ x) >>= fun y =>
+ OK (weakCV_ y)) (weakLT_○ξ) ig _ (weakL_ lev) e
+ >>= fun e' => castExpr we "WETyLam2" _ _
+ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev 0 e')
| WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
match te with