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.dataConEqTheta".
  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 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 unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
 203   match lht with t@@l => t end.
 204
 205 Structure Global Γ :=
 206 { glob_wv    : WeakExprVar
 207 ; glob_kinds : list Kind
 208 ; glob_tf    : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★
 209 }.
 210 Coercion glob_tf : Global >-> Funclass.
 211 Coercion glob_wv : Global >-> WeakExprVar.
 212
 213 (* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
 214 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
 215 Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
 216   match exp as E in RawHaskType _ K return list (RawHaskType _ K) with
 217     | TApp   κ₁ κ₂ x y      =>
 218       (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> list (RawHaskType TV κ₂) -> list (RawHaskType _ K1) with
 219          | KindStar =>
 220            match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> list (RawHaskType TV K2) -> list (RawHaskType _ KindStar) with
 221              | KindStar => fun x' =>
 222                match x' return list (RawHaskType TV KindStar) -> list (RawHaskType _ KindStar) with
 223                  | TApp κ₁'' κ₂'' w'' x'' =>
 224                    match κ₂'' as K2'' return RawHaskType TV K2'' -> list (RawHaskType TV KindStar) ->
 225                                                                     list (RawHaskType _ KindStar) with
 226                      | KindStar     =>
 227                        match w'' with
 228                          | TArrow => fun a b => a::b
 229                          | _      => fun _ _ => nil
 230                        end
 231                      | _ => fun _ _ => nil
 232                    end x''
 233                  | _                      => fun _  => nil
 234                end
 235              | _        => fun _ _ => nil
 236            end
 237          | _ => fun _ _ => nil
 238        end) x (take_arg_types y)
 239     | _                     => nil
 240   end.
 241
 242 Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat :=
 243   match exp as E in RawHaskType _ K return nat with
 244     | TApp   κ₁ κ₂ x y      =>
 245       (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with
 246          | KindStar =>
 247            match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with
 248              | KindStar => fun x' =>
 249                match x' return nat -> nat with
 250                  | TApp κ₁'' κ₂'' w'' x'' =>
 251                    match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with
 252                      | KindStar     =>
 253                        match w'' with
 254                          | TArrow => fun a b => S b
 255                          | _      => fun _ _ => 0
 256                        end
 257                      | _ => fun _ _ => 0
 258                    end x''
 259                  | _                      => fun _  => 0
 260                end
 261              | _        => fun _ _ => 0
 262            end
 263          | _ => fun _ _ => 0
 264        end) x (count_arg_types y)
 265     | _                     => 0
 266   end.
 267
 268   Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
 269     intros.
 270     induction Γ.
 271     apply INil.
 272     apply ICons; auto.
 273     apply tt.
 274     Defined.
 275
 276 Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ :=
 277   fun pf =>
 278   fun TV ite =>
 279     match take_arg_types (ht TV ite) with
 280     | nil => Prelude_error "impossible"
 281     | x::y => x
 282     end.
 283
 284 (* From (t1->(t2->(t3-> ... t))), return t *)
 285 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
 286 Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 287   match exp as E in RawHaskType _ K return RawHaskType _ K with
 288     | TApp   κ₁ κ₂ x y      =>
 289       let q :=
 290       (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> (RawHaskType TV κ₂) -> ??(RawHaskType _ K1) with
 291          | KindStar =>
 292            match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> (RawHaskType TV K2) -> ??(RawHaskType _ KindStar) with
 293              | KindStar => fun x' =>
 294                match x' return  (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
 295                  | TApp κ₁'' κ₂'' w'' x'' =>
 296                    match κ₂'' as K2'' return RawHaskType TV K2'' ->  (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
 297                      | KindStar     =>
 298                        match w'' with
 299                          | TArrow => fun _ b => Some b
 300                          | _      => fun _ b => None
 301                        end
 302                      | _ => fun _ b => None
 303                    end x''
 304                  | _       => fun _ => None
 305                end
 306              | _        => fun _ _ => None
 307            end
 308          | _ => fun _ _ => None
 309        end) x (drop_arg_types y)
 310       in match q with
 311            | None   => TApp x y
 312            | Some y => y
 313          end
 314     | b                     => b
 315   end.
 316
 317
 318
 319
 320 (* yeah, things are kind of messy below this point *)
 321
 322
 323 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
 324   := ilist_tail ite.
 325 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
 326   map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
 327 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
 328   : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
 329 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
 330   (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
 331   : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
 332     simpl.
 333     unfold InstantiatedCoercionEnv.
 334     unfold addKindToCoercionEnv.
 335     simpl.
 336     rewrite <- map_preserves_length.
 337     apply env.
 338     Defined.
 339 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
 340   (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
 341   := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
 342 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
 343   κ::Δ.
 344 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
 345   : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
 346   simpl.
 347   unfold addCoercionToCoercionEnv; simpl.
 348   unfold InstantiatedCoercionEnv; simpl.
 349   apply vec_cons; auto.
 350   Defined.
 351 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
 352 Definition weakITE  {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
 353   := ilist_tail ite.
 354 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
 355   induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
 356 Definition weakCE   {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
 357   := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
 358 Definition weakV  {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
 359   := fun TV ite => (cv' TV (weakITE ite)).
 360 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
 361   induction κ; auto. apply weakV; auto. Defined.
 362 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
 363   := fun TV ite => lt TV (weakITE ite).
 364 Definition weakL  {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
 365   := map weakV lt.
 366 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
 367   induction κ; auto. apply weakT; auto. Defined.
 368 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
 369   unfold HaskType in *.
 370   unfold InstantiatedTypeEnv in *.
 371   intros.
 372   apply ilist_chop in X.
 373   apply lt.
 374   apply X.
 375   Defined.
 376 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a  b) c) κ) : HaskType (app a (app b c)) κ.
 377   rewrite <- ass_app in lt.
 378   exact lt.
 379   Defined.
 380 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
 381   induction κ; auto. apply weakL; auto. Defined.
 382 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
 383   := match lt with t @@ l => weakT t @@ weakL l end.
 384 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
 385   := match lt with t @@ l => weakT' t @@ weakL' l end.
 386 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
 387   induction κ; auto. apply weakCE; auto. Defined.
 388 Definition weakICE  {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
 389   : InstantiatedCoercionEnv TV CV Γ Δ.
 390   intros.
 391   unfold InstantiatedCoercionEnv; intros.
 392   unfold InstantiatedCoercionEnv in ice.
 393   unfold weakCE in ice.
 394   simpl in ice.
 395   rewrite <- map_preserves_length in ice.
 396   apply ice.
 397   Defined.
 398 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
 399   unfold HaskCoercionKind in *.
 400   intros.
 401   apply hck; clear hck.
 402   inversion X; subst; auto.
 403   Defined.
 404 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
 405   induction κ; auto.
 406   apply weakCK.
 407   apply IHκ.
 408   Defined.
 409 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
 410   map weakCK' hck.
 411 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
 412   fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
 413 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
 414   forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
 415   := fun TV ite tv => (f TV (weakITE ite) tv).
 416
 417 Fixpoint caseType0 {Γ}(lk:list Kind) :
 418   IList _ (HaskType Γ) lk ->
 419   HaskType Γ (fold_right KindArrow ★ lk) ->
 420   HaskType Γ ★ :=
 421   match lk as LK return
 422     IList _ (HaskType Γ) LK ->
 423     HaskType Γ (fold_right KindArrow ★ LK) ->
 424     HaskType Γ ★
 425   with
 426   | nil    => fun _     ht => ht
 427   | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
 428   end.
 429
 430 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
 431   caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
 432
 433 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 434 Record StrongAltCon {tc:TyCon} :=
 435 { sac_tc          := tc
 436 ; sac_altcon      :  WeakAltCon
 437 ; sac_numExTyVars :  nat
 438 ; sac_numCoerVars :  nat
 439 ; sac_numExprVars :  nat
 440 ; sac_ekinds      :  vec Kind sac_numExTyVars
 441 ; sac_kinds       := app (tyConKind tc) (vec2list sac_ekinds)
 442 ; sac_gamma          := fun Γ => app (vec2list sac_ekinds) Γ
 443 ; sac_coercions   :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars
 444 ; sac_types       :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars
 445 ; sac_delta          := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
 446 }.
 447 Coercion sac_tc     : StrongAltCon >-> TyCon.
 448 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
 449
 450
 451 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
 452
 453 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
 454
 455 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
 456   set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
 457   unfold tyConKind' in z.
 458   rewrite literal_tycons_are_of_ordinary_kind in z.
 459   unfold HaskType.
 460   apply z.
 461   Defined.
 462
 463 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
 464
 465 Fixpoint update_xi
 466   `{EQD_VV:EqDecidable VV}{Γ}
 467    (ξ:VV -> LeveledHaskType Γ ★)
 468    (lev:HaskLevel Γ)
 469    (vt:list (VV * HaskType Γ ★))
 470    : VV -> LeveledHaskType Γ ★ :=
 471   match vt with
 472     | nil => ξ
 473     | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v'
 474   end.
 475
 476 Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
 477   not (In v (map (@fst _ _) varstypes)) ->
 478   (update_xi ξ lev varstypes) v = ξ v.
 479   intros.
 480   induction varstypes.
 481   reflexivity.
 482   simpl.
 483   destruct a.
 484   destruct (eqd_dec v0 v).
 485   subst.
 486   simpl in  H.
 487   assert False.
 488   apply H.
 489   auto.
 490   inversion H0.
 491   apply IHvarstypes.
 492   unfold not; intros.
 493   apply H.
 494   simpl.
 495   auto.
 496   Defined.
 497
 498
 499 (***************************************************************************************************)
 500 (* Well-Formedness of Types and Coercions                                                          *)
 501 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
 502 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
 503   mkTFD : Kind -> TypeFunctionDecl tfc vk.
 504
 505 (*
 506 Section WFCo.
 507   Context {TV:Kind->Type}.
 508   Context {CV:Type}.
 509
 510   (* local notations *)
 511   Notation "ienv '⊢ᴛy' σ : κ"              := (@WellKinded_RawHaskType TV _ ienv σ κ).
 512   Notation "env  ∋  cv : t1 ∼ t2 : Γ : t"  := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
 513                  (at level 20, t1 at level 99, t2 at level 99, t at level 99).
 514   Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
 515         (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
 516
 517   (* Figure 8, lower half *)
 518   Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
 519     @InstantiatedTypeEnv TV Γ ->
 520     @InstantiatedCoercionEnv TV CV Γ Δ ->
 521     @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
 522   | CoTVar':∀ Γ Δ t e c σ τ,
 523     (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ  : Δ : Γ : t
 524   | CoRefl :∀ Γ Δ t e   τ κ,                                         t ⊢ᴛy τ :κ    -> e⊢ᴄᴏ CoType τ    :         τ ∼ τ  : Δ :Γ: t
 525   | Sym    :∀ Γ Δ t e γ σ τ,                            (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t)  -> e⊢ᴄᴏ CoSym  γ    :         τ ∼ σ  : Δ :Γ: t
 526   | Trans  :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂:        σ₁ ∼ σ₃ : Δ :Γ: t
 527   | Left   :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t    )  -> e⊢ᴄᴏ CoLeft  γ   :        σ₁ ∼ τ₁ : Δ :Γ: t
 528   | Right  :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t   )   -> e⊢ᴄᴏ CoRight γ   :        σ₂ ∼ τ₂ : Δ :Γ: t
 529   (*
 530   | SComp  :∀ Γ Δ t e γ n S σ τ κ,
 531             ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ  -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
 532   | CoAx   :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
 533     ListWFCo                              Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
 534     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₁))            (vec2list κ)  ->
 535     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₂))            (vec2list κ)  ->
 536     e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
 537   *)
 538   | WFCoAll  : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ    ,
 539       (∀ a,           e ⊢ᴄᴏ (        γ a) : (       σ a) ∼ (       τ a) : _ : _ : (t + a : κ))
 540       ->    weakICE e ⊢ᴄᴏ (CoAll κ γ  ) : (TAll κ σ  ) ∼ (TAll κ τ  ) : Δ : Γ :  t
 541   | Comp   :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
 542             (t ⊢ᴛy TApp σ₁ σ₂:κ)->
 543             (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
 544             (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
 545             e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
 546   | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
 547           t ⊢ᴛy v TV t : κ  ->
 548             (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
 549             e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
 550   with ListWFCo  : forall Γ (Δ:CoercionEnv Γ),
 551      @InstantiatedTypeEnv TV Γ ->
 552      InstantiatedCoercionEnv TV CV Γ Δ ->
 553      list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
 554   | LWFCo_nil  : ∀ Γ Δ t e ,                                                            ListWFCo Γ Δ t e nil     nil     nil
 555   | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
 556     ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
 557   where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
 558 End WFCo.
 559
 560 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
 561   forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
 562     @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
 563     Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
 564 *)
 565
 566
 567
 568
 569 (* Decidable equality on PHOAS types *)
 570 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
 571 match t1 with
 572 | TVar    _  x     => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
 573 | TAll     _ y     => match t2 with TAll _ y' => compareT (S n) (y n) (y' n)          | _ => false end
 574 | TApp   _ _ x y   => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
 575 | TCon       tc    => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
 576 | TArrow           => match t2 with TArrow => true | _ => false end
 577 | TCode      ec t  => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
 578 | 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
 579 | TyFunApp tfc kl k lt  => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
 580 end
 581 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
 582 match t1 with
 583 | TyFunApp_nil              => match t2 with TyFunApp_nil => true | _ => false end
 584 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
 585 end.
 586
 587 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
 588 match lk as LK return IList _ _ LK with
 589   | nil    => INil
 590   | h::t   => n::::(count' t (S n))
 591 end.
 592
 593 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
 594   compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
 595
 596 (* The PHOAS axioms
 597  *
 598  * This is not provable in Coq's logic because the Coq function space
 599  * is "too big" - although its only definable inhabitants are Coq
 600  * functions, it is not provable in Coq that all function space
 601  * inhabitants are definable (i.e. there are no "exotic" inhabitants).
 602  * This is actually an important feature of Coq: it lets us reason
 603  * about properties of non-computable (non-recursive) functions since
 604  * any property proven to hold for the entire function space will hold
 605  * even for those functions.  However when representing binding
 606  * structure using functions we would actually prefer the smaller
 607  * function-space of *definable* functions only.  These two axioms
 608  * assert that. *)
 609 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
 610   if compareHT Γ κ ht1 ht2
 611   then ht1=ht2
 612   else ht1≠ht2.
 613 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
 614   if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
 615   then htv1=htv2
 616   else htv1≠htv2.
 617
 618 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
 619 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
 620   apply Build_EqDecidable.
 621   intros.
 622   set (compareHT_decides _ _ v1 v2) as z.
 623   set (compareHT Γ κ v1 v2) as q.
 624   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 625     left; auto.
 626     right; auto.
 627     Defined.
 628
 629 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
 630   apply Build_EqDecidable.
 631   intros.
 632   set (compareVars _ _ v1 v2) as z.
 633   set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
 634   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 635     left; auto.
 636     right; auto.
 637     Defined.
 638
 639 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
 640   apply Build_EqDecidable.
 641   intros.
 642   unfold HaskLevel in *.
 643   apply (eqd_dec v1 v2).
 644   Defined.
 645
 646
 647
 648
 649
 650 (* ToString instance for PHOAS types *)
 651 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
 652     match t with
 653     | TVar    _ v          => "tv" +++ toString v
 654     | TCon    tc           => toString tc
 655     | TCoerc _ t1 t2   t   => "("+++typeToString' false n t1+++"~"
 656                                   +++typeToString' false n t2+++")=>"
 657                                   +++typeToString' needparens n t
 658     | TApp  _ _  t1 t2     =>
 659       match t1 with
 660         | TApp _ _ TArrow t1 =>
 661                      if needparens
 662                      then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
 663                      else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
 664         | _ =>
 665                      if needparens
 666                      then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
 667                      else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
 668       end
 669     | TArrow => "(->)"
 670     | TAll   k f           => let alpha := "tv"+++ toString n
 671                               in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
 672                                    typeToString' false (S n) (f n)
 673     | TCode  ec t          => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
 674     | TyFunApp   tfc kl k lt    => toString tfc+++ "_" +++ toString n+++" ["+++
 675       (fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
 676   end
 677   with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
 678   match t with
 679   | TyFunApp_nil                 => nil
 680   | TyFunApp_cons  κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
 681   end.
 682
 683 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
 684   typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
 685
 686 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
 687   { toString := typeToString }.