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