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    (vt:list (VV * LeveledHaskType Γ ★))
 389    : VV -> LeveledHaskType Γ ★ :=
 390   match vt with
 391     | nil => ξ
 392     | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
 393   end.
 394
 395
 396
 397 (***************************************************************************************************)
 398 (* Well-Formedness of Types and Coercions                                                          *)
 399 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
 400 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
 401   mkTFD : Kind -> TypeFunctionDecl tfc vk.
 402
 403 (*
 404 Section WFCo.
 405   Context {TV:Kind->Type}.
 406   Context {CV:Type}.
 407
 408   (* local notations *)
 409   Notation "ienv '⊢ᴛy' σ : κ"              := (@WellKinded_RawHaskType TV _ ienv σ κ).
 410   Notation "env  ∋  cv : t1 ∼ t2 : Γ : t"  := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
 411                  (at level 20, t1 at level 99, t2 at level 99, t at level 99).
 412   Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
 413         (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
 414
 415   (* Figure 8, lower half *)
 416   Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
 417     @InstantiatedTypeEnv TV Γ ->
 418     @InstantiatedCoercionEnv TV CV Γ Δ ->
 419     @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
 420   | CoTVar':∀ Γ Δ t e c σ τ,
 421     (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ  : Δ : Γ : t
 422   | CoRefl :∀ Γ Δ t e   τ κ,                                         t ⊢ᴛy τ :κ    -> e⊢ᴄᴏ CoType τ    :         τ ∼ τ  : Δ :Γ: t
 423   | Sym    :∀ Γ Δ t e γ σ τ,                            (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t)  -> e⊢ᴄᴏ CoSym  γ    :         τ ∼ σ  : Δ :Γ: t
 424   | Trans  :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂:        σ₁ ∼ σ₃ : Δ :Γ: t
 425   | Left   :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t    )  -> e⊢ᴄᴏ CoLeft  γ   :        σ₁ ∼ τ₁ : Δ :Γ: t
 426   | Right  :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t   )   -> e⊢ᴄᴏ CoRight γ   :        σ₂ ∼ τ₂ : Δ :Γ: t
 427   (*
 428   | SComp  :∀ Γ Δ t e γ n S σ τ κ,
 429             ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ  -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
 430   | CoAx   :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
 431     ListWFCo                              Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
 432     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₁))            (vec2list κ)  ->
 433     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₂))            (vec2list κ)  ->
 434     e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
 435   *)
 436   | WFCoAll  : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ    ,
 437       (∀ a,           e ⊢ᴄᴏ (        γ a) : (       σ a) ∼ (       τ a) : _ : _ : (t + a : κ))
 438       ->    weakICE e ⊢ᴄᴏ (CoAll κ γ  ) : (TAll κ σ  ) ∼ (TAll κ τ  ) : Δ : Γ :  t
 439   | Comp   :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
 440             (t ⊢ᴛy TApp σ₁ σ₂:κ)->
 441             (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
 442             (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
 443             e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
 444   | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
 445           t ⊢ᴛy v TV t : κ  ->
 446             (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
 447             e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
 448   with ListWFCo  : forall Γ (Δ:CoercionEnv Γ),
 449      @InstantiatedTypeEnv TV Γ ->
 450      InstantiatedCoercionEnv TV CV Γ Δ ->
 451      list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
 452   | LWFCo_nil  : ∀ Γ Δ t e ,                                                            ListWFCo Γ Δ t e nil     nil     nil
 453   | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
 454     ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
 455   where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
 456 End WFCo.
 457
 458 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
 459   forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
 460     @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
 461     Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
 462 *)
 463
 464
 465
 466
 467 (* Decidable equality on PHOAS types *)
 468 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
 469 match t1 with
 470 | TVar    _  x     => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
 471 | TAll     _ y     => match t2 with TAll _ y' => compareT (S n) (y n) (y' n)          | _ => false end
 472 | TApp   _ _ x y   => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
 473 | TCon       tc    => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
 474 | TArrow           => match t2 with TArrow => true | _ => false end
 475 | TCode      ec t  => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
 476 | 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
 477 | TyFunApp tfc lt  => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
 478 end
 479 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
 480 match t1 with
 481 | TyFunApp_nil              => match t2 with TyFunApp_nil => true | _ => false end
 482 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
 483 end.
 484
 485 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
 486 match lk as LK return IList _ _ LK with
 487   | nil    => INil
 488   | h::t   => n::::(count' t (S n))
 489 end.
 490
 491 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
 492   compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
 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" +++ 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"+++n
 567                               in "(forall "+++ alpha +++ ":"+++ k +++")"+++
 568                                    typeToString' false (S n) (f n)
 569     | TCode  ec t          => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
 570     | TyFunApp   tfc lt    => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
 571   end
 572   with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
 573   match t with
 574   | TyFunApp_nil                 => nil
 575   | TyFunApp_cons  κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
 576   end.
 577
 578 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
 579   typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
 580
 581 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
 582   { toString := typeToString }.