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