From 44d184b6d4a198a720b8d50a2fb127c77459e08e Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Thu, 8 Feb 2024 15:47:35 +0100
Subject: [PATCH] Infer.has_type: include a full example of a constraint that
 works for (lambda x. x)

Suggested-by: Dai Weituo
---
 src/Infer.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/Infer.ml b/src/Infer.ml
index 2069528..4c72967 100644
--- a/src/Infer.ml
+++ b/src/Infer.ml
@@ -64,6 +64,19 @@ module Make(T : Utils.Functor) = struct
       For example, if [t] is the term [lambda x. x], then [has_type env t w]
       generates a constraint equivalent to [∃?v. ?w = (?v -> ?v)].
 
+      More precisely, one possible generated constraint would be:
+      {[
+        Exist(v, None,
+          Map(
+            Conj(
+              Exist (arr, Some (Arrow (v, v)), Eq (arr, w)),
+              MapErr(Decode v, fun e -> Cycle e)
+            ),
+            fun ((), ty) -> Abs (x, ty, Var x)
+        ))
+      ]}
+      but the actually generated constraint may be more complex/verbose.
+
       Precondition: when calling [has_type env t], [env] must map each
       term variable that is free in [t] to an inference variable.
   *)