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