+Definition coreTypeToWeakType t :=
+ addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).
+
+Definition coreVarToWeakVar' (cv:CoreVar) : ???WeakVar :=
+ addErrorMessage ("during coreVarToWeakVar on " +++ toString cv +++ eol)
+ match coreVarToWeakVar cv with
+ | CVTWVR_EVar ct => coreTypeToWeakType ct >>= fun t' => OK (WExprVar (weakExprVar cv t'))
+ | CVTWVR_TyVar k => OK (WTypeVar (weakTypeVar cv k))
+ | CVTWVR_CoVar t1 t2 =>
+ (* this will choke if given a coercion-between-coercions (EqPred (EqPred c1 c2) (EqPred c3 c4)) *)
+ addErrorMessage ("with t2=" +++ toString t2 +++ eol)
+ ((coreTypeToWeakType t2) >>= fun t2' =>
+ addErrorMessage ("with t1=" +++ toString t1 +++ eol)
+ (coreTypeToWeakType t1) >>= fun t1' =>
+ OK (WCoerVar (weakCoerVar cv t1' t2')))
+ end.
+Definition tyConTyVars (tc:CoreTyCon) :=
+ filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (getTyConTyVars_ tc)).
+ Opaque tyConTyVars.
+Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).