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 HaskLiterals.
  12 Require Import HaskTyCons.
  13 Require Import HaskCoreTypes.
  14 Require Import HaskCoreVars.
  15 Require Import HaskWeakTypes.
  16 Require Import HaskWeakVars.
  17 Require Import HaskWeak.
  18 Require Import HaskCoreToWeak.
  19
  20 Variable dataConTyCon      : CoreDataCon -> TyCon.         Extract Inlined Constant dataConTyCon      => "DataCon.dataConTyCon".
  21 Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Constant dataConExVars_    => "DataCon.dataConExTyVars".
  22 Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConEqTheta".
  23 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
  24
  25 Definition dataConExTyVars cdc :=
  26   filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
  27   Opaque dataConExTyVars.
  28 Definition dataConCoerKinds cdc :=
  29   filter (map (fun x => match x with EqPred t1 t2 =>
  30                           match (
  31                             coreTypeToWeakType t1 >>= fun t1' =>
  32                               coreTypeToWeakType t2 >>= fun t2' =>
  33                                 OK (t1',t2'))
  34                           with OK z => Some z
  35                             | _ => None
  36                           end
  37                           | _ => None
  38                         end) (dataConEqTheta_ cdc)).
  39   Opaque dataConCoerKinds.
  40 Definition dataConFieldTypes cdc :=
  41   filter (map (fun x => match coreTypeToWeakType x with
  42                           | OK z => Some z
  43                           | _ => None
  44                         end) (dataConOrigArgTys_ cdc)).
  45
  46 Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc).
  47   Coercion tyConNumKinds : TyCon >-> nat.
  48
  49 Inductive DataCon : TyCon -> Type :=
  50   mkDataCon : forall cdc:CoreDataCon, DataCon (dataConTyCon cdc).
  51   Definition dataConToCoreDataCon `(dc:DataCon tc) : CoreDataCon := match dc with mkDataCon cdc => cdc end.
  52   Coercion mkDataCon : CoreDataCon >-> DataCon.
  53   Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon.
  54   (*Opaque DataCon.*)
  55
  56 Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
  57
  58 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
  59 Section Raw.
  60
  61   (* TV is the PHOAS type which stands for type variables of System FC *)
  62   Context {TV:Kind -> Type}.
  63
  64   (* Figure 7: ρ, σ, τ, ν *)
  65   Inductive RawHaskType : Kind -> Type :=
  66   | TVar           : ∀ κ, TV κ                                              -> RawHaskType κ                     (* a        *)
  67   | TCon           : ∀ tc,                                                     RawHaskType (tyConKind' tc)       (* T        *)
  68   | TArrow         :                                                           RawHaskType (★ ⇛★ ⇛★ )            (* (->)     *)
  69   | TCoerc         : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★   -> RawHaskType ★                     (* (+>)     *)
  70   | TApp           : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁)        -> RawHaskType κ₂  -> RawHaskType κ₁                    (* φ φ      *)
  71   | TAll           : ∀ κ,                          (TV κ -> RawHaskType ★)  -> RawHaskType ★                     (* ∀a:κ.φ   *)
  72   | TCode          : RawHaskType ECKind                  -> RawHaskType ★   -> RawHaskType ★                     (* from λ^α *)
  73   | TyFunApp       : forall (tf:TyFun) kl k, RawHaskTypeList kl             -> RawHaskType k                     (* S_n      *)
  74   with RawHaskTypeList : list Kind -> Type :=
  75   | TyFunApp_nil   : RawHaskTypeList nil
  76   | TyFunApp_cons  : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl).
  77
  78   (* the "kind" of a coercion is a pair of types *)
  79   Inductive RawCoercionKind : Type :=
  80     mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
  81
  82   (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *)
  83   Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := .
  84   (*
  85    *  This has been disabled until we manage to reconcile SystemFC's
  86    *  coercions with what GHC actually implements (they are not the
  87    *  same!)
  88    *
  89   | CoVar          : CV                                           -> RawHaskCoer (* g      *)
  90   | CoType         : RawHaskType                                  -> RawHaskCoer (* τ      *)
  91   | CoApp          : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* γ γ    *)
  92   | CoAppT         : RawHaskCoer -> RawHaskType                   -> RawHaskCoer (* γ@v    *)
  93   | CoCFApp        : ∀ n, CoFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* C   γⁿ *)
  94   | CoTFApp        : ∀ n, TyFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* S_n γⁿ *)
  95   | CoAll          : Kind  -> (TV -> RawHaskCoer)                 -> RawHaskCoer (* ∀a:κ.γ *)
  96   | CoSym          : RawHaskCoer                                  -> RawHaskCoer (* sym    *)
  97   | CoComp         : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* ◯      *)
  98   | CoLeft         : RawHaskCoer                                  -> RawHaskCoer (* left   *)
  99   | CoRight        : RawHaskCoer                                  -> RawHaskCoer (* right  *).
 100   *)
 101 End Raw.
 102
 103 Implicit Arguments TCon   [ [TV] ].
 104 Implicit Arguments TyFunApp [ [TV] ].
 105 Implicit Arguments RawHaskType  [ ].
 106 Implicit Arguments RawHaskCoer  [ ].
 107 Implicit Arguments RawCoercionKind [ ].
 108 Implicit Arguments TVar [ [TV] [κ] ].
 109 Implicit Arguments TCoerc [ [TV] [κ] ].
 110 Implicit Arguments TApp   [ [TV] [κ₁] [κ₂] ].
 111 Implicit Arguments TAll   [ [TV] ].
 112
 113 Notation "t1 ---> t2"        := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
 114 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"     := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
 115
 116 (* Kind and Coercion Environments *)
 117 (*
 118  *  In System FC, the environment consists of three components, each of
 119  *  whose well-formedness depends on all of those prior to it:
 120  *
 121  *    1. (TypeEnv)        The list of free type     variables and their kinds
 122  *    2. (CoercionEnv)    The list of free coercion variables and the pair of types between which it witnesses coercibility
 123  *    3. (Tree ??CoreVar) The list of free value    variables and the type of each one
 124  *)
 125
 126 Definition TypeEnv                                                         := list Kind.
 127 Definition InstantiatedTypeEnv     (TV:Kind->Type)         (Γ:TypeEnv)     := IList _ TV Γ.
 128 Definition HaskCoercionKind                    (Γ:TypeEnv)                 := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
 129 Definition CoercionEnv             (Γ:TypeEnv)                             := list (HaskCoercionKind Γ).
 130 Definition InstantiatedCoercionEnv (TV:Kind->Type) CV       (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
 131
 132 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
 133 Definition HaskTyVar (Γ:TypeEnv) κ :=  forall TV    (env:@InstantiatedTypeEnv TV Γ), TV κ.
 134 Definition HaskCoVar Γ Δ           :=  forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
 135 Definition HaskLevel (Γ:TypeEnv)   :=  list (HaskTyVar Γ ECKind).
 136 Definition HaskType  (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
 137 Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
 138
 139 Inductive HaskTypeOfSomeKind (Γ:TypeEnv) :=
 140   haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ.
 141   Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ].
 142   Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) :=
 143     match htosk with
 144       haskTypeOfSomeKind κ _ => κ
 145     end.
 146   Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind.
 147   Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk :=
 148     match htosk as H return HaskType Γ H with
 149       haskTypeOfSomeKind _ ht => ht
 150       end.
 151   Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType.
 152
 153 Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
 154     @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
 155 Inductive  LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
 156
 157 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
 158 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
 159   := fun TV env => TAll κ (σ TV env).
 160 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
 161   (cv:HaskTyVar Γ κ) : HaskType Γ ★
 162   := fun TV env => σ TV env (cv TV env).
 163 Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:=
 164   fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
 165 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
 166   := fun TV ite => TCon tc.
 167 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
 168   fun TV ite => TApp (t1 TV ite) (t2 TV ite).
 169 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
 170  fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
 171
 172 Section Flatten.
 173   Context {TV:Kind -> Type }.
 174 Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
 175      match exp with
 176     | TVar    _  x        => x
 177     | TAll     _ y        => TAll   _  (fun v => flattenT  (y (TVar v)))
 178     | TApp   _ _ x y      => TApp      (flattenT  x) (flattenT  y)
 179     | TCon       tc       => TCon      tc
 180     | TCoerc _ t1 t2 t    => TCoerc    (flattenT  t1) (flattenT  t2)   (flattenT  t)
 181     | TArrow              => TArrow
 182     | TCode      v e      => TCode     (flattenT  v) (flattenT  e)
 183     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flattenTyFunApp _ lt)
 184     end
 185     with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
 186     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 187     | TyFunApp_nil               => TyFunApp_nil
 188     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flattenT  t) (flattenTyFunApp _ rest)
 189     end.
 190 End Flatten.
 191
 192 (* PHOAS substitution on types *)
 193 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
 194   : @HaskType Γ κ₂ :=
 195   fun TV env =>
 196     flattenT (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
 197
 198 Notation "t @@  l" := (@mkLeveledHaskType _ _ t l) (at level 20).
 199 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
 200 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
 201
 202 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
 203   match lht with t@@l => t end.
 204
 205 Structure Global Γ :=
 206 { glob_wv    : WeakExprVar
 207 ; glob_kinds : list Kind
 208 ; glob_tf    : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★
 209 }.
 210 Coercion glob_tf : Global >-> Funclass.
 211 Coercion glob_wv : Global >-> WeakExprVar.
 212
 213 (* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
 214 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
 215 Definition take_arg_types : forall {TV}{κ}(exp: RawHaskType TV κ), list (RawHaskType TV κ).
 216 refine (fix take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
 217   match exp as E in RawHaskType _ K return κ=K -> list (RawHaskType _ K) with
 218   | TApp   κ₁ κ₂ x y      =>
 219     fun eqpf =>
 220       ((fun q:list (RawHaskType TV κ₂) =>
 221         match x as X in RawHaskType _ KX return κ₂ ⇛ κ₁ = KX -> list (RawHaskType _ _) with
 222           | TApp   κ₁' κ₂' x' y'      =>
 223             fun eqpf' => match x' in RawHaskType _ KX' return (κ₂' ⇛ κ₁') = KX' -> _ with
 224                            | TArrow => fun eqpf'' => _
 225                            | _      => fun _      => nil
 226                          end (refl_equal _)
 227           | _                         => fun _ => nil
 228         end (refl_equal _))
 229       (take_arg_types TV _ y))
 230     | _                     => fun _ => nil
 231   end (refl_equal _)).
 232   subst; inversion eqpf''; subst.
 233   apply (y'::q).
 234   Defined.
 235
 236 (* From (t1->(t2->(t3-> ... t))), return t *)
 237 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
 238 Definition drop_arg_types : forall {TV}{κ}(exp: RawHaskType TV κ), RawHaskType TV κ.
 239 refine (fix drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : RawHaskType TV κ :=
 240   match exp as E in RawHaskType _ K return κ=K -> RawHaskType _ K with
 241   | TApp   κ₁ κ₂ x y      =>
 242     fun eqpf =>
 243       ((fun q:RawHaskType TV κ₂ =>
 244         match x as X in RawHaskType _ KX return κ₂ ⇛ κ₁ = KX -> RawHaskType _ _ with
 245           | TApp   κ₁' κ₂' x' y'      =>
 246             fun eqpf' => match x' in RawHaskType _ KX' return (κ₂' ⇛ κ₁') = KX' -> _ with
 247                            | TArrow => fun eqpf'' => _
 248                            | z      => fun _      => TApp x y
 249                          end (refl_equal _)
 250           | z                         => fun _ => TApp x y
 251         end (refl_equal _))
 252       (drop_arg_types TV _ y))
 253     | z                     => fun _ => z
 254   end (refl_equal _)).
 255   subst; inversion eqpf''; subst.
 256   apply q.
 257   Defined.
 258
 259
 260
 261
 262 (* yeah, things are kind of messy below this point *)
 263
 264
 265 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
 266   := ilist_tail ite.
 267 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
 268   map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
 269 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
 270   : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
 271 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
 272   (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
 273   : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
 274     simpl.
 275     unfold InstantiatedCoercionEnv.
 276     unfold addKindToCoercionEnv.
 277     simpl.
 278     rewrite <- map_preserves_length.
 279     apply env.
 280     Defined.
 281 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
 282   (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
 283   := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
 284 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
 285   κ::Δ.
 286 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
 287   : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
 288   simpl.
 289   unfold addCoercionToCoercionEnv; simpl.
 290   unfold InstantiatedCoercionEnv; simpl.
 291   apply vec_cons; auto.
 292   Defined.
 293 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
 294 Definition weakITE  {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
 295   := ilist_tail ite.
 296 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
 297   induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
 298 Definition weakCE   {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
 299   := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
 300 Definition weakV  {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
 301   := fun TV ite => (cv' TV (weakITE ite)).
 302 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
 303   induction κ; auto. apply weakV; auto. Defined.
 304 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
 305   := fun TV ite => lt TV (weakITE ite).
 306 Definition weakL  {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
 307   := map weakV lt.
 308 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
 309   induction κ; auto. apply weakT; auto. Defined.
 310 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
 311   unfold HaskType in *.
 312   unfold InstantiatedTypeEnv in *.
 313   intros.
 314   apply ilist_chop in X.
 315   apply lt.
 316   apply X.
 317   Defined.
 318 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a  b) c) κ) : HaskType (app a (app b c)) κ.
 319   rewrite <- ass_app in lt.
 320   exact lt.
 321   Defined.
 322 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
 323   induction κ; auto. apply weakL; auto. Defined.
 324 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
 325   := match lt with t @@ l => weakT t @@ weakL l end.
 326 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
 327   := match lt with t @@ l => weakT' t @@ weakL' l end.
 328 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
 329   induction κ; auto. apply weakCE; auto. Defined.
 330 Definition weakICE  {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
 331   : InstantiatedCoercionEnv TV CV Γ Δ.
 332   intros.
 333   unfold InstantiatedCoercionEnv; intros.
 334   unfold InstantiatedCoercionEnv in ice.
 335   unfold weakCE in ice.
 336   simpl in ice.
 337   rewrite <- map_preserves_length in ice.
 338   apply ice.
 339   Defined.
 340 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
 341   unfold HaskCoercionKind in *.
 342   intros.
 343   apply hck; clear hck.
 344   inversion X; subst; auto.
 345   Defined.
 346 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
 347   induction κ; auto.
 348   apply weakCK.
 349   apply IHκ.
 350   Defined.
 351 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
 352   map weakCK' hck.
 353 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
 354   fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
 355 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
 356   forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
 357   := fun TV ite tv => (f TV (weakITE ite) tv).
 358
 359 Fixpoint caseType0 {Γ}(lk:list Kind) :
 360   IList _ (HaskType Γ) lk ->
 361   HaskType Γ (fold_right KindArrow ★ lk) ->
 362   HaskType Γ ★ :=
 363   match lk as LK return
 364     IList _ (HaskType Γ) LK ->
 365     HaskType Γ (fold_right KindArrow ★ LK) ->
 366     HaskType Γ ★
 367   with
 368   | nil    => fun _     ht => ht
 369   | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
 370   end.
 371
 372 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
 373   caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
 374
 375 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 376 Record StrongAltCon {tc:TyCon} :=
 377 { sac_tc          := tc
 378 ; sac_altcon      :  WeakAltCon
 379 ; sac_numExTyVars :  nat
 380 ; sac_numCoerVars :  nat
 381 ; sac_numExprVars :  nat
 382 ; sac_ekinds      :  vec Kind sac_numExTyVars
 383 ; sac_kinds       := app (tyConKind tc) (vec2list sac_ekinds)
 384 ; sac_Γ           := fun Γ => app (vec2list sac_ekinds) Γ
 385 ; sac_coercions   :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
 386 ; sac_types       :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
 387 ; sac_Δ           := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
 388 }.
 389 Coercion sac_tc     : StrongAltCon >-> TyCon.
 390 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
 391
 392
 393 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
 394
 395 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
 396
 397 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
 398   set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
 399   unfold tyConKind' in z.
 400   rewrite literal_tycons_are_of_ordinary_kind in z.
 401   unfold HaskType.
 402   apply z.
 403   Defined.
 404
 405 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
 406
 407 Fixpoint update_ξ
 408   `{EQD_VV:EqDecidable VV}{Γ}
 409    (ξ:VV -> LeveledHaskType Γ ★)
 410    (lev:HaskLevel Γ)
 411    (vt:list (VV * HaskType Γ ★))
 412    : VV -> LeveledHaskType Γ ★ :=
 413   match vt with
 414     | nil => ξ
 415     | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
 416   end.
 417
 418 Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
 419   not (In v (map (@fst _ _) varstypes)) ->
 420   (update_ξ ξ lev varstypes) v = ξ v.
 421   intros.
 422   induction varstypes.
 423   reflexivity.
 424   simpl.
 425   destruct a.
 426   destruct (eqd_dec v0 v).
 427   subst.
 428   simpl in  H.
 429   assert False.
 430   apply H.
 431   auto.
 432   inversion H0.
 433   apply IHvarstypes.
 434   unfold not; intros.
 435   apply H.
 436   simpl.
 437   auto.
 438   Defined.
 439
 440
 441 (***************************************************************************************************)
 442 (* Well-Formedness of Types and Coercions                                                          *)
 443 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
 444 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
 445   mkTFD : Kind -> TypeFunctionDecl tfc vk.
 446
 447 (*
 448 Section WFCo.
 449   Context {TV:Kind->Type}.
 450   Context {CV:Type}.
 451
 452   (* local notations *)
 453   Notation "ienv '⊢ᴛy' σ : κ"              := (@WellKinded_RawHaskType TV _ ienv σ κ).
 454   Notation "env  ∋  cv : t1 ∼ t2 : Γ : t"  := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
 455                  (at level 20, t1 at level 99, t2 at level 99, t at level 99).
 456   Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
 457         (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
 458
 459   (* Figure 8, lower half *)
 460   Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
 461     @InstantiatedTypeEnv TV Γ ->
 462     @InstantiatedCoercionEnv TV CV Γ Δ ->
 463     @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
 464   | CoTVar':∀ Γ Δ t e c σ τ,
 465     (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ  : Δ : Γ : t
 466   | CoRefl :∀ Γ Δ t e   τ κ,                                         t ⊢ᴛy τ :κ    -> e⊢ᴄᴏ CoType τ    :         τ ∼ τ  : Δ :Γ: t
 467   | Sym    :∀ Γ Δ t e γ σ τ,                            (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t)  -> e⊢ᴄᴏ CoSym  γ    :         τ ∼ σ  : Δ :Γ: t
 468   | Trans  :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂:        σ₁ ∼ σ₃ : Δ :Γ: t
 469   | Left   :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t    )  -> e⊢ᴄᴏ CoLeft  γ   :        σ₁ ∼ τ₁ : Δ :Γ: t
 470   | Right  :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t   )   -> e⊢ᴄᴏ CoRight γ   :        σ₂ ∼ τ₂ : Δ :Γ: t
 471   (*
 472   | SComp  :∀ Γ Δ t e γ n S σ τ κ,
 473             ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ  -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
 474   | CoAx   :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
 475     ListWFCo                              Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
 476     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₁))            (vec2list κ)  ->
 477     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₂))            (vec2list κ)  ->
 478     e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
 479   *)
 480   | WFCoAll  : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ    ,
 481       (∀ a,           e ⊢ᴄᴏ (        γ a) : (       σ a) ∼ (       τ a) : _ : _ : (t + a : κ))
 482       ->    weakICE e ⊢ᴄᴏ (CoAll κ γ  ) : (TAll κ σ  ) ∼ (TAll κ τ  ) : Δ : Γ :  t
 483   | Comp   :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
 484             (t ⊢ᴛy TApp σ₁ σ₂:κ)->
 485             (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
 486             (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
 487             e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
 488   | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
 489           t ⊢ᴛy v TV t : κ  ->
 490             (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
 491             e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
 492   with ListWFCo  : forall Γ (Δ:CoercionEnv Γ),
 493      @InstantiatedTypeEnv TV Γ ->
 494      InstantiatedCoercionEnv TV CV Γ Δ ->
 495      list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
 496   | LWFCo_nil  : ∀ Γ Δ t e ,                                                            ListWFCo Γ Δ t e nil     nil     nil
 497   | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
 498     ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
 499   where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
 500 End WFCo.
 501
 502 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
 503   forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
 504     @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
 505     Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
 506 *)
 507
 508
 509
 510
 511 (* Decidable equality on PHOAS types *)
 512 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
 513 match t1 with
 514 | TVar    _  x     => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
 515 | TAll     _ y     => match t2 with TAll _ y' => compareT (S n) (y n) (y' n)          | _ => false end
 516 | TApp   _ _ x y   => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
 517 | TCon       tc    => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
 518 | TArrow           => match t2 with TArrow => true | _ => false end
 519 | TCode      ec t  => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
 520 | TCoerc _ t1 t2 t => match t2 with TCoerc _ t1' t2' t' => compareT n t1 t1' && compareT n t2 t2' && compareT n t t' | _ =>false end
 521 | TyFunApp tfc kl k lt  => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
 522 end
 523 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
 524 match t1 with
 525 | TyFunApp_nil              => match t2 with TyFunApp_nil => true | _ => false end
 526 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
 527 end.
 528
 529 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
 530 match lk as LK return IList _ _ LK with
 531   | nil    => INil
 532   | h::t   => n::::(count' t (S n))
 533 end.
 534
 535 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
 536   compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
 537
 538 (* The PHOAS axioms
 539  *
 540  * This is not provable in Coq's logic because the Coq function space
 541  * is "too big" - although its only definable inhabitants are Coq
 542  * functions, it is not provable in Coq that all function space
 543  * inhabitants are definable (i.e. there are no "exotic" inhabitants).
 544  * This is actually an important feature of Coq: it lets us reason
 545  * about properties of non-computable (non-recursive) functions since
 546  * any property proven to hold for the entire function space will hold
 547  * even for those functions.  However when representing binding
 548  * structure using functions we would actually prefer the smaller
 549  * function-space of *definable* functions only.  These two axioms
 550  * assert that. *)
 551 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
 552   if compareHT Γ κ ht1 ht2
 553   then ht1=ht2
 554   else ht1≠ht2.
 555 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
 556   if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
 557   then htv1=htv2
 558   else htv1≠htv2.
 559
 560 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
 561 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
 562   apply Build_EqDecidable.
 563   intros.
 564   set (compareHT_decides _ _ v1 v2) as z.
 565   set (compareHT Γ κ v1 v2) as q.
 566   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 567     left; auto.
 568     right; auto.
 569     Defined.
 570
 571 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
 572   apply Build_EqDecidable.
 573   intros.
 574   set (compareVars _ _ v1 v2) as z.
 575   set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
 576   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 577     left; auto.
 578     right; auto.
 579     Defined.
 580
 581 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
 582   apply Build_EqDecidable.
 583   intros.
 584   unfold HaskLevel in *.
 585   apply (eqd_dec v1 v2).
 586   Defined.
 587
 588
 589
 590
 591
 592 (* ToString instance for PHOAS types *)
 593 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
 594     match t with
 595     | TVar    _ v          => "tv" +++ toString v
 596     | TCon    tc           => toString tc
 597     | TCoerc _ t1 t2   t   => "("+++typeToString' false n t1+++"~"
 598                                   +++typeToString' false n t2+++")=>"
 599                                   +++typeToString' needparens n t
 600     | TApp  _ _  t1 t2     =>
 601       match t1 with
 602         | TApp _ _ TArrow t1 =>
 603                      if needparens
 604                      then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
 605                      else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
 606         | _ =>
 607                      if needparens
 608                      then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
 609                      else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
 610       end
 611     | TArrow => "(->)"
 612     | TAll   k f           => let alpha := "tv"+++ toString n
 613                               in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
 614                                    typeToString' false (S n) (f n)
 615     | TCode  ec t          => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
 616     | TyFunApp   tfc kl k lt    => toString tfc+++ "_" +++ toString n+++" ["+++
 617       (fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
 618   end
 619   with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
 620   match t with
 621   | TyFunApp_nil                 => nil
 622   | TyFunApp_cons  κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
 623   end.
 624
 625 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
 626   typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
 627
 628 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
 629   { toString := typeToString }.