1 (*********************************************************************************************************************************)
2 (* HaskStrongTypes: representation of types and coercions for HaskStrong *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.String.
9 Require Import Coq.Lists.List.
10 Require Import HaskGeneral.
11 Require Import HaskLiterals.
13 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
16 (* TV is the PHOAS type which stands for type variables of System FC *)
19 (* Figure 7: ρ, σ, τ, ν *)
20 Inductive RawHaskType : Type :=
21 | TVar : TV -> RawHaskType (* a *)
22 | TCon : ∀n, TyCon n -> RawHaskType (* T *)
23 | TCoerc : Kind -> RawHaskType (* (+>) *)
24 | TApp : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *)
25 | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *)
26 | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *)
27 | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *).
29 (* the "kind" of a coercion is a pair of types *)
30 Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind.
34 (* the PHOAS type which stands for coercion variables of System FC *)
38 Inductive RawHaskCoer : Prop :=
39 | CoVar : CV -> RawHaskCoer (* g *)
40 | CoType : RawHaskType -> RawHaskCoer (* τ *)
41 | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
42 | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
43 | CoCFApp : ∀n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
44 | CoTFApp : ∀n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
45 | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
46 | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
47 | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
48 | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
49 | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
54 Implicit Arguments TCon [ [TV] [n]].
55 Implicit Arguments TFCApp [ [TV] [n]].
56 Implicit Arguments RawHaskType [ ].
57 Implicit Arguments RawHaskCoer [ ].
58 Implicit Arguments RawCoercionKind [ ].
60 Notation "t1 ---> t2" := (fun TV env => (@TApp _ (@TApp _ (@TCon TV _ ArrowTyCon) (t1 TV env)) (t2 TV env))).
61 Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" :=
62 (fun TV env => @TApp _ (@TApp _ (@TCon _ _ ArrowTyCon) (@TApp _ (@TApp _ (@TCoerc _ κ) (φ₁ TV env)) (φ₂ TV env))) (φ₃ TV env)).
66 (* Kind and Coercion Environments *)
68 * In System FC, the environment consists of three components, each of
69 * whose well-formedness depends on all of those prior to it:
71 * 1. (TypeEnv) The list of free type variables and their kinds
72 * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility
73 * 3. (Tree ??CoreVar) The list of free value variables and the type of each one
76 Definition TypeEnv := list Kind.
77 Definition InstantiatedTypeEnv (TV:Type) (Γ:TypeEnv) := vec TV (length Γ).
78 Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
79 Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ).
80 Definition InstantiatedCoercionEnv (TV CV:Type)(Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
83 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
84 Definition HaskTyVar (Γ:TypeEnv) := forall TV (env:@InstantiatedTypeEnv TV Γ), TV.
85 Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
86 Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ).
87 Definition HaskType (Γ:TypeEnv) := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV.
88 Definition HaskCoercion Γ Δ := ∀ TV CV,
89 @InstantiatedTypeEnv TV Γ -> @InstantiatedCoercionEnv TV CV Γ Δ -> RawHaskCoer TV CV.
90 Inductive LeveledHaskType (Γ:TypeEnv) := mkLeveledHaskType : HaskType Γ -> HaskLevel Γ -> LeveledHaskType Γ.
91 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) := fun TV env => vec_head env.
92 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) : HaskType Γ
93 := fun TV env => TAll κ (σ TV env).
94 Definition HaskTApp {Γ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(cv:HaskTyVar Γ) : HaskType Γ
95 := fun TV env => σ TV env (cv TV env).
96 Definition HaskBrak {Γ}(v:HaskTyVar Γ)(t:HaskType Γ) : HaskType Γ := fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
97 Definition HaskTCon {Γ}{n}(tc:TyCon n) : HaskType Γ := fun TV ite => TCon tc.
98 Definition HaskAppT {Γ}(t1 t2:HaskType Γ) : HaskType Γ := fun TV ite => TApp (t1 TV ite) (t2 TV ite).
99 Definition mkHaskCoercionKind {Γ}(t1 t2:HaskType Γ) : HaskCoercionKind Γ :=
100 fun TV ite => mkRawCoercionKind (t1 TV ite) (t2 TV ite).
103 (* PHOAS substitution on types *)
104 Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(v:@HaskType Γ) : @HaskType Γ
106 (fix flattenT (exp: RawHaskType (RawHaskType TV)) : RawHaskType TV :=
109 | TAll k y => TAll k (fun v => flattenT (y (TVar v)))
110 | TApp x y => TApp (flattenT x) (flattenT y)
111 | TCon n tc => TCon tc
112 | TCoerc k => TCoerc k
113 | TCode v e => TCode (flattenT v) (flattenT e)
114 | TFCApp n tfc lt => TFCApp tfc
115 ((fix flatten_vec n (expv:vec (RawHaskType (RawHaskType TV)) n) : vec (RawHaskType TV) n :=
116 match expv in vec _ N return vec (RawHaskType TV) N with
118 | x:::y => (flattenT x):::(flatten_vec _ y)
121 (exp (RawHaskType TV) (vec_map (fun tv => TVar tv) env) (v TV env)).
122 Notation "t @@ l" := (@mkLeveledHaskType _ t l) (at level 20).
123 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
124 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
129 (* A "tag" is something that distinguishes one case branch from another; it's a lot like Core's AltCon *)
130 Inductive Tag {n:nat}(tc:TyCon n) : Type :=
131 | TagDefault : Tag tc
132 | TagLiteral : forall lit:HaskLiteral , Tag tc (* FIXME: solution is a new StrongLiteral indexed by a tycon *)
133 | TagDataCon : forall m q z, DataCon tc m q z -> Tag tc.
135 (* the number of value variables bound in branches with the given tag *)
136 Definition tagNumValVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
139 | TagLiteral lit => 0
140 | TagDataCon m q z dc => z
143 (* the number of existential type variables bound in branches with the given tag *)
144 Definition tagNumExVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
147 | TagLiteral lit => 0
148 | TagDataCon m q z dc => m
151 (* the number of coercion variables bound in branches with the given tag *)
152 Definition tagNumCoVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
155 | TagLiteral lit => 0
156 | TagDataCon m q z dc => q
159 Definition caseType {Γ:TypeEnv}{n}(tc:TyCon n)(atypes:vec (HaskType Γ) n) :=
160 fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc).
162 Record StrongAltCon {n}{tc:TyCon n}{alt:Tag tc} :=
163 { cb_akinds : vec Kind n
164 ; cb_ekinds : vec Kind (tagNumExVars alt)
165 ; cb_kinds := app (vec2list cb_akinds) (vec2list cb_ekinds)
166 ; cb_coercions : vec (HaskType cb_kinds * HaskType cb_kinds) (tagNumCoVars alt)
167 ; cb_types : vec (HaskType cb_kinds) (tagNumValVars alt)
169 Implicit Arguments StrongAltCon [[n][tc]].
180 (* FIXME: it's a mess below this point *)
183 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Type}(ite:InstantiatedTypeEnv TV (κ::Γ)) := vec_tail ite.
184 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
185 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
186 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind)
187 : InstantiatedTypeEnv TV (κ::Γ) := tv:::env.
188 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV CV:Type}(env:InstantiatedCoercionEnv TV CV Γ Δ)(tv:TV)(κ:Kind)
189 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
191 unfold InstantiatedCoercionEnv.
192 unfold addKindToCoercionEnv.
194 rewrite <- map_preserves_length.
197 Definition typeEnvContainsType {Γ}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind) : Prop
198 := @vec_In _ _ (tv,κ) (vec_zip env (list2vec Γ)).
199 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV CV:Type}(ite:InstantiatedTypeEnv TV Γ)
200 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
201 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
202 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
204 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
205 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
207 unfold addCoercionToCoercionEnv; simpl.
208 unfold InstantiatedCoercionEnv; simpl.
209 apply vec_cons; auto.
211 Notation "env ∋ tv : κ" := (@typeEnvContainsType _ _ env tv κ).
212 Notation "env '+' tv : κ" := (@addKindToInstantiatedTypeEnv _ _ env tv κ).
214 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
215 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := vec_tail ite.
216 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
217 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
218 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
219 Definition weakV {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (κ::Γ) := fun TV ite => (cv' TV (weakITE ite)).
220 Definition weakV' {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (app κ Γ).
221 induction κ; auto. apply weakV; auto. Defined.
222 Definition weakT {Γ:TypeEnv}{κ:Kind}(lt:HaskType Γ) : HaskType (κ::Γ) := fun TV ite => lt TV (weakITE ite).
223 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt.
224 Definition weakT' {Γ}{κ}(lt:HaskType Γ) : HaskType (app κ Γ).
225 induction κ; auto. apply weakT; auto. Defined.
226 Definition weakT'' {Γ}{κ}(lt:HaskType Γ) : HaskType (app Γ κ).
227 unfold HaskType in *.
228 unfold InstantiatedTypeEnv in *.
234 Definition lamer {a}{b}{c}(lt:HaskType (app (app a b) c)) : HaskType (app a (app b c)).
235 rewrite <- ass_app in lt.
238 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
239 induction κ; auto. apply weakL; auto. Defined.
240 Definition weakLT {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (κ::Γ) := match lt with t @@ l => weakT t @@ weakL l end.
241 Definition weakLT' {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (app κ Γ)
242 := match lt with t @@ l => weakT' t @@ weakL' l end.
243 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
244 induction κ; auto. apply weakCE; auto. Defined.
245 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
246 : InstantiatedCoercionEnv TV CV Γ Δ.
248 unfold InstantiatedCoercionEnv; intros.
249 unfold InstantiatedCoercionEnv in ice.
250 unfold weakCE in ice.
252 rewrite <- map_preserves_length in ice.
255 Definition weakICE' {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (app κ Γ) (weakCE' Δ))
256 : InstantiatedCoercionEnv TV CV Γ Δ.
257 induction κ; auto. apply IHκ. eapply weakICE. apply ice. Defined.
258 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
259 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
260 Definition weakC {Γ}{κ}{Δ}(c:HaskCoercion Γ Δ) : HaskCoercion (κ::Γ) (weakCE Δ) :=
261 fun TV CV ite ice => c TV CV (weakITE ite) (weakICE ice).
262 Definition weakF {Γ:TypeEnv}{κ:Kind}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) :
263 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV -> RawHaskType TV
264 := fun TV ite tv => (f TV (weakITE ite) tv).
266 (***************************************************************************************************)
267 (* Well-Formedness of Types and Coercions *)
268 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
269 Inductive TypeFunctionDecl (n:nat)(tfc:TyFunConst n)(vk:vec Kind n) : Type :=
270 mkTFD : Kind -> TypeFunctionDecl n tfc vk.
273 (* Figure 8, upper half *)
274 Inductive WellKinded_RawHaskType (TV:Type)
275 : forall Γ:TypeEnv, InstantiatedTypeEnv TV Γ -> RawHaskType TV -> Kind -> Prop :=
276 | WFTyVar : forall Γ env κ d,
278 WellKinded_RawHaskType TV Γ env (TVar d) κ
279 | WFTyApp : forall Γ env κ₁ κ₂ σ₁ σ₂,
280 WellKinded_RawHaskType TV Γ env σ₁ (κ₁ ⇛ κ₂) ->
281 WellKinded_RawHaskType TV Γ env σ₂ κ₂ ->
282 WellKinded_RawHaskType TV Γ env (TApp σ₁ σ₂) κ₂
283 | WFTyAll : forall Γ (env:InstantiatedTypeEnv TV Γ) κ σ ,
284 (∀ a, WellKinded_RawHaskType TV _ (@addKindToInstantiatedTypeEnv _ TV env a κ) (σ a) ★ ) ->
285 WellKinded_RawHaskType TV _ env (TAll κ σ) ★
286 | TySCon : forall Γ env n tfc lt vk ι ,
287 @TypeFunctionDecl n tfc vk ->
288 ListWellKinded_RawHaskType TV Γ _ env lt vk ->
289 WellKinded_RawHaskType TV Γ env (TFCApp tfc lt) ι
290 with ListWellKinded_RawHaskType (TV:Type)
291 : forall (Γ:TypeEnv) n, InstantiatedTypeEnv TV Γ -> vec (RawHaskType TV) n -> vec Kind n -> Prop :=
292 | ListWFRawHaskTypenil : forall Γ env,
293 ListWellKinded_RawHaskType TV Γ 0 env vec_nil vec_nil
294 | ListWFRawHaskTypecons : forall Γ env n t k lt lk,
295 WellKinded_RawHaskType TV Γ env t k ->
296 ListWellKinded_RawHaskType TV Γ n env lt lk ->
297 ListWellKinded_RawHaskType TV Γ (S n) env (t:::lt) (k:::lk).
300 Fixpoint kindOfRawHaskType {TV}(rht:RawHaskType Kind) : Kind :=
303 | TCon n tc => ̱★ (* FIXME: use the StrongAltCon *)
304 | TCoerc k => k ⇛ (k ⇛ (★ ⇛ ★ ))
305 | TApp ht1 ht2 : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *)
306 | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *)
307 | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *)
308 | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *).
310 Definition WellKindedHaskType Γ (ht:HaskType Γ) κ :=
311 forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ.
312 Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ).
316 (* "decl", production for "axiom" *)
317 Structure AxiomDecl (n:nat)(ccon:CoFunConst n)(vk:vec Kind n){TV:Type} : Type :=
318 { axd_τ : vec TV n -> RawHaskType TV
319 ; axd_σ : vec TV n -> RawHaskType TV
329 (* local notations *)
330 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
331 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
332 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
333 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
334 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
336 (* Figure 8, lower half *)
337 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
338 @InstantiatedTypeEnv TV Γ ->
339 @InstantiatedCoercionEnv TV CV Γ Δ ->
340 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=.
342 | CoTVar':∀ Γ Δ t e c σ τ,
343 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
344 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
345 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
346 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
347 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
348 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
349 | SComp :∀ Γ Δ t e γ n S σ τ κ,
350 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TFCApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TFCApp S σ∼TFCApp S τ : Δ : Γ : t
351 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
352 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
353 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
354 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
355 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
357 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
358 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
359 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
361 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
362 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
363 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
364 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
365 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
367 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
369 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
370 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
371 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
372 @InstantiatedTypeEnv TV Γ ->
373 InstantiatedCoercionEnv TV CV Γ Δ ->
374 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
375 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
376 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
377 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
378 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
382 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
383 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
384 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
385 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
387 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)).
388 Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18).
392 `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ :=
395 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
409 Definition literalType (lit:Literal) : ∀ Γ, HaskType Γ := fun Γ TV ite => (TCon (literalTyCon lit)).
410 Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end.
411 Definition getlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskLevel Γ := match lht with t @@ l => l end.
412 (* the type of the scrutinee in a case branch *)
413 Require Import Coq.Arith.EqNat.
414 Definition bump (n:nat) : {z:nat & lt z n} -> {z:nat & lt z (S n)}.
419 Definition vecOfNats (n:nat) : vec {z:nat & lt z n} n.
424 apply (vec_map (bump _)); auto.
426 Definition var_eq_dec {Γ:TypeEnv}(hv1 hv2:HaskTyVar Γ) : sumbool (eq hv1 hv2) (not (eq hv1 hv2)).
427 set (hv1 _ (vecOfNats _)) as hv1'.
428 set (hv2 _ (vecOfNats _)) as hv2'.
429 destruct hv1' as [hv1_n hv1_pf].
430 destruct hv2' as [hv2_n hv2_pf].
433 set (eq_nat_decide hv1_n hv2_n) as dec.
436 right. intro. apply n. assert (hv1_n=hv2_n). admit. rewrite H0. apply eq_nat_refl.
438 (* equality on levels is decidable *)
439 Definition lev_eq_dec {Γ:TypeEnv}(l1 l2:HaskLevel Γ) : sumbool (eq l1 l2) (not (eq l1 l2))
440 := @list_eq_dec (HaskTyVar Γ) (@var_eq_dec Γ) l1 l2.
447 (* just like GHC's AltCon, but using PHOAS types and coercions *)
448 Record StrongAltConInContext {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} :=
450 ; cbi_cb : StrongAltCon cbi_tag
451 ; cbi_Γ : TypeEnv := app (vec2list (cb_ekinds cbi_cb)) Γ
452 ; cbi_Δ : CoercionEnv cbi_Γ
453 ; cbi_types : vec (LeveledHaskType (app (vec2list (cb_ekinds cbi_cb)) Γ)) (tagNumValVars cbi_tag)
455 Implicit Arguments StrongAltConInContext [[n][Γ]].