-(* Figure 8, upper half *)
-Inductive WellKinded_RawHaskType (TV:Type)
- : forall Γ:TypeEnv, InstantiatedTypeEnv TV Γ -> RawHaskType TV -> Kind -> Prop :=
- | WFTyVar : forall Γ env κ d,
- env∋d:κ ->
- WellKinded_RawHaskType TV Γ env (TVar d) κ
- | WFTyApp : forall Γ env κ₁ κ₂ σ₁ σ₂,
- WellKinded_RawHaskType TV Γ env σ₁ (κ₁ ⇛ κ₂) ->
- WellKinded_RawHaskType TV Γ env σ₂ κ₂ ->
- WellKinded_RawHaskType TV Γ env (TApp σ₁ σ₂) κ₂
- | WFTyAll : forall Γ (env:InstantiatedTypeEnv TV Γ) κ σ ,
- (∀ a, WellKinded_RawHaskType TV _ (@addKindToInstantiatedTypeEnv _ TV env a κ) (σ a) ★ ) ->
- WellKinded_RawHaskType TV _ env (TAll κ σ) ★
- | TySCon : forall Γ env tfc lt vk ι ,
- @TypeFunctionDecl tfc vk ->
- ListWellKinded_RawHaskType TV Γ _ env lt vk ->
- WellKinded_RawHaskType TV Γ env (TFCApp tfc lt) ι
-with ListWellKinded_RawHaskType (TV:Type)
- : forall (Γ:TypeEnv) n, InstantiatedTypeEnv TV Γ -> vec (RawHaskType TV) n -> vec Kind n -> Prop :=
- | ListWFRawHaskTypenil : forall Γ env,
- ListWellKinded_RawHaskType TV Γ 0 env vec_nil vec_nil
- | ListWFRawHaskTypecons : forall Γ env n t k lt lk,
- WellKinded_RawHaskType TV Γ env t k ->
- ListWellKinded_RawHaskType TV Γ n env lt lk ->
- ListWellKinded_RawHaskType TV Γ (S n) env (t:::lt) (k:::lk).
-
-Variable kindOfTyCon : forall (tc:TyCon), Kind.
- Extract Inlined Constant kindOfTyCon => "(\x -> Prelude.error ""not implemented yet"")".
-
-Fixpoint kindOfRawHaskType (rht:RawHaskType Kind) : ???Kind :=
-match rht with
- | TVar k => OK k
- | TCon tc => OK (kindOfTyCon tc)
- | TCoerc t1 t2 t => OK (★ ⇛ ★ )
- | TArrow => OK (★ ⇛ ★ ⇛ ★ )
- | TApp ht1 ht2 => kindOfRawHaskType ht1 >>= fun k1 =>
- kindOfRawHaskType ht2 >>= fun k2 =>
- match k1 with
- | k1' ⇛ k2' => if eqd_dec k1' k1 then OK k2' else Error "kind mismatch"
- | _ => Error "attempt to apply a non-functional kind"
- end
- | TFCApp tc rht' => Error "calculating kind of TFCApp is not yet implemented"
- | TAll k t' => kindOfRawHaskType (t' k) >>= fun k' => OK (k ⇛ k')
- | TCode t1 t2 => OK ★
-end.