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.
  13 Require Import HaskCoreVars.
  14 Require Import HaskWeakTypes.
  15 Require Import HaskWeakVars.
  16 Require Import HaskCoreToWeak.
  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
 179 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
 180 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
 181   := fun TV env => TAll κ (σ TV env).
 182 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
 183   (cv:HaskTyVar Γ κ) : HaskType Γ ★
 184   := fun TV env => σ TV env (cv TV env).
 185 Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:=
 186   fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
 187 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindTypeFunction ★ (tyConKind tc))
 188   := fun TV ite => TCon tc.
 189 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
 190   fun TV ite => TApp (t1 TV ite) (t2 TV ite).
 191 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
 192  fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
 193
 194 (* PHOAS substitution on types *)
 195 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
 196   : @HaskType Γ κ₂ :=
 197 fun TV env =>
 198     (fix flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
 199      match exp with
 200     | TVar    _  x        => x
 201     | TAll     _ y        => TAll   _  (fun v => flattenT _ (y (TVar v)))
 202     | TApp   _ _ x y      => TApp      (flattenT _ x) (flattenT _ y)
 203     | TCon       tc       => TCon      tc
 204     | TCoerc _ t1 t2 t    => TCoerc    (flattenT _ t1) (flattenT _ t2)   (flattenT _ t)
 205     | TArrow              => TArrow
 206     | TCode      v e      => TCode     (flattenT _ v) (flattenT _ e)
 207     | TyFunApp       tfc lt => TyFunApp tfc (flattenTyFunApp _ lt)
 208     end
 209     with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
 210     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 211     | TyFunApp_nil               => TyFunApp_nil
 212     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flattenT _ t) (flattenTyFunApp _ rest)
 213     end
 214     for flattenT) _ (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
 215
 216 Notation "t @@  l" := (@mkLeveledHaskType _ _ t l) (at level 20).
 217 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
 218 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
 219
 220 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
 221   match lht with t@@l => t end.
 222
 223
 224
 225
 226
 227
 228 (* yeah, things are kind of messy below this point *)
 229
 230
 231 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
 232   := ilist_tail ite.
 233 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
 234   map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
 235 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
 236   : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
 237 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
 238   (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
 239   : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
 240     simpl.
 241     unfold InstantiatedCoercionEnv.
 242     unfold addKindToCoercionEnv.
 243     simpl.
 244     rewrite <- map_preserves_length.
 245     apply env.
 246     Defined.
 247 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
 248   (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
 249   := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
 250 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
 251   κ::Δ.
 252 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
 253   : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
 254   simpl.
 255   unfold addCoercionToCoercionEnv; simpl.
 256   unfold InstantiatedCoercionEnv; simpl.
 257   apply vec_cons; auto.
 258   Defined.
 259 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
 260 Definition weakITE  {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
 261   := ilist_tail ite.
 262 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
 263   induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
 264 Definition weakCE   {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
 265   := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
 266 Definition weakV  {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
 267   := fun TV ite => (cv' TV (weakITE ite)).
 268 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
 269   induction κ; auto. apply weakV; auto. Defined.
 270 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
 271   := fun TV ite => lt TV (weakITE ite).
 272 Definition weakL  {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
 273   := map weakV lt.
 274 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
 275   induction κ; auto. apply weakT; auto. Defined.
 276 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
 277   unfold HaskType in *.
 278   unfold InstantiatedTypeEnv in *.
 279   intros.
 280   apply ilist_chop in X.
 281   apply lt.
 282   apply X.
 283   Defined.
 284 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a  b) c) κ) : HaskType (app a (app b c)) κ.
 285   rewrite <- ass_app in lt.
 286   exact lt.
 287   Defined.
 288 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
 289   induction κ; auto. apply weakL; auto. Defined.
 290 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
 291   := match lt with t @@ l => weakT t @@ weakL l end.
 292 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
 293   := match lt with t @@ l => weakT' t @@ weakL' l end.
 294 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
 295   induction κ; auto. apply weakCE; auto. Defined.
 296 Definition weakICE  {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
 297   : InstantiatedCoercionEnv TV CV Γ Δ.
 298   intros.
 299   unfold InstantiatedCoercionEnv; intros.
 300   unfold InstantiatedCoercionEnv in ice.
 301   unfold weakCE in ice.
 302   simpl in ice.
 303   rewrite <- map_preserves_length in ice.
 304   apply ice.
 305   Defined.
 306 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
 307   unfold HaskCoercionKind in *.
 308   intros.
 309   apply hck; clear hck.
 310   inversion X; subst; auto.
 311   Defined.
 312 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
 313   induction κ; auto.
 314   apply weakCK.
 315   apply IHκ.
 316   Defined.
 317 (*
 318 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
 319   match κ as K return list (HaskCoercionKind (app K Γ)) with
 320   | nil => hck
 321   | _   => map weakCK' hck
 322   end.
 323 *)
 324 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
 325   map weakCK' hck.
 326 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
 327   fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
 328 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
 329   forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
 330   := fun TV ite tv => (f TV (weakITE ite) tv).
 331
 332 (* I keep mixing up left/right folds *)
 333 (* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *)
 334 (*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*)
 335
 336 Fixpoint caseType0 {Γ}(lk:list Kind) :
 337   IList _ (HaskType Γ) lk ->
 338   HaskType Γ (fold_right KindTypeFunction ★ lk) ->
 339   HaskType Γ ★ :=
 340   match lk as LK return
 341     IList _ (HaskType Γ) LK ->
 342     HaskType Γ (fold_right KindTypeFunction ★ LK) ->
 343     HaskType Γ ★
 344   with
 345   | nil    => fun _     ht => ht
 346   | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
 347   end.
 348
 349 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
 350   caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
 351
 352 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 353 Record StrongAltCon {tc:TyCon} :=
 354 { sac_tc          := tc
 355 ; sac_altcon      :  AltCon
 356 ; sac_numExTyVars :  nat
 357 ; sac_numCoerVars :  nat
 358 ; sac_numExprVars :  nat
 359 ; sac_ekinds      :  vec Kind sac_numExTyVars
 360 ; sac_kinds       := app (tyConKind tc) (vec2list sac_ekinds)
 361 ; sac_Γ           := fun Γ => app (vec2list sac_ekinds) Γ
 362 ; sac_coercions   :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
 363 ; sac_types       :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
 364 ; sac_Δ           := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
 365 }.
 366 Coercion sac_tc     : StrongAltCon >-> TyCon.
 367 Coercion sac_altcon : StrongAltCon >-> AltCon.
 368
 369
 370 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
 371
 372 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
 373
 374 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
 375   set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
 376   unfold tyConKind' in z.
 377   rewrite literal_tycons_are_of_ordinary_kind in z.
 378   unfold HaskType.
 379   apply z.
 380   Defined.
 381
 382 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
 383
 384 Fixpoint update_ξ
 385   `{EQD_VV:EqDecidable VV}{Γ}
 386    (ξ:VV -> LeveledHaskType Γ ★)
 387    (vt:list (VV * LeveledHaskType Γ ★))
 388    : VV -> LeveledHaskType Γ ★ :=
 389   match vt with
 390     | nil => ξ
 391     | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
 392   end.
 393
 394
 395
 396 (***************************************************************************************************)
 397 (* Well-Formedness of Types and Coercions                                                          *)
 398 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
 399 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
 400   mkTFD : Kind -> TypeFunctionDecl tfc vk.
 401
 402 (*
 403 Section WFCo.
 404   Context {TV:Kind->Type}.
 405   Context {CV:Type}.
 406
 407   (* local notations *)
 408   Notation "ienv '⊢ᴛy' σ : κ"              := (@WellKinded_RawHaskType TV _ ienv σ κ).
 409   Notation "env  ∋  cv : t1 ∼ t2 : Γ : t"  := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
 410                  (at level 20, t1 at level 99, t2 at level 99, t at level 99).
 411   Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
 412         (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
 413
 414   (* Figure 8, lower half *)
 415   Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
 416     @InstantiatedTypeEnv TV Γ ->
 417     @InstantiatedCoercionEnv TV CV Γ Δ ->
 418     @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
 419   | CoTVar':∀ Γ Δ t e c σ τ,
 420     (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ  : Δ : Γ : t
 421   | CoRefl :∀ Γ Δ t e   τ κ,                                         t ⊢ᴛy τ :κ    -> e⊢ᴄᴏ CoType τ    :         τ ∼ τ  : Δ :Γ: t
 422   | Sym    :∀ Γ Δ t e γ σ τ,                            (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t)  -> e⊢ᴄᴏ CoSym  γ    :         τ ∼ σ  : Δ :Γ: t
 423   | Trans  :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂:        σ₁ ∼ σ₃ : Δ :Γ: t
 424   | Left   :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t    )  -> e⊢ᴄᴏ CoLeft  γ   :        σ₁ ∼ τ₁ : Δ :Γ: t
 425   | Right  :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t   )   -> e⊢ᴄᴏ CoRight γ   :        σ₂ ∼ τ₂ : Δ :Γ: t
 426   (*
 427   | SComp  :∀ Γ Δ t e γ n S σ τ κ,
 428             ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ  -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
 429   | CoAx   :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
 430     ListWFCo                              Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
 431     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₁))            (vec2list κ)  ->
 432     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₂))            (vec2list κ)  ->
 433     e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
 434   *)
 435   | WFCoAll  : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ    ,
 436       (∀ a,           e ⊢ᴄᴏ (        γ a) : (       σ a) ∼ (       τ a) : _ : _ : (t + a : κ))
 437       ->    weakICE e ⊢ᴄᴏ (CoAll κ γ  ) : (TAll κ σ  ) ∼ (TAll κ τ  ) : Δ : Γ :  t
 438   | Comp   :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
 439             (t ⊢ᴛy TApp σ₁ σ₂:κ)->
 440             (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
 441             (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
 442             e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
 443   | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
 444           t ⊢ᴛy v TV t : κ  ->
 445             (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
 446             e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
 447   with ListWFCo  : forall Γ (Δ:CoercionEnv Γ),
 448      @InstantiatedTypeEnv TV Γ ->
 449      InstantiatedCoercionEnv TV CV Γ Δ ->
 450      list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
 451   | LWFCo_nil  : ∀ Γ Δ t e ,                                                            ListWFCo Γ Δ t e nil     nil     nil
 452   | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
 453     ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
 454   where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
 455 End WFCo.
 456
 457 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
 458   forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
 459     @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
 460     Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
 461 *)
 462
 463
 464
 465
 466 (* Decidable equality on PHOAS types *)
 467 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
 468 match t1 with
 469 | TVar    _  x     => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
 470 | TAll     _ y     => match t2 with TAll _ y' => compareT (S n) (y n) (y' n)          | _ => false end
 471 | TApp   _ _ x y   => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
 472 | TCon       tc    => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
 473 | TArrow           => match t2 with TArrow => true | _ => false end
 474 | TCode      ec t  => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
 475 | 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
 476 | TyFunApp tfc lt  => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
 477 end
 478 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
 479 match t1 with
 480 | TyFunApp_nil              => match t2 with TyFunApp_nil => true | _ => false end
 481 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
 482 end.
 483
 484 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
 485 match lk as LK return IList _ _ LK with
 486   | nil    => INil
 487   | h::t   => n::::(count' t (S n))
 488 end.
 489
 490 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
 491   compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
 492
 493 (* This is not provable in Coq's logic because the Coq function space
 494  * is "too big" - although its only definable inhabitants are Coq
 495  * functions, it is not provable in Coq that all function space
 496  * inhabitants are definable (i.e. there are no "exotic" inhabitants).
 497  * This is actually an important feature of Coq: it lets us reason
 498  * about properties of non-computable (non-recursive) functions since
 499  * any property proven to hold for the entire function space will hold
 500  * even for those functions.  However when representing binding
 501  * structure using functions we would actually prefer the smaller
 502  * function-space of *definable* functions only.  These two axioms
 503  * assert that. *)
 504 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
 505   if compareHT Γ κ ht1 ht2
 506   then ht1=ht2
 507   else ht1≠ht2.
 508 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
 509   if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
 510   then htv1=htv2
 511   else htv1≠htv2.
 512
 513 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
 514 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
 515   apply Build_EqDecidable.
 516   intros.
 517   set (compareHT_decides _ _ v1 v2) as z.
 518   set (compareHT Γ κ v1 v2) as q.
 519   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 520     left; auto.
 521     right; auto.
 522     Defined.
 523
 524 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
 525   apply Build_EqDecidable.
 526   intros.
 527   set (compareVars _ _ v1 v2) as z.
 528   set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
 529   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 530     left; auto.
 531     right; auto.
 532     Defined.
 533
 534 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
 535   apply Build_EqDecidable.
 536   intros.
 537   unfold HaskLevel in *.
 538   apply (eqd_dec v1 v2).
 539   Defined.
 540
 541
 542
 543
 544
 545 (* ToString instance for PHOAS types *)
 546 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
 547     match t with
 548     | TVar    _ v          => "tv" +++ v
 549     | TCon    tc           => toString tc
 550     | TCoerc _ t1 t2   t   => "("+++typeToString' false n t1+++"~"
 551                                   +++typeToString' false n t2+++")=>"
 552                                   +++typeToString' needparens n t
 553     | TApp  _ _  t1 t2     =>
 554       match t1 with
 555         | TApp _ _ TArrow t1 =>
 556                      if needparens
 557                      then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
 558                      else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
 559         | _ =>
 560                      if needparens
 561                      then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
 562                      else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
 563       end
 564     | TArrow => "(->)"
 565     | TAll   k f           => let alpha := "tv"+++n
 566                               in "(forall "+++ alpha +++ ":"+++ k +++")"+++
 567                                    typeToString' false (S n) (f n)
 568     | TCode  ec t          => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
 569     | TyFunApp   tfc lt    => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
 570   end
 571   with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
 572   match t with
 573   | TyFunApp_nil                 => nil
 574   | TyFunApp_cons  κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
 575   end.
 576
 577 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
 578   typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
 579
 580 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
 581   { toString := typeToString }.