1 (*********************************************************************************************************************************)
2 (* HaskStrongTypes: representation of types and coercions for HaskStrong *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import Coq.Strings.String.
8 Require Import Coq.Lists.List.
9 Require Import General.
10 Require Import HaskKinds.
11 Require Import HaskLiterals.
12 Require Import HaskTyCons.
13 Require Import HaskCoreTypes.
14 Require Import HaskCoreVars.
15 Require Import HaskWeakTypes.
16 Require Import HaskWeakVars.
17 Require Import HaskWeak.
18 Require Import HaskCoreToWeak.
20 Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
21 Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
22 Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConTheta".
23 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
25 Definition dataConExTyVars cdc :=
26 filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (dataConExVars_ cdc)).
27 Opaque dataConExTyVars.
28 Definition dataConCoerKinds cdc :=
29 filter (map (fun x => match x with EqPred t1 t2 =>
31 coreTypeToWeakType t1 >>= fun t1' =>
32 coreTypeToWeakType t2 >>= fun t2' =>
38 end) (dataConEqTheta_ cdc)).
39 Opaque dataConCoerKinds.
40 Definition dataConFieldTypes cdc :=
41 filter (map (fun x => match coreTypeToWeakType x with
44 end) (dataConOrigArgTys_ cdc)).
46 Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc).
47 Coercion tyConNumKinds : TyCon >-> nat.
49 Inductive DataCon : TyCon -> Type :=
50 mkDataCon : forall cdc:CoreDataCon, DataCon (dataConTyCon cdc).
51 Definition dataConToCoreDataCon `(dc:DataCon tc) : CoreDataCon := match dc with mkDataCon cdc => cdc end.
52 Coercion mkDataCon : CoreDataCon >-> DataCon.
53 Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon.
56 Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
58 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
61 (* TV is the PHOAS type which stands for type variables of System FC *)
62 Context {TV:Kind -> Type}.
64 (* Figure 7: ρ, σ, τ, ν *)
65 Inductive RawHaskType : Kind -> Type :=
66 | TVar : ∀ κ, TV κ -> RawHaskType κ (* a *)
67 | TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *)
68 | TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *)
70 | TKappa : RawHaskType (★ ⇛★ ⇛★ ) (* (~~>) *)
72 | TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
73 | TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
74 | TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
75 | TCode : RawHaskType ECKind -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
76 | TyFunApp : forall (tf:TyFun) kl k, RawHaskTypeList kl -> RawHaskType k (* S_n *)
77 with RawHaskTypeList : list Kind -> Type :=
78 | TyFunApp_nil : RawHaskTypeList nil
79 | TyFunApp_cons : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl).
81 (* the "kind" of a coercion is a pair of types *)
82 Inductive RawCoercionKind : Type :=
83 mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
85 (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *)
86 Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := .
88 * This has been disabled until we manage to reconcile SystemFC's
89 * coercions with what GHC actually implements (they are not the
92 | CoVar : CV -> RawHaskCoer (* g *)
93 | CoType : RawHaskType -> RawHaskCoer (* τ *)
94 | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
95 | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
96 | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
97 | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
98 | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
99 | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
100 | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
101 | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
102 | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
106 Implicit Arguments TCon [ [TV] ].
107 Implicit Arguments TyFunApp [ [TV] ].
108 Implicit Arguments RawHaskType [ ].
109 Implicit Arguments RawHaskCoer [ ].
110 Implicit Arguments RawCoercionKind [ ].
111 Implicit Arguments TVar [ [TV] [κ] ].
112 Implicit Arguments TCoerc [ [TV] [κ] ].
113 Implicit Arguments TApp [ [TV] [κ₁] [κ₂] ].
114 Implicit Arguments TAll [ [TV] ].
116 Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
117 (*Notation "t1 ~~~> t2" := (fun TV env => (TApp (TApp TKappa (t1 TV env)) (t2 TV env))).*)
118 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
120 (* Kind and Coercion Environments *)
122 * In System FC, the environment consists of three components, each of
123 * whose well-formedness depends on all of those prior to it:
125 * 1. (TypeEnv) The list of free type variables and their kinds
126 * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility
127 * 3. (Tree ??CoreVar) The list of free value variables and the type of each one
130 Definition TypeEnv := list Kind.
131 Definition InstantiatedTypeEnv (TV:Kind->Type) (Γ:TypeEnv) := IList _ TV Γ.
132 Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
133 Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ).
134 Definition InstantiatedCoercionEnv (TV:Kind->Type) CV (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
136 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
137 Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ.
138 Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
139 Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ECKind).
140 Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
141 Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
143 Inductive HaskTypeOfSomeKind (Γ:TypeEnv) :=
144 haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ.
145 Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ].
146 Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) :=
148 haskTypeOfSomeKind κ _ => κ
150 Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind.
151 Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk :=
152 match htosk as H return HaskType Γ H with
153 haskTypeOfSomeKind _ ht => ht
155 Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType.
157 Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
158 @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
159 Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
161 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
163 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
164 := fun TV env => TAll κ (σ TV env).
165 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
166 (cv:HaskTyVar Γ κ) : HaskType Γ ★
167 := fun TV env => σ TV env (cv TV env).
168 Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:=
169 fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
170 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
171 := fun TV ite => TCon tc.
172 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
173 fun TV ite => TApp (t1 TV ite) (t2 TV ite).
174 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
175 fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
178 Context {TV:Kind -> Type }.
179 Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
182 | TAll _ y => TAll _ (fun v => flattenT (y (TVar v)))
183 | TApp _ _ x y => TApp (flattenT x) (flattenT y)
185 | TCoerc _ t1 t2 t => TCoerc (flattenT t1) (flattenT t2) (flattenT t)
187 | TCode v e => TCode (flattenT v) (flattenT e)
188 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flattenTyFunApp _ lt)
190 with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
191 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
192 | TyFunApp_nil => TyFunApp_nil
193 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT t) (flattenTyFunApp _ rest)
197 (* PHOAS substitution on types *)
198 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
201 flattenT (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
203 Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20).
204 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
205 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
207 Definition getlev {Γ}(lt:LeveledHaskType Γ ★) := match lt with _ @@ l => l end.
209 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
210 match lht with t@@l => t end.
212 Structure Global Γ :=
213 { glob_wv : WeakExprVar
214 ; glob_kinds : list Kind
215 ; glob_tf : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★
217 Coercion glob_tf : Global >-> Funclass.
218 Coercion glob_wv : Global >-> WeakExprVar.
220 (* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
221 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
222 Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
223 match exp as E in RawHaskType _ K return list (RawHaskType _ K) with
225 (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> list (RawHaskType TV κ₂) -> list (RawHaskType _ K1) with
227 match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> list (RawHaskType TV K2) -> list (RawHaskType _ KindStar) with
228 | KindStar => fun x' =>
229 match x' return list (RawHaskType TV KindStar) -> list (RawHaskType _ KindStar) with
230 | TApp κ₁'' κ₂'' w'' x'' =>
231 match κ₂'' as K2'' return RawHaskType TV K2'' -> list (RawHaskType TV KindStar) ->
232 list (RawHaskType _ KindStar) with
235 | TArrow => fun a b => a::b
236 | _ => fun _ _ => nil
238 | _ => fun _ _ => nil
242 | _ => fun _ _ => nil
244 | _ => fun _ _ => nil
245 end) x (take_arg_types y)
249 Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat :=
250 match exp as E in RawHaskType _ K return nat with
252 (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with
254 match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with
255 | KindStar => fun x' =>
256 match x' return nat -> nat with
257 | TApp κ₁'' κ₂'' w'' x'' =>
258 match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with
261 | TArrow => fun a b => S b
271 end) x (count_arg_types y)
275 Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
283 Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ :=
286 match take_arg_types (ht TV ite) with
287 | nil => Prelude_error "impossible"
291 (* From (t1->(t2->(t3-> ... t))), return t *)
292 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
293 Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
294 match exp as E in RawHaskType _ K return RawHaskType _ K with
297 (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> (RawHaskType TV κ₂) -> ??(RawHaskType _ K1) with
299 match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> (RawHaskType TV K2) -> ??(RawHaskType _ KindStar) with
300 | KindStar => fun x' =>
301 match x' return (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
302 | TApp κ₁'' κ₂'' w'' x'' =>
303 match κ₂'' as K2'' return RawHaskType TV K2'' -> (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
306 | TArrow => fun _ b => Some b
307 | _ => fun _ b => None
309 | _ => fun _ b => None
313 | _ => fun _ _ => None
315 | _ => fun _ _ => None
316 end) x (drop_arg_types y)
327 (* yeah, things are kind of messy below this point *)
330 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
332 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
333 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
334 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
335 : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
336 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
337 (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
338 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
340 unfold InstantiatedCoercionEnv.
341 unfold addKindToCoercionEnv.
343 rewrite <- map_preserves_length.
346 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
347 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
348 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
349 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
351 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
352 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
354 unfold addCoercionToCoercionEnv; simpl.
355 unfold InstantiatedCoercionEnv; simpl.
356 apply vec_cons; auto.
359 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
360 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := ilist_tail ite.
361 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
362 Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv := fun TV ite => (cv' TV (weakITE ite)).
363 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂ := fun TV ite => lt TV (weakITE ite).
364 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt.
365 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂ := match lt with t @@ l => weakT t @@ weakL l end.
366 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
367 : InstantiatedCoercionEnv TV CV Γ Δ.
369 unfold InstantiatedCoercionEnv; intros.
370 unfold InstantiatedCoercionEnv in ice.
371 unfold weakCE in ice.
373 rewrite <- map_preserves_length in ice.
376 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
377 unfold HaskCoercionKind in *.
379 apply hck; clear hck.
380 inversion X; subst; auto.
382 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
383 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
384 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
385 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
386 := fun TV ite tv => (f TV (weakITE ite) tv).
389 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
390 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
391 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
392 induction κ; auto. apply weakV; auto. Defined.
393 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
394 induction κ; auto. apply weakT; auto. Defined.
395 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
396 unfold HaskType in *.
397 unfold InstantiatedTypeEnv in *.
399 apply ilist_chop in X.
403 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
404 induction κ; auto. apply weakL; auto. Defined.
405 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
406 := match lt with t @@ l => weakT' t @@ weakL' l end.
407 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
408 induction κ; auto. apply weakCE; auto. Defined.
409 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
414 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
417 Definition weakITE_ {Γ:TypeEnv}{κ}{n}{TV}(ite:InstantiatedTypeEnv TV (list_ins n κ Γ)) : InstantiatedTypeEnv TV Γ.
418 rewrite list_ins_app in ite.
419 set (weakITE' ite) as ite'.
420 set (ilist_chop ite) as a.
421 rewrite <- (list_take_drop _ Γ n).
422 apply ilist_app; auto.
423 inversion ite'; auto.
426 Definition weakV_ {Γ:TypeEnv}{κ}{n}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (list_ins n κ Γ) κv.
427 unfold HaskTyVar; intros.
428 unfold HaskTyVar in cv'.
430 apply weakITE_ in env.
434 Definition weakT_ {Γ}{κ}{n}{κ₂}(lt:HaskType Γ κ₂) : HaskType (list_ins n κ Γ) κ₂.
435 unfold HaskType; intros.
440 Definition weakL_ {Γ}{κ}{n}(lev:HaskLevel Γ) : HaskLevel (list_ins n κ Γ).
441 unfold HaskLevel; intros.
442 unfold HaskLevel in lev.
447 Definition weakLT_ {Γ}{κ}{n}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (list_ins n κ Γ) κ₂ :=
448 match lt with t@@l => weakT_ t @@ weakL_ l end.
449 Definition weakCK_ {Γ}{κ}{n}(hck:HaskCoercionKind Γ) : HaskCoercionKind (list_ins n κ Γ).
450 unfold HaskCoercionKind; intros.
451 unfold HaskCoercionKind in hck.
456 Definition weakCE_ {Γ:TypeEnv}{κ}{n}(Δ:CoercionEnv Γ) : CoercionEnv (list_ins n κ Γ) := map weakCK_ Δ.
457 Definition weakF_ {Γ:TypeEnv}{n}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
458 forall TV (env:@InstantiatedTypeEnv TV (list_ins n κ Γ)), TV κ -> RawHaskType TV κ₂.
461 apply weakITE_ in env.
465 Definition weakCV_ {Γ}{Δ}{κ}{n}(cv':HaskCoVar Γ Δ) : HaskCoVar (list_ins n κ Γ) (weakCE_ Δ).
466 unfold HaskCoVar; intros.
467 unfold HaskCoVar in cv'.
469 apply weakITE_ in env.
471 unfold InstantiatedCoercionEnv.
472 unfold InstantiatedCoercionEnv in cenv.
473 replace (length (@weakCE_ _ κ n Δ)) with (length Δ) in cenv.
476 rewrite <- map_preserves_length.
480 Definition FreshHaskTyVar_ {Γ}(κ:Kind) : forall {n}, HaskTyVar (list_ins n κ Γ) κ.
484 rewrite list_ins_app in env.
485 apply weakITE' in env.
486 inversion env; subst; auto.
491 Fixpoint caseType0 {Γ}(lk:list Kind) :
492 IList _ (HaskType Γ) lk ->
493 HaskType Γ (fold_right KindArrow ★ lk) ->
495 match lk as LK return
496 IList _ (HaskType Γ) LK ->
497 HaskType Γ (fold_right KindArrow ★ LK) ->
500 | nil => fun _ ht => ht
501 | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
504 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
505 caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
507 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
508 Record StrongAltCon {tc:TyCon} :=
510 ; sac_altcon : WeakAltCon
511 ; sac_numExTyVars : nat
512 ; sac_numCoerVars : nat
513 ; sac_numExprVars : nat
514 ; sac_ekinds : vec Kind sac_numExTyVars
515 ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
516 ; sac_gamma := fun Γ => app (vec2list sac_ekinds) Γ
517 ; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars
518 ; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars
519 ; sac_delta := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
521 Coercion sac_tc : StrongAltCon >-> TyCon.
522 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
525 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
527 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
529 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
530 set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
531 unfold tyConKind' in z.
532 rewrite literal_tycons_are_of_ordinary_kind in z.
537 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
540 `{EQD_VV:EqDecidable VV}{Γ}
541 (ξ:VV -> LeveledHaskType Γ ★)
543 (vt:list (VV * HaskType Γ ★))
544 : VV -> LeveledHaskType Γ ★ :=
547 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v'
550 Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
551 not (In v (map (@fst _ _) varstypes)) ->
552 (update_xi ξ lev varstypes) v = ξ v.
558 destruct (eqd_dec v0 v).
573 (***************************************************************************************************)
574 (* Well-Formedness of Types and Coercions *)
575 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
576 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
577 mkTFD : Kind -> TypeFunctionDecl tfc vk.
581 Context {TV:Kind->Type}.
584 (* local notations *)
585 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
586 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
587 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
588 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
589 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
591 (* Figure 8, lower half *)
592 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
593 @InstantiatedTypeEnv TV Γ ->
594 @InstantiatedCoercionEnv TV CV Γ Δ ->
595 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
596 | CoTVar':∀ Γ Δ t e c σ τ,
597 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
598 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
599 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
600 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
601 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
602 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
604 | SComp :∀ Γ Δ t e γ n S σ τ κ,
605 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
606 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
607 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
608 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
609 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
610 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
612 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
613 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
614 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
615 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
616 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
617 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
618 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
619 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
620 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
622 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
623 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
624 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
625 @InstantiatedTypeEnv TV Γ ->
626 InstantiatedCoercionEnv TV CV Γ Δ ->
627 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
628 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
629 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
630 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
631 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
634 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
635 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
636 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
637 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
643 (* Decidable equality on PHOAS types *)
644 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
646 | TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
647 | TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end
648 | TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
649 | TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
650 | TArrow => match t2 with TArrow => true | _ => false end
651 | TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
652 | TCoerc _ t1 t2 t => match t2 with TCoerc _ t1' t2' t' => compareT n t1 t1' && compareT n t2 t2' && compareT n t t' | _ =>false end
653 | TyFunApp tfc kl k lt => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
655 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
657 | TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end
658 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
661 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
662 match lk as LK return IList _ _ LK with
664 | h::t => n::::(count' t (S n))
667 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
668 compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
672 * This is not provable in Coq's logic because the Coq function space
673 * is "too big" - although its only definable inhabitants are Coq
674 * functions, it is not provable in Coq that all function space
675 * inhabitants are definable (i.e. there are no "exotic" inhabitants).
676 * This is actually an important feature of Coq: it lets us reason
677 * about properties of non-computable (non-recursive) functions since
678 * any property proven to hold for the entire function space will hold
679 * even for those functions. However when representing binding
680 * structure using functions we would actually prefer the smaller
681 * function-space of *definable* functions only. These two axioms
683 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
684 if compareHT Γ κ ht1 ht2
687 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
688 if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
692 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
693 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
694 apply Build_EqDecidable.
696 set (compareHT_decides _ _ v1 v2) as z.
697 set (compareHT Γ κ v1 v2) as q.
698 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
703 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
704 apply Build_EqDecidable.
706 set (compareVars _ _ v1 v2) as z.
707 set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
708 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
713 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
714 apply Build_EqDecidable.
716 unfold HaskLevel in *.
717 apply (eqd_dec v1 v2).
724 (* ToString instance for PHOAS types *)
725 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
727 | TVar _ v => "tv" +++ toString v
728 | TCon tc => toString tc
729 | TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~"
730 +++typeToString' false n t2+++")=>"
731 +++typeToString' needparens n t
734 | TApp _ _ TArrow t1 =>
736 then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
737 else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
740 then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
741 else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
744 | TAll k f => let alpha := "tv"+++ toString n
745 in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
746 typeToString' false (S n) (f n)
747 | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
748 | TyFunApp tfc kl k lt => toString tfc+++ "_" +++ toString n+++" ["+++
749 (fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
751 with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
753 | TyFunApp_nil => nil
754 | TyFunApp_cons κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
757 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
758 typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
760 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
761 { toString := typeToString }.
763 Definition TBool {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp BoolTyCon _ _ TyFunApp_nil.
764 Definition TInt {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp IntTyCon _ _ TyFunApp_nil.