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