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