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 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 *)
  17
  18 Variable CoFunConst        : nat -> Type.  (* FIXME *)
  19 Variable TyFunConst        : nat -> Type.  (* FIXME *)
  20
  21 Variable dataConTyCon      : CoreDataCon -> TyCon.     Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
  22
  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".
  27
  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)).
  31   Opaque tyConTyVars.
  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 =>
  37                           match (
  38                             coreTypeToWeakType t1 >>= fun t1' =>
  39                               coreTypeToWeakType t2 >>= fun t2' =>
  40                                 OK (t1',t2'))
  41                           with OK z => Some z
  42                             | _ => None
  43                           end
  44                           | _ => None
  45                         end) (dataConEqTheta_ cdc)).
  46   Opaque dataConCoerKinds.
  47 Definition dataConFieldTypes cdc :=
  48   filter (map (fun x => match coreTypeToWeakType x with
  49                           | OK z => Some z
  50                           | _ => None
  51                         end) (dataConOrigArgTys_ cdc)).
  52
  53 Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc).
  54   Coercion tyConNumKinds : TyCon >-> nat.
  55
  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.
  61   (*Opaque DataCon.*)
  62
  63 Definition compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool.
  64   intros.
  65   destruct dc1.
  66   destruct dc2.
  67   exact (if eqd_dec cdc cdc0 then true else false).
  68   Defined.
  69
  70 Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2).
  71
  72 Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc).
  73   intros.
  74   apply Build_EqDecidable.
  75   intros.
  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.
  80   left; auto.
  81   right; auto.
  82   Defined.
  83
  84 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
  85 Section Raw.
  86
  87   (* TV is the PHOAS type which stands for type variables of System FC *)
  88   Context {TV:Type}.
  89
  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 λ^α *).
 100
 101   (* the "kind" of a coercion is a pair of types *)
 102   Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind.
 103
 104   Section CV.
 105
 106     (* the PHOAS type which stands for coercion variables of System FC *)
 107     Context {CV:Type}.
 108
 109     (* Figure 7: γ, δ *)
 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  *).
 122
 123   End CV.
 124 End Raw.
 125
 126 Implicit Arguments TCon   [ [TV] ].
 127 Implicit Arguments TFCApp [ [TV] ].
 128 Implicit Arguments RawHaskType  [ ].
 129 Implicit Arguments RawHaskCoer  [ ].
 130 Implicit Arguments RawCoercionKind [ ].
 131
 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)).
 134
 135
 136
 137 (* Kind and Coercion Environments *)
 138 (*
 139  *  In System FC, the environment consists of three components, each of
 140  *  whose well-formedness depends on all of those prior to it:
 141  *
 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
 145  *)
 146
 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 Δ).
 152
 153
 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)).
 175
 176
 177 (* PHOAS substitution on types *)
 178 Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(v:@HaskType Γ) : @HaskType Γ
 179   := fun TV env =>
 180     (fix flattenT (exp: RawHaskType (RawHaskType TV)) : RawHaskType TV :=
 181      match exp with
 182     | TVar       x        => x
 183     | TAll       k y      => TAll      k (fun v => flattenT (y (TVar v)))
 184     | TApp       x y      => TApp      (flattenT x) (flattenT y)
 185     | TCon       tc       => TCon      tc
 186     | TCoerc t1 t2   t    => TCoerc    (flattenT t1) (flattenT t2)   (flattenT t)
 187     | TArrow              => TArrow
 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
 192           | vec_nil => vec_nil
 193           | x:::y   => (flattenT x):::(flatten_vec _ y)
 194         end) _ lt)
 195     end)
 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).
 200
 201
 202
 203
 204
 205
 206
 207
 208
 209
 210
 211
 212
 213
 214 (* yeah, things are kind of messy below this point *)
 215
 216
 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 Γ Δ κ).
 224     simpl.
 225     unfold InstantiatedCoercionEnv.
 226     unfold addKindToCoercionEnv.
 227     simpl.
 228     rewrite <- map_preserves_length.
 229     apply env.
 230     Defined.
 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 Γ :=
 237   κ::Δ.
 238 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
 239   : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
 240   simpl.
 241   unfold addCoercionToCoercionEnv; simpl.
 242   unfold InstantiatedCoercionEnv; simpl.
 243   apply vec_cons; auto.
 244   Defined.
 245 Notation "env  ∋  tv : κ"        := (@typeEnvContainsType  _ _ env tv κ).
 246 Notation "env '+' tv : κ"        := (@addKindToInstantiatedTypeEnv  _ _ env tv κ).
 247
 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 *.
 263 intros.
 264 apply vec_chop in X.
 265 apply lt.
 266 apply X.
 267 Defined.
 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.
 270 exact lt.
 271 Defined.
 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
 278   | nil => hck
 279   | _   => map weakCK' hck
 280 end.
 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 Γ Δ.
 290   intros.
 291   unfold InstantiatedCoercionEnv; intros.
 292   unfold InstantiatedCoercionEnv in ice.
 293   unfold weakCE in ice.
 294   simpl in ice.
 295   rewrite <- map_preserves_length in ice.
 296   apply ice.
 297   Defined.
 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).
 308
 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)) Δ
 322 }.
 323 Coercion sac_altcon : StrongAltCon >-> AltCon.
 324
 325 Definition caseType {Γ:TypeEnv}(tc:TyCon)(atypes:vec (HaskType Γ) tc) :=
 326   fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc).
 327
 328
 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.
 334
 335
 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,
 340                 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).
 361
 362 Variable kindOfTyCon : forall (tc:TyCon), Kind.
 363   Extract Inlined Constant kindOfTyCon => "(\x -> Prelude.error ""not implemented yet"")".
 364
 365 Fixpoint kindOfRawHaskType (rht:RawHaskType Kind) : ???Kind :=
 366 match rht with
 367   | TVar   k         => OK k
 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 =>
 373                           match k1 with
 374                             | k1' ⇛ k2' => if eqd_dec k1' k1 then OK k2' else Error "kind mismatch"
 375                             | _         =>                                    Error "attempt to apply a non-functional kind"
 376                           end
 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 ★
 380 end.
 381
 382 Definition kindITE (Γ:TypeEnv) : InstantiatedTypeEnv Kind Γ :=
 383   list2vec Γ.
 384
 385 Definition kindOfType {Γ}(ht:HaskType Γ) : ???Kind :=
 386   kindOfRawHaskType (ht Kind (kindITE Γ)).
 387
 388 Definition WellKindedHaskType Γ (ht:HaskType Γ) κ :=
 389   forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ.
 390   Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ).
 391
 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
 396 }.
 397
 398 Section WFCo.
 399   Context {TV:Type}.
 400   Context {CV:Type}.
 401
 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).
 408
 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
 421   (*
 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
 429   *)
 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),
 439           t ⊢ᴛy v TV t : κ  ->
 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)).
 450 End WFCo.
 451
 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).
 456
 457 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)).
 458
 459 Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18).
 460
 461 Fixpoint update_ξ
 462   `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ :=
 463   match vt with
 464     | nil => ξ
 465     | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
 466   end.