Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskKinds.
Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskKinds.
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskCoreVars.
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskCoreVars.
Coercion coVarKind : WeakCoerVar >-> Kind.
Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
Coercion coVarKind : WeakCoerVar >-> Kind.
Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
weakTypeOfWeakExpr e >>= fun te =>
weakTypeToTypeOfKind φ te ★ >>= fun te' =>
weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
weakTypeOfWeakExpr e >>= fun te =>
weakTypeToTypeOfKind φ te ★ >>= fun te' =>
weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>