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 Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
 216   match exp as E in RawHaskType _ K return list (RawHaskType _ K) with
 217     | TApp   κ₁ κ₂ x y      =>
 218       (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> list (RawHaskType TV κ₂) -> list (RawHaskType _ K1) with
 219          | KindStar =>
 220            match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> list (RawHaskType TV K2) -> list (RawHaskType _ KindStar) with
 221              | KindStar => fun x' =>
 222                match x' return list (RawHaskType TV KindStar) -> list (RawHaskType _ KindStar) with
 223                  | TApp κ₁'' κ₂'' w'' x'' =>
 224                    match κ₂'' as K2'' return RawHaskType TV K2'' -> list (RawHaskType TV KindStar) ->
 225                                                                     list (RawHaskType _ KindStar) with
 226                      | KindStar     =>
 227                        match w'' with
 228                          | TArrow => fun a b => a::b
 229                          | _      => fun _ _ => nil
 230                        end
 231                      | _ => fun _ _ => nil
 232                    end x''
 233                  | _                      => fun _  => nil
 234                end
 235              | _        => fun _ _ => nil
 236            end
 237          | _ => fun _ _ => nil
 238        end) x (take_arg_types y)
 239     | _                     => nil
 240   end.
 241
 242 (* From (t1->(t2->(t3-> ... t))), return t *)
 243 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
 244 Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 245   match exp as E in RawHaskType _ K return RawHaskType _ K with
 246     | TApp   κ₁ κ₂ x y      =>
 247       let q :=
 248       (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> (RawHaskType TV κ₂) -> ??(RawHaskType _ K1) with
 249          | KindStar =>
 250            match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> (RawHaskType TV K2) -> ??(RawHaskType _ KindStar) with
 251              | KindStar => fun x' =>
 252                match x' return  (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
 253                  | TApp κ₁'' κ₂'' w'' x'' =>
 254                    match κ₂'' as K2'' return RawHaskType TV K2'' ->  (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
 255                      | KindStar     =>
 256                        match w'' with
 257                          | TArrow => fun _ b => Some b
 258                          | _      => fun _ b => None
 259                        end
 260                      | _ => fun _ b => None
 261                    end x''
 262                  | _       => fun _ => None
 263                end
 264              | _        => fun _ _ => None
 265            end
 266          | _ => fun _ _ => None
 267        end) x (drop_arg_types y)
 268       in match q with
 269            | None   => TApp x y
 270            | Some y => y
 271          end
 272     | b                     => b
 273   end.
 274
 275
 276
 277
 278 (* yeah, things are kind of messy below this point *)
 279
 280
 281 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
 282   := ilist_tail ite.
 283 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
 284   map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
 285 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
 286   : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
 287 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
 288   (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
 289   : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
 290     simpl.
 291     unfold InstantiatedCoercionEnv.
 292     unfold addKindToCoercionEnv.
 293     simpl.
 294     rewrite <- map_preserves_length.
 295     apply env.
 296     Defined.
 297 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
 298   (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
 299   := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
 300 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
 301   κ::Δ.
 302 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
 303   : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
 304   simpl.
 305   unfold addCoercionToCoercionEnv; simpl.
 306   unfold InstantiatedCoercionEnv; simpl.
 307   apply vec_cons; auto.
 308   Defined.
 309 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
 310 Definition weakITE  {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
 311   := ilist_tail ite.
 312 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
 313   induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
 314 Definition weakCE   {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
 315   := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
 316 Definition weakV  {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
 317   := fun TV ite => (cv' TV (weakITE ite)).
 318 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
 319   induction κ; auto. apply weakV; auto. Defined.
 320 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
 321   := fun TV ite => lt TV (weakITE ite).
 322 Definition weakL  {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
 323   := map weakV lt.
 324 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
 325   induction κ; auto. apply weakT; auto. Defined.
 326 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
 327   unfold HaskType in *.
 328   unfold InstantiatedTypeEnv in *.
 329   intros.
 330   apply ilist_chop in X.
 331   apply lt.
 332   apply X.
 333   Defined.
 334 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a  b) c) κ) : HaskType (app a (app b c)) κ.
 335   rewrite <- ass_app in lt.
 336   exact lt.
 337   Defined.
 338 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
 339   induction κ; auto. apply weakL; auto. Defined.
 340 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
 341   := match lt with t @@ l => weakT t @@ weakL l end.
 342 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
 343   := match lt with t @@ l => weakT' t @@ weakL' l end.
 344 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
 345   induction κ; auto. apply weakCE; auto. Defined.
 346 Definition weakICE  {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
 347   : InstantiatedCoercionEnv TV CV Γ Δ.
 348   intros.
 349   unfold InstantiatedCoercionEnv; intros.
 350   unfold InstantiatedCoercionEnv in ice.
 351   unfold weakCE in ice.
 352   simpl in ice.
 353   rewrite <- map_preserves_length in ice.
 354   apply ice.
 355   Defined.
 356 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
 357   unfold HaskCoercionKind in *.
 358   intros.
 359   apply hck; clear hck.
 360   inversion X; subst; auto.
 361   Defined.
 362 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
 363   induction κ; auto.
 364   apply weakCK.
 365   apply IHκ.
 366   Defined.
 367 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
 368   map weakCK' hck.
 369 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
 370   fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
 371 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
 372   forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
 373   := fun TV ite tv => (f TV (weakITE ite) tv).
 374
 375 Fixpoint caseType0 {Γ}(lk:list Kind) :
 376   IList _ (HaskType Γ) lk ->
 377   HaskType Γ (fold_right KindArrow ★ lk) ->
 378   HaskType Γ ★ :=
 379   match lk as LK return
 380     IList _ (HaskType Γ) LK ->
 381     HaskType Γ (fold_right KindArrow ★ LK) ->
 382     HaskType Γ ★
 383   with
 384   | nil    => fun _     ht => ht
 385   | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
 386   end.
 387
 388 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
 389   caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
 390
 391 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 392 Record StrongAltCon {tc:TyCon} :=
 393 { sac_tc          := tc
 394 ; sac_altcon      :  WeakAltCon
 395 ; sac_numExTyVars :  nat
 396 ; sac_numCoerVars :  nat
 397 ; sac_numExprVars :  nat
 398 ; sac_ekinds      :  vec Kind sac_numExTyVars
 399 ; sac_kinds       := app (tyConKind tc) (vec2list sac_ekinds)
 400 ; sac_Γ           := fun Γ => app (vec2list sac_ekinds) Γ
 401 ; sac_coercions   :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
 402 ; sac_types       :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
 403 ; sac_Δ           := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
 404 }.
 405 Coercion sac_tc     : StrongAltCon >-> TyCon.
 406 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
 407
 408
 409 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
 410
 411 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
 412
 413 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
 414   set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
 415   unfold tyConKind' in z.
 416   rewrite literal_tycons_are_of_ordinary_kind in z.
 417   unfold HaskType.
 418   apply z.
 419   Defined.
 420
 421 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
 422
 423 Fixpoint update_ξ
 424   `{EQD_VV:EqDecidable VV}{Γ}
 425    (ξ:VV -> LeveledHaskType Γ ★)
 426    (lev:HaskLevel Γ)
 427    (vt:list (VV * HaskType Γ ★))
 428    : VV -> LeveledHaskType Γ ★ :=
 429   match vt with
 430     | nil => ξ
 431     | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
 432   end.
 433
 434 Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
 435   not (In v (map (@fst _ _) varstypes)) ->
 436   (update_ξ ξ lev varstypes) v = ξ v.
 437   intros.
 438   induction varstypes.
 439   reflexivity.
 440   simpl.
 441   destruct a.
 442   destruct (eqd_dec v0 v).
 443   subst.
 444   simpl in  H.
 445   assert False.
 446   apply H.
 447   auto.
 448   inversion H0.
 449   apply IHvarstypes.
 450   unfold not; intros.
 451   apply H.
 452   simpl.
 453   auto.
 454   Defined.
 455
 456
 457 (***************************************************************************************************)
 458 (* Well-Formedness of Types and Coercions                                                          *)
 459 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
 460 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
 461   mkTFD : Kind -> TypeFunctionDecl tfc vk.
 462
 463 (*
 464 Section WFCo.
 465   Context {TV:Kind->Type}.
 466   Context {CV:Type}.
 467
 468   (* local notations *)
 469   Notation "ienv '⊢ᴛy' σ : κ"              := (@WellKinded_RawHaskType TV _ ienv σ κ).
 470   Notation "env  ∋  cv : t1 ∼ t2 : Γ : t"  := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
 471                  (at level 20, t1 at level 99, t2 at level 99, t at level 99).
 472   Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
 473         (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
 474
 475   (* Figure 8, lower half *)
 476   Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
 477     @InstantiatedTypeEnv TV Γ ->
 478     @InstantiatedCoercionEnv TV CV Γ Δ ->
 479     @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
 480   | CoTVar':∀ Γ Δ t e c σ τ,
 481     (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ  : Δ : Γ : t
 482   | CoRefl :∀ Γ Δ t e   τ κ,                                         t ⊢ᴛy τ :κ    -> e⊢ᴄᴏ CoType τ    :         τ ∼ τ  : Δ :Γ: t
 483   | Sym    :∀ Γ Δ t e γ σ τ,                            (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t)  -> e⊢ᴄᴏ CoSym  γ    :         τ ∼ σ  : Δ :Γ: t
 484   | Trans  :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂:        σ₁ ∼ σ₃ : Δ :Γ: t
 485   | Left   :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t    )  -> e⊢ᴄᴏ CoLeft  γ   :        σ₁ ∼ τ₁ : Δ :Γ: t
 486   | Right  :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t   )   -> e⊢ᴄᴏ CoRight γ   :        σ₂ ∼ τ₂ : Δ :Γ: t
 487   (*
 488   | SComp  :∀ Γ Δ t e γ n S σ τ κ,
 489             ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ  -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
 490   | CoAx   :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
 491     ListWFCo                              Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
 492     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₁))            (vec2list κ)  ->
 493     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₂))            (vec2list κ)  ->
 494     e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
 495   *)
 496   | WFCoAll  : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ    ,
 497       (∀ a,           e ⊢ᴄᴏ (        γ a) : (       σ a) ∼ (       τ a) : _ : _ : (t + a : κ))
 498       ->    weakICE e ⊢ᴄᴏ (CoAll κ γ  ) : (TAll κ σ  ) ∼ (TAll κ τ  ) : Δ : Γ :  t
 499   | Comp   :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
 500             (t ⊢ᴛy TApp σ₁ σ₂:κ)->
 501             (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
 502             (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
 503             e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
 504   | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
 505           t ⊢ᴛy v TV t : κ  ->
 506             (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
 507             e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
 508   with ListWFCo  : forall Γ (Δ:CoercionEnv Γ),
 509      @InstantiatedTypeEnv TV Γ ->
 510      InstantiatedCoercionEnv TV CV Γ Δ ->
 511      list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
 512   | LWFCo_nil  : ∀ Γ Δ t e ,                                                            ListWFCo Γ Δ t e nil     nil     nil
 513   | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
 514     ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
 515   where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
 516 End WFCo.
 517
 518 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
 519   forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
 520     @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
 521     Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
 522 *)
 523
 524
 525
 526
 527 (* Decidable equality on PHOAS types *)
 528 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
 529 match t1 with
 530 | TVar    _  x     => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
 531 | TAll     _ y     => match t2 with TAll _ y' => compareT (S n) (y n) (y' n)          | _ => false end
 532 | TApp   _ _ x y   => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
 533 | TCon       tc    => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
 534 | TArrow           => match t2 with TArrow => true | _ => false end
 535 | TCode      ec t  => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
 536 | 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
 537 | TyFunApp tfc kl k lt  => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
 538 end
 539 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
 540 match t1 with
 541 | TyFunApp_nil              => match t2 with TyFunApp_nil => true | _ => false end
 542 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
 543 end.
 544
 545 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
 546 match lk as LK return IList _ _ LK with
 547   | nil    => INil
 548   | h::t   => n::::(count' t (S n))
 549 end.
 550
 551 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
 552   compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
 553
 554 (* The PHOAS axioms
 555  *
 556  * This is not provable in Coq's logic because the Coq function space
 557  * is "too big" - although its only definable inhabitants are Coq
 558  * functions, it is not provable in Coq that all function space
 559  * inhabitants are definable (i.e. there are no "exotic" inhabitants).
 560  * This is actually an important feature of Coq: it lets us reason
 561  * about properties of non-computable (non-recursive) functions since
 562  * any property proven to hold for the entire function space will hold
 563  * even for those functions.  However when representing binding
 564  * structure using functions we would actually prefer the smaller
 565  * function-space of *definable* functions only.  These two axioms
 566  * assert that. *)
 567 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
 568   if compareHT Γ κ ht1 ht2
 569   then ht1=ht2
 570   else ht1≠ht2.
 571 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
 572   if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
 573   then htv1=htv2
 574   else htv1≠htv2.
 575
 576 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
 577 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
 578   apply Build_EqDecidable.
 579   intros.
 580   set (compareHT_decides _ _ v1 v2) as z.
 581   set (compareHT Γ κ v1 v2) as q.
 582   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 583     left; auto.
 584     right; auto.
 585     Defined.
 586
 587 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
 588   apply Build_EqDecidable.
 589   intros.
 590   set (compareVars _ _ v1 v2) as z.
 591   set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
 592   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 593     left; auto.
 594     right; auto.
 595     Defined.
 596
 597 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
 598   apply Build_EqDecidable.
 599   intros.
 600   unfold HaskLevel in *.
 601   apply (eqd_dec v1 v2).
 602   Defined.
 603
 604
 605
 606
 607
 608 (* ToString instance for PHOAS types *)
 609 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
 610     match t with
 611     | TVar    _ v          => "tv" +++ toString v
 612     | TCon    tc           => toString tc
 613     | TCoerc _ t1 t2   t   => "("+++typeToString' false n t1+++"~"
 614                                   +++typeToString' false n t2+++")=>"
 615                                   +++typeToString' needparens n t
 616     | TApp  _ _  t1 t2     =>
 617       match t1 with
 618         | TApp _ _ TArrow t1 =>
 619                      if needparens
 620                      then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
 621                      else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
 622         | _ =>
 623                      if needparens
 624                      then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
 625                      else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
 626       end
 627     | TArrow => "(->)"
 628     | TAll   k f           => let alpha := "tv"+++ toString n
 629                               in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
 630                                    typeToString' false (S n) (f n)
 631     | TCode  ec t          => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
 632     | TyFunApp   tfc kl k lt    => toString tfc+++ "_" +++ toString n+++" ["+++
 633       (fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
 634   end
 635   with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
 636   match t with
 637   | TyFunApp_nil                 => nil
 638   | TyFunApp_cons  κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
 639   end.
 640
 641 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
 642   typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
 643
 644 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
 645   { toString := typeToString }.