src/HaskStrongTypes.v

   1 (*********************************************************************************************************************************)
   2 (* HaskStrongTypes: representation of types and coercions for HaskStrong                                                         *)
   3 (*********************************************************************************************************************************)
   4
   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.
  12
  13 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
  14 Section Raw.
  15
  16   (* TV is the PHOAS type which stands for type variables of System FC *)
  17   Context {TV:Type}.
  18
  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 λ^α *).
  28
  29   (* the "kind" of a coercion is a pair of types *)
  30   Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind.
  31
  32   Section CV.
  33
  34     (* the PHOAS type which stands for coercion variables of System FC *)
  35     Context {CV:Type}.
  36
  37     (* Figure 7: γ, δ *)
  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  *).
  50
  51   End CV.
  52 End Raw.
  53
  54 Implicit Arguments TCon   [ [TV] [n]].
  55 Implicit Arguments TFCApp [ [TV] [n]].
  56 Implicit Arguments RawHaskType  [ ].
  57 Implicit Arguments RawHaskCoer  [ ].
  58 Implicit Arguments RawCoercionKind [ ].
  59
  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)).
  63
  64
  65
  66 (* Kind and Coercion Environments *)
  67 (*
  68  *  In System FC, the environment consists of three components, each of
  69  *  whose well-formedness depends on all of those prior to it:
  70  *
  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
  74  *)
  75
  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 Δ).
  81
  82
  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).
 101
 102
 103 (* PHOAS substitution on types *)
 104 Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(v:@HaskType Γ) : @HaskType Γ
 105   := fun TV env =>
 106     (fix flattenT (exp: RawHaskType (RawHaskType TV)) : RawHaskType TV :=
 107      match exp with
 108     | TVar       x        => x
 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
 117           | vec_nil => vec_nil
 118           | x:::y   => (flattenT x):::(flatten_vec _ y)
 119         end) n lt)
 120     end)
 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).
 125
 126
 127
 128
 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.
 134
 135 (* the number of value variables bound in branches with the given tag *)
 136 Definition tagNumValVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
 137   match tag with
 138     | TagDefault          => 0
 139     | TagLiteral  lit     => 0
 140     | TagDataCon m q z dc => z
 141   end.
 142
 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 :=
 145   match tag with
 146     | TagDefault          => 0
 147     | TagLiteral  lit     => 0
 148     | TagDataCon m q z dc => m
 149   end.
 150
 151 (* the number of coercion variables bound in branches with the given tag *)
 152 Definition tagNumCoVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
 153   match tag with
 154     | TagDefault          => 0
 155     | TagLiteral  lit     => 0
 156     | TagDataCon m q z dc => q
 157   end.
 158
 159 Definition caseType {Γ:TypeEnv}{n}(tc:TyCon n)(atypes:vec (HaskType Γ) n) :=
 160   fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc).
 161
 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)
 168 }.
 169 Implicit Arguments StrongAltCon [[n][tc]].
 170
 171
 172
 173
 174
 175
 176
 177
 178
 179
 180 (* FIXME: it's a mess below this point *)
 181
 182
 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 Γ Δ κ).
 190     simpl.
 191     unfold InstantiatedCoercionEnv.
 192     unfold addKindToCoercionEnv.
 193     simpl.
 194     rewrite <- map_preserves_length.
 195     apply env.
 196     Defined.
 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 Γ :=
 203   κ::Δ.
 204 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
 205   : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
 206   simpl.
 207   unfold addCoercionToCoercionEnv; simpl.
 208   unfold InstantiatedCoercionEnv; simpl.
 209   apply vec_cons; auto.
 210   Defined.
 211 Notation "env  ∋  tv : κ"        := (@typeEnvContainsType  _ _ env tv κ).
 212 Notation "env '+' tv : κ"        := (@addKindToInstantiatedTypeEnv  _ _ env tv κ).
 213
 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 *.
 229 intros.
 230 apply vec_chop in X.
 231 apply lt.
 232 apply X.
 233 Defined.
 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.
 236 exact lt.
 237 Defined.
 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 Γ Δ.
 247   intros.
 248   unfold InstantiatedCoercionEnv; intros.
 249   unfold InstantiatedCoercionEnv in ice.
 250   unfold weakCE in ice.
 251   simpl in ice.
 252   rewrite <- map_preserves_length in ice.
 253   apply ice.
 254   Defined.
 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).
 265
 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.
 271
 272
 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,
 277                 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).
 298
 299 (*
 300 Fixpoint kindOfRawHaskType {TV}(rht:RawHaskType Kind) : Kind :=
 301 match rht with
 302   | TVar   k    => k
 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 λ^α *).
 309 *)
 310 Definition WellKindedHaskType Γ (ht:HaskType Γ) κ :=
 311   forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ.
 312   Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ).
 313
 314
 315
 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
 320 }.
 321
 322
 323
 324
 325 Section WFCo.
 326   Context {TV:Type}.
 327   Context {CV:Type}.
 328
 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).
 335
 336   (* Figure 8, lower half *)
 337   Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
 338     @InstantiatedTypeEnv TV Γ ->
 339     @InstantiatedCoercionEnv TV CV Γ Δ ->
 340     @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=.
 341 (*
 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
 356
 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
 360
 361   | Comp   :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
 362             (t ⊢ᴛy TApp σ₁ σ₂:κ)->
 363             (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
 364             (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
 365             e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
 366
 367   | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
 368           t ⊢ᴛy v TV t : κ  ->
 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)).
 379 *)
 380 End WFCo.
 381
 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).
 386
 387   Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)).
 388   Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18).
 389
 390
 391 Fixpoint update_ξ
 392   `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ :=
 393   match vt with
 394     | nil => ξ
 395     | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
 396   end.
 397
 398
 399
 400
 401
 402
 403
 404
 405
 406
 407
 408 (*
 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)}.
 415   intros.
 416   destruct H.
 417   exists x; omega.
 418   Defined.
 419 Definition vecOfNats (n:nat) : vec {z:nat & lt z n} n.
 420   induction n.
 421   apply vec_nil.
 422   apply vec_cons.
 423     exists n; omega.
 424     apply (vec_map (bump _)); auto.
 425     Defined.
 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].
 431   clear hv1_pf.
 432   clear hv2_pf.
 433   set (eq_nat_decide hv1_n hv2_n) as dec.
 434   destruct dec.
 435     left.  admit.
 436     right. intro. apply n. assert (hv1_n=hv2_n). admit. rewrite H0. apply eq_nat_refl.
 437   Defined.
 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.
 441 *)
 442
 443
 444
 445
 446
 447 (* just like GHC's AltCon, but using PHOAS types and coercions *)
 448 Record StrongAltConInContext {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} :=
 449 { cbi_tag       :  Tag tc
 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)
 454 }.
 455 Implicit Arguments StrongAltConInContext [[n][Γ]].
 456