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