+Require Import General.
+Require Import HaskKinds.
+Require Import HaskCoreLiterals.
+Require Import HaskCoreTypes.
+Require Import HaskCoreVars.
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
+Require Import HaskWeak.
+Require Import HaskCoreToWeak.
+
+Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
+Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
+Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta".
+Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
+
+(* FIXME: might be a better idea to panic here than simply drop things that look wrong *)
+Definition dataConExTyVars cdc :=
+ filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
+ Opaque dataConExTyVars.
+Definition dataConCoerKinds cdc :=
+ filter (map (fun x => match x with EqPred t1 t2 =>
+ match (
+ coreTypeToWeakType t1 >>= fun t1' =>
+ coreTypeToWeakType t2 >>= fun t2' =>
+ OK (t1',t2'))
+ with OK z => Some z
+ | _ => None
+ end
+ | _ => None
+ end) (dataConEqTheta_ cdc)).
+ Opaque dataConCoerKinds.
+Definition dataConFieldTypes cdc :=
+ filter (map (fun x => match coreTypeToWeakType x with
+ | OK z => Some z
+ | _ => None
+ end) (dataConOrigArgTys_ cdc)).
+
+Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc).
+ Coercion tyConNumKinds : TyCon >-> nat.
+
+Inductive DataCon : TyCon -> Type :=
+ mkDataCon : forall cdc:CoreDataCon, DataCon (dataConTyCon cdc).
+ Definition dataConToCoreDataCon `(dc:DataCon tc) : CoreDataCon := match dc with mkDataCon cdc => cdc end.
+ Coercion mkDataCon : CoreDataCon >-> DataCon.
+ Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon.
+ (*Opaque DataCon.*)
+
+Definition compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool.
+ intros.
+ destruct dc1.
+ destruct dc2.
+ exact (if eqd_dec cdc cdc0 then true else false).
+ Defined.
+
+Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2).
+
+Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc).
+ intros.
+ apply Build_EqDecidable.
+ intros.
+ set (trust_compare_datacons _ v1 v2) as x.
+ set (compare_datacons tc v1 v2) as y.
+ assert (y=compare_datacons tc v1 v2). reflexivity.
+ destruct y; rewrite <- H in x.
+ left; auto.
+ right; auto.
+ Defined.
+
+Definition tyConKind' tc := fold_right KindTypeFunction ★ (tyConKind tc).