[ fix ] subtle infinite loop induced by bad subtyping check

eg/zoiks.ask

@@ -0,0 +1,2 @@
+data Boo = Bah
+prove f Bah = f ?

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

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."

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
 ------------------------------------------------------------------------------

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