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 *)
+(* TODO: 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.
Fixpoint update_ξ
`{EQD_VV:EqDecidable VV}{Γ}
(ξ:VV -> LeveledHaskType Γ ★)
- (vt:list (VV * LeveledHaskType Γ ★))
+ (lev:HaskLevel Γ)
+ (vt:list (VV * HaskType Γ ★))
: VV -> LeveledHaskType Γ ★ :=
match vt with
| nil => ξ
- | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
+ | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
end.
+Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+ not (In v (map (@fst _ _) varstypes)) ->
+ (update_ξ ξ lev varstypes) v = ξ v.
+ intros.
+ induction varstypes.
+ reflexivity.
+ simpl.
+ destruct a.
+ destruct (eqd_dec v0 v).
+ subst.
+ simpl in H.
+ assert False.
+ apply H.
+ auto.
+ inversion H0.
+ apply IHvarstypes.
+ unfold not; intros.
+ apply H.
+ simpl.
+ auto.
+ Defined.
(***************************************************************************************************)