Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskWeakTypes.
Require Import HaskWeakVars.
Require Import HaskWeak.
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
Open Scope string_scope.
Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
Defined.
Definition coVarKind (wcv:WeakCoerVar) : Kind :=
- match wcv with weakCoerVar _ κ _ _ => κ end.
+ match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
Coercion coVarKind : WeakCoerVar >-> Kind.
Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
| _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
end
- | WECoLam cv e => let (_,_,t1,t2) := cv in
+ | WECoLam cv e => let (_,t1,t2) := cv in
weakTypeOfWeakExpr e >>= fun te =>
weakTypeToTypeOfKind φ te ★ >>= fun te' =>
weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>