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' =>