+Require Import General.
+Require Import HaskKinds.
+Require Import HaskCoreLiterals.
+Require Import HaskCoreTypes. (* FIXME *)
+Require Import HaskCoreVars. (* FIXME *)
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars. (* FIXME *)
+Require Import HaskCoreToWeak. (* FIXME *)
+
+Variable CoFunConst : nat -> Type. (* FIXME *)
+Variable TyFunConst : nat -> Type. (* FIXME *)
+
+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".
+Variable getTyConTyVars_ : TyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "TyCon.tyConTyVars".
+
+(* FIXME: might be a better idea to panic here than simply drop things that look wrong *)
+Definition tyConTyVars (tc:TyCon) :=
+ filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)).
+ Opaque tyConTyVars.
+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.