From 112c4686d1f02963905c02dcaaf648dca48cf768 Mon Sep 17 00:00:00 2001
From: Conor McBride <conor@strictlypositive.org>
Date: Tue, 15 Oct 2024 12:13:59 +0100
Subject: [PATCH] [ fix ] subtle infinite loop induced by bad subtyping check

---
 eg/zoiks.ask                 |  2 ++
 lib/Language/Ask/Context.hs  |  1 +
 lib/Language/Ask/Printing.hs |  1 +
 lib/Language/Ask/Tm.hs       | 29 +++++++++++++++++++++++++++++
 lib/Language/Ask/Typing.hs   | 22 ++++++++++++++--------
 5 files changed, 47 insertions(+), 8 deletions(-)
 create mode 100644 eg/zoiks.ask

diff --git a/eg/zoiks.ask b/eg/zoiks.ask
new file mode 100644
index 0000000..f06f5c3
--- /dev/null
+++ b/eg/zoiks.ask
@@ -0,0 +1,2 @@
+data Boo = Bah
+prove f Bah = f ?
diff --git a/lib/Language/Ask/Context.hs b/lib/Language/Ask/Context.hs
index 8f7830c..59d10d3 100644
--- a/lib/Language/Ask/Context.hs
+++ b/lib/Language/Ask/Context.hs
@@ -85,6 +85,7 @@ data Gripe
   | UnderNeedsEq Tm
   | NotGiven Tm
   | NotEqual
+  | InfiniteType
   | Terror [LexL] Tm Tm
   | NotARule Appl
   | BadRec String
diff --git a/lib/Language/Ask/Printing.hs b/lib/Language/Ask/Printing.hs
index 33caf7b..51d66c6 100644
--- a/lib/Language/Ask/Printing.hs
+++ b/lib/Language/Ask/Printing.hs
@@ -223,6 +223,7 @@ ppGripe (ParseNoMake s) = return $ concat
   ["This doesn't make ", s, "."]
 ppGripe ParseStubSub = return "Don't give subtrees until you've chosen a production."
 ppGripe (Bland x) = return x
+ppGripe InfiniteType = return "Can't make an infinite type!"
 
 ppGripe FAIL = return $
   "It went wrong but I've forgotten how. Please ask a human for help."
diff --git a/lib/Language/Ask/Tm.hs b/lib/Language/Ask/Tm.hs
index 47ae88f..2dd6edf 100644
--- a/lib/Language/Ask/Tm.hs
+++ b/lib/Language/Ask/Tm.hs
@@ -69,6 +69,35 @@ pattern Big    = TC "Z" []
 type Nom = [(String, Int)]   -- names for parameters are chosen by the system
 
 
+------------------------------------------------------------------------------
+--  Subterm Checking
+------------------------------------------------------------------------------
+
+class SubTm t where
+  subTm :: Tm -> t -> Bool
+
+instance SubTm Tm where
+  subTm s t | s == t = True
+  subTm s (TM _ ss) = subTm s ss
+  subTm s (TC _ ts) = subTm s ts
+  subTm s (TB b) = subTm s b
+  subTm s (TE e) = subTm s e
+
+instance SubTm Syn where
+  subTm s (tm ::: ty) = subTm s tm || subTm s ty
+  subTm s (e :$ t) = subTm s e || subTm s t
+  subTm _ _ = False
+
+instance SubTm t => SubTm [t] where
+  subTm = any . subTm
+
+instance SubTm t => SubTm (Bind t) where
+  subTm s (K b) = subTm s b
+  subTm s (L b) = subTm (s <^> o' mempty) b
+
+  
+
+
 ------------------------------------------------------------------------------
 --  Patterns
 ------------------------------------------------------------------------------
diff --git a/lib/Language/Ask/Typing.hs b/lib/Language/Ask/Typing.hs
index 441804b..7d4a031 100644
--- a/lib/Language/Ask/Typing.hs
+++ b/lib/Language/Ask/Typing.hs
@@ -423,14 +423,20 @@ subtype s t = do
   go s t
  where
   go s t | track ("SOOTY " ++ show s ++ " " ++ show t) False = undefined
-  go (TC "->" [s0, t0]) u = do
-    (s1, t1) <- makeFun u
-    subtype s1 s0
-    subtype t0 t1
-  go u (TC "->" [s1, t1]) = do
-    (s0, t0) <- makeFun u
-    subtype s1 s0
-    subtype t0 t1
+  go (TC "->" [s0, t0]) u =
+    if subTm u [s0, t0]
+    then gripe InfiniteType
+    else do
+      (s1, t1) <- makeFun u
+      subtype s1 s0
+      subtype t0 t1
+  go u (TC "->" [s1, t1]) =
+    if subTm u [s1, t1]
+    then gripe InfiniteType
+    else do
+      (s0, t0) <- makeFun u
+      subtype s1 s0
+      subtype t0 t1
   go (TC "$" [ty0, non0, num0]) (TC "$" [ty1, non1, num1]) = do
     unify Type ty0 ty1
     unify Zone non0 non1