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