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 HaskCoreLiterals.
12 Require Import HaskCoreTypes. (* FIXME *)
13 Require Import HaskCoreVars. (* FIXME *)
14 Require Import HaskWeakTypes.
15 Require Import HaskWeakVars. (* FIXME *)
16 Require Import HaskCoreToWeak. (* FIXME *)
18 Variable CoFunConst : nat -> Type. (* FIXME *)
19 Variable TyFunConst : nat -> Type. (* FIXME *)
21 Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
23 Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
24 Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta".
25 Variable dataConOrigArgTys_:CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_ =>"DataCon.dataConOrigArgTys".
26 Variable getTyConTyVars_ : TyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "TyCon.tyConTyVars".
28 (* FIXME: might be a better idea to panic here than simply drop things that look wrong *)
29 Definition tyConTyVars (tc:TyCon) :=
30 filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)).
32 Definition dataConExTyVars cdc :=
33 filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
34 Opaque dataConExTyVars.
35 Definition dataConCoerKinds cdc :=
36 filter (map (fun x => match x with EqPred t1 t2 =>
38 coreTypeToWeakType t1 >>= fun t1' =>
39 coreTypeToWeakType t2 >>= fun t2' =>
45 end) (dataConEqTheta_ cdc)).
46 Opaque dataConCoerKinds.
47 Definition dataConFieldTypes cdc :=
48 filter (map (fun x => match coreTypeToWeakType x with
51 end) (dataConOrigArgTys_ cdc)).
53 Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc).
54 Coercion tyConNumKinds : TyCon >-> nat.
56 Inductive DataCon : TyCon -> Type :=
57 mkDataCon : forall cdc:CoreDataCon, DataCon (dataConTyCon cdc).
58 Definition dataConToCoreDataCon `(dc:DataCon tc) : CoreDataCon := match dc with mkDataCon cdc => cdc end.
59 Coercion mkDataCon : CoreDataCon >-> DataCon.
60 Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon.
63 Definition compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool.
67 exact (if eqd_dec cdc cdc0 then true else false).
70 Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2).
72 Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc).
74 apply Build_EqDecidable.
76 set (trust_compare_datacons _ v1 v2) as x.
77 set (compare_datacons tc v1 v2) as y.
78 assert (y=compare_datacons tc v1 v2). reflexivity.
79 destruct y; rewrite <- H in x.
84 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
87 (* TV is the PHOAS type which stands for type variables of System FC *)
90 (* Figure 7: ρ, σ, τ, ν *)
91 Inductive RawHaskType : Type :=
92 | TVar : TV -> RawHaskType (* a *)
93 | TCon : TyCon -> RawHaskType (* T *)
94 | TArrow : RawHaskType (* (->) *)
95 | TCoerc : RawHaskType -> RawHaskType -> RawHaskType -> RawHaskType (* (+>) *)
96 | TApp : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *)
97 | TFCApp : forall tc:TyCon, vec RawHaskType tc -> RawHaskType (* S_n *)
98 | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *)
99 | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *).
101 (* the "kind" of a coercion is a pair of types *)
102 Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind.
106 (* the PHOAS type which stands for coercion variables of System FC *)
110 Inductive RawHaskCoer : Prop :=
111 | CoVar : CV -> RawHaskCoer (* g *)
112 | CoType : RawHaskType -> RawHaskCoer (* τ *)
113 | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
114 | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
115 | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
116 | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
117 | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
118 | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
119 | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
120 | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
121 | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
126 Implicit Arguments TCon [ [TV] ].
127 Implicit Arguments TFCApp [ [TV] ].
128 Implicit Arguments RawHaskType [ ].
129 Implicit Arguments RawHaskCoer [ ].
130 Implicit Arguments RawCoercionKind [ ].
132 Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
133 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
137 (* Kind and Coercion Environments *)
139 * In System FC, the environment consists of three components, each of
140 * whose well-formedness depends on all of those prior to it:
142 * 1. (TypeEnv) The list of free type variables and their kinds
143 * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility
144 * 3. (Tree ??CoreVar) The list of free value variables and the type of each one
147 Definition TypeEnv := list Kind.
148 Definition InstantiatedTypeEnv (TV:Type) (Γ:TypeEnv) := vec TV (length Γ).
149 Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
150 Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ).
151 Definition InstantiatedCoercionEnv (TV CV:Type)(Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
154 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
155 Definition HaskTyVar (Γ:TypeEnv) := forall TV (env:@InstantiatedTypeEnv TV Γ), TV.
156 Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
157 Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ).
158 Definition HaskType (Γ:TypeEnv) := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV.
159 Definition HaskCoercion Γ Δ := ∀ TV CV,
160 @InstantiatedTypeEnv TV Γ -> @InstantiatedCoercionEnv TV CV Γ Δ -> RawHaskCoer TV CV.
161 Inductive LeveledHaskType (Γ:TypeEnv) := mkLeveledHaskType : HaskType Γ -> HaskLevel Γ -> LeveledHaskType Γ.
162 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) := fun TV env => vec_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)(cv:HaskTyVar Γ) : HaskType Γ
166 := fun TV env => σ TV env (cv TV env).
167 Definition HaskBrak {Γ}(v:HaskTyVar Γ)(t:HaskType Γ) : HaskType Γ := fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
168 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ := fun TV ite => TCon tc.
169 Definition HaskAppT {Γ}(t1 t2:HaskType Γ) : HaskType Γ := fun TV ite => TApp (t1 TV ite) (t2 TV ite).
170 Definition mkHaskCoercionKind {Γ}(t1 t2:HaskType Γ) : HaskCoercionKind Γ :=
171 fun TV ite => mkRawCoercionKind (t1 TV ite) (t2 TV ite).
172 Definition unMkHaskCoercionKind {Γ}(hck:HaskCoercionKind Γ) : (HaskType Γ * HaskType Γ) :=
173 ((fun TV ite => match (hck TV ite) with mkRawCoercionKind t1 _ => t1 end),
174 (fun TV ite => match (hck TV ite) with mkRawCoercionKind _ t2 => t2 end)).
177 (* PHOAS substitution on types *)
178 Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(v:@HaskType Γ) : @HaskType Γ
180 (fix flattenT (exp: RawHaskType (RawHaskType TV)) : RawHaskType TV :=
183 | TAll k y => TAll k (fun v => flattenT (y (TVar v)))
184 | TApp x y => TApp (flattenT x) (flattenT y)
186 | TCoerc t1 t2 t => TCoerc (flattenT t1) (flattenT t2) (flattenT t)
188 | TCode v e => TCode (flattenT v) (flattenT e)
189 | TFCApp tfc lt => TFCApp tfc
190 ((fix flatten_vec n (expv:vec (RawHaskType (RawHaskType TV)) n) : vec (RawHaskType TV) n :=
191 match expv in vec _ N return vec (RawHaskType TV) N with
193 | x:::y => (flattenT x):::(flatten_vec _ y)
196 (exp (RawHaskType TV) (vec_map (fun tv => TVar tv) env) (v TV env)).
197 Notation "t @@ l" := (@mkLeveledHaskType _ t l) (at level 20).
198 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
199 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
214 (* yeah, things are kind of messy below this point *)
217 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Type}(ite:InstantiatedTypeEnv TV (κ::Γ)) := vec_tail ite.
218 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
219 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
220 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind)
221 : InstantiatedTypeEnv TV (κ::Γ) := tv:::env.
222 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV CV:Type}(env:InstantiatedCoercionEnv TV CV Γ Δ)(tv:TV)(κ:Kind)
223 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
225 unfold InstantiatedCoercionEnv.
226 unfold addKindToCoercionEnv.
228 rewrite <- map_preserves_length.
231 Definition typeEnvContainsType {Γ}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind) : Prop
232 := @vec_In _ _ (tv,κ) (vec_zip env (list2vec Γ)).
233 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV CV:Type}(ite:InstantiatedTypeEnv TV Γ)
234 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
235 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
236 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
238 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
239 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
241 unfold addCoercionToCoercionEnv; simpl.
242 unfold InstantiatedCoercionEnv; simpl.
243 apply vec_cons; auto.
245 Notation "env ∋ tv : κ" := (@typeEnvContainsType _ _ env tv κ).
246 Notation "env '+' tv : κ" := (@addKindToInstantiatedTypeEnv _ _ env tv κ).
248 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
249 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := vec_tail ite.
250 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
251 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
252 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
253 Definition weakV {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (κ::Γ) := fun TV ite => (cv' TV (weakITE ite)).
254 Definition weakV' {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (app κ Γ).
255 induction κ; auto. apply weakV; auto. Defined.
256 Definition weakT {Γ:TypeEnv}{κ:Kind}(lt:HaskType Γ) : HaskType (κ::Γ) := fun TV ite => lt TV (weakITE ite).
257 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt.
258 Definition weakT' {Γ}{κ}(lt:HaskType Γ) : HaskType (app κ Γ).
259 induction κ; auto. apply weakT; auto. Defined.
260 Definition weakT'' {Γ}{κ}(lt:HaskType Γ) : HaskType (app Γ κ).
261 unfold HaskType in *.
262 unfold InstantiatedTypeEnv in *.
268 Definition lamer {a}{b}{c}(lt:HaskType (app (app a b) c)) : HaskType (app a (app b c)).
269 rewrite <- ass_app in lt.
272 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ) :=
273 let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT t1) (weakT t2).
274 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ) :=
275 let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT' t1) (weakT' t2).
276 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
277 match κ as K return list (HaskCoercionKind (app K Γ)) with
279 | _ => map weakCK' hck
281 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
282 induction κ; auto. apply weakL; auto. Defined.
283 Definition weakLT {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (κ::Γ) := match lt with t @@ l => weakT t @@ weakL l end.
284 Definition weakLT' {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (app κ Γ)
285 := match lt with t @@ l => weakT' t @@ weakL' l end.
286 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
287 induction κ; auto. apply weakCE; auto. Defined.
288 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
289 : InstantiatedCoercionEnv TV CV Γ Δ.
291 unfold InstantiatedCoercionEnv; intros.
292 unfold InstantiatedCoercionEnv in ice.
293 unfold weakCE in ice.
295 rewrite <- map_preserves_length in ice.
298 Definition weakICE' {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (app κ Γ) (weakCE' Δ))
299 : InstantiatedCoercionEnv TV CV Γ Δ.
300 induction κ; auto. apply IHκ. eapply weakICE. apply ice. Defined.
301 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
302 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
303 Definition weakC {Γ}{κ}{Δ}(c:HaskCoercion Γ Δ) : HaskCoercion (κ::Γ) (weakCE Δ) :=
304 fun TV CV ite ice => c TV CV (weakITE ite) (weakICE ice).
305 Definition weakF {Γ:TypeEnv}{κ:Kind}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) :
306 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV -> RawHaskType TV
307 := fun TV ite tv => (f TV (weakITE ite) tv).
309 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
310 Record StrongAltCon {tc:TyCon} :=
311 { sac_altcon : AltCon
312 ; sac_numExTyVars : nat
313 ; sac_numCoerVars : nat
314 ; sac_numExprVars : nat
315 ; sac_akinds : vec Kind tc
316 ; sac_ekinds : vec Kind sac_numExTyVars
317 ; sac_kinds := app (vec2list sac_akinds) (vec2list sac_ekinds)
318 ; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ
319 ; sac_coercions : forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
320 ; sac_types : forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskType (sac_Γ Γ)) sac_numExprVars
321 ; sac_Δ := fun Γ (atypes:vec (HaskType Γ) tc) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
323 Coercion sac_altcon : StrongAltCon >-> AltCon.
325 Definition caseType {Γ:TypeEnv}(tc:TyCon)(atypes:vec (HaskType Γ) tc) :=
326 fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc).
329 (***************************************************************************************************)
330 (* Well-Formedness of Types and Coercions *)
331 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
332 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
333 mkTFD : Kind -> TypeFunctionDecl tfc vk.
336 (* Figure 8, upper half *)
337 Inductive WellKinded_RawHaskType (TV:Type)
338 : forall Γ:TypeEnv, InstantiatedTypeEnv TV Γ -> RawHaskType TV -> Kind -> Prop :=
339 | WFTyVar : forall Γ env κ d,
341 WellKinded_RawHaskType TV Γ env (TVar d) κ
342 | WFTyApp : forall Γ env κ₁ κ₂ σ₁ σ₂,
343 WellKinded_RawHaskType TV Γ env σ₁ (κ₁ ⇛ κ₂) ->
344 WellKinded_RawHaskType TV Γ env σ₂ κ₂ ->
345 WellKinded_RawHaskType TV Γ env (TApp σ₁ σ₂) κ₂
346 | WFTyAll : forall Γ (env:InstantiatedTypeEnv TV Γ) κ σ ,
347 (∀ a, WellKinded_RawHaskType TV _ (@addKindToInstantiatedTypeEnv _ TV env a κ) (σ a) ★ ) ->
348 WellKinded_RawHaskType TV _ env (TAll κ σ) ★
349 | TySCon : forall Γ env tfc lt vk ι ,
350 @TypeFunctionDecl tfc vk ->
351 ListWellKinded_RawHaskType TV Γ _ env lt vk ->
352 WellKinded_RawHaskType TV Γ env (TFCApp tfc lt) ι
353 with ListWellKinded_RawHaskType (TV:Type)
354 : forall (Γ:TypeEnv) n, InstantiatedTypeEnv TV Γ -> vec (RawHaskType TV) n -> vec Kind n -> Prop :=
355 | ListWFRawHaskTypenil : forall Γ env,
356 ListWellKinded_RawHaskType TV Γ 0 env vec_nil vec_nil
357 | ListWFRawHaskTypecons : forall Γ env n t k lt lk,
358 WellKinded_RawHaskType TV Γ env t k ->
359 ListWellKinded_RawHaskType TV Γ n env lt lk ->
360 ListWellKinded_RawHaskType TV Γ (S n) env (t:::lt) (k:::lk).
362 Variable kindOfTyCon : forall (tc:TyCon), Kind.
363 Extract Inlined Constant kindOfTyCon => "(\x -> Prelude.error ""not implemented yet"")".
365 Fixpoint kindOfRawHaskType (rht:RawHaskType Kind) : ???Kind :=
368 | TCon tc => OK (kindOfTyCon tc)
369 | TCoerc t1 t2 t => OK (★ ⇛ ★ )
370 | TArrow => OK (★ ⇛ ★ ⇛ ★ )
371 | TApp ht1 ht2 => kindOfRawHaskType ht1 >>= fun k1 =>
372 kindOfRawHaskType ht2 >>= fun k2 =>
374 | k1' ⇛ k2' => if eqd_dec k1' k1 then OK k2' else Error "kind mismatch"
375 | _ => Error "attempt to apply a non-functional kind"
377 | TFCApp tc rht' => Error "calculating kind of TFCApp is not yet implemented"
378 | TAll k t' => kindOfRawHaskType (t' k) >>= fun k' => OK (k ⇛ k')
379 | TCode t1 t2 => OK ★
382 Definition kindITE (Γ:TypeEnv) : InstantiatedTypeEnv Kind Γ :=
385 Definition kindOfType {Γ}(ht:HaskType Γ) : ???Kind :=
386 kindOfRawHaskType (ht Kind (kindITE Γ)).
388 Definition WellKindedHaskType Γ (ht:HaskType Γ) κ :=
389 forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ.
390 Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ).
392 (* "decl", production for "axiom" *)
393 Structure AxiomDecl (n:nat)(ccon:CoFunConst n)(vk:vec Kind n){TV:Type} : Type :=
394 { axd_τ : vec TV n -> RawHaskType TV
395 ; axd_σ : vec TV n -> RawHaskType TV
402 (* local notations *)
403 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
404 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
405 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
406 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
407 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
409 (* Figure 8, lower half *)
410 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
411 @InstantiatedTypeEnv TV Γ ->
412 @InstantiatedCoercionEnv TV CV Γ Δ ->
413 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
414 | CoTVar':∀ Γ Δ t e c σ τ,
415 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
416 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
417 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
418 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
419 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
420 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
422 | SComp :∀ Γ Δ t e γ n S σ τ κ,
423 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TFCApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TFCApp S σ∼TFCApp S τ : Δ : Γ : t
424 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
425 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
426 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
427 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
428 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
430 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
431 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
432 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
433 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
434 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
435 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
436 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
437 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
438 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
440 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
441 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
442 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
443 @InstantiatedTypeEnv TV Γ ->
444 InstantiatedCoercionEnv TV CV Γ Δ ->
445 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
446 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
447 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
448 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
449 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
452 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
453 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
454 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
455 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
457 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)).
459 Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18).
462 `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ :=
465 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'