Explained the forall contract
@@ -30,6 +30,17 @@ typToExpr (tarrow S T) (lam (bind _ (fun l => lam (bind _
(fun t => ite (eunop isFun t) (lam (bind _ (fun x => app (app Ct l) (app t (app (app Cs (neg l)) x))))) (eunop blame l)))))) :-
typToExpr S Cs,
typToExpr T Ct.
+
+(* forall contract
+ * We have two versions of the contract, TyTrue and TyFalse, which one is used
+ * depends on the polarity relative to the polarity at the point the forall is at.
+ * They do the opposite of the other, unwrap or wrap the value depending whether the
+ * polarity has changed or not.
+ * Keep in mind TyTrue and TyFalse is not the instantiation of the variable a to a contract,
+ * but the body of the forall applied to different instantiation, and then converted to a contract.
+ * A simpler implementation should be possible at the expense of extending Nickel,
+ * for now this is the simplest way to proceed.
+ *)
typToExpr (forall (bind _ F)) (lam (bind _ (fun l => ite (pos l) (app TyTrue l) (app TyFalse l)))) :-
typToExpr (F (fromExpr (lam (bind _ (fun lp => lam (bind _ (fun t =>
ite (pos lp)
