From e6cf303d3acce1d82e1dc477efc67867cbacf3c3 Mon Sep 17 00:00:00 2001
From: JJ
Date: Sat, 31 Aug 2024 15:46:09 -0700
Subject: stlc-full: fix bug in context stratification

---
 stlc-full.rkt | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/stlc-full.rkt b/stlc-full.rkt
index 434c906..b25b56c 100644
--- a/stlc-full.rkt
+++ b/stlc-full.rkt
@@ -503,15 +503,15 @@
 (define (equiv-type-core t1 t2 Γ1 Γ2)
   (match* (t1 t2)
     ; bound identifiers: if a key exists in the context, look it up
-    [(x1 x2) #:when (dict-has-key? Γ1 x1)
-      (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
-    [(x1 x2) #:when (dict-has-key? Γ2 x2)
-      (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
+    [(x1 x2) #:when (dict-has-key? Γ1 `(type ,x1))
+      (equiv-type-core (dict-ref Γ1 `(type ,x1)) x2 Γ1 Γ2)]
+    [(x1 x2) #:when (dict-has-key? Γ2 `(type ,x2))
+      (equiv-type-core x1 (dict-ref Γ2 `(type ,x2)) Γ1 Γ2)]
 
     ; recursive types: self-referential names can be arbitrary
     [(`(μ ,x1 ,t1) `(μ ,x2 ,t2))
       (let ([name gensym])
-        (equiv-type-core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
+        (equiv-type-core t1 t2 (dict-set Γ1 `(type ,x1) name) (dict-set Γ2 `(type ,x2) name)))]
 
     ; check for syntactic equivalence on remaining forms
     [(`(,l1 ...) `(,l2 ...))
@@ -860,9 +860,9 @@
           (some ⇒ (! (cdr (cdr some))))
           (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))))
   '(DoublyLinkedList → 1 DoublyLinkedList)
-    #hash((DoublyLinkedList . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))))
+    #hash(((type DoublyLinkedList) . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))))
 
-(check-true ; FIXME: fold is not in check form?
+(check-true
   (check (desugar '
     (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
     (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit)))
-- 
cgit v1.2.3-70-g09d2