missing occurs check

full/pi/Hurkens.pi

@@ -1,26 +1,38 @@
 -- from Jonathan Chan
 module Hurkens where
 
-data Void : Type where {}
+Void : Type
+Void = (x:Type) -> x
+
 neg : Type -> Type
 neg = \X. X -> Void
+
 P : Type -> Type
 P = \S. S -> Type
+
 U : Type
 U = (x : Type) -> ((P (P x)) -> x) -> P (P x)
+
 tau : (P (P U)) -> U
 tau = \t. \x. \f. \p. t (\s. p (f (s x f)))
+
 sigma : U -> P (P U)
 sigma = \s. s U (\t. tau t)
+
 Delta : P U
 Delta = \y. neg ((p : P U) -> sigma y p -> p (tau (sigma y)))
+
 Omega : U
 Omega = tau (\p. (x : U) -> sigma x p -> p x)
+
 R : (p : P U) -> ((x : U) -> sigma x p -> p x) -> p Omega
 R = \zero. \one. one Omega (\x. one (tau (sigma x)))
+
 M : (x : U) -> sigma x Delta -> Delta x
 M = \x. \two. \three. three Delta two (\p. three (\y. p (tau (sigma y))))
+
 L : neg ((p : P U) -> ((x : U) -> sigma x p -> p x) -> p Omega)
 L = \zero. zero Delta M (\p. zero (\y. p (tau (sigma y))))
+
 false : Void
 false = L R

full/src/Equal.hs

@@ -243,8 +243,8 @@ unify ns tx ty = do
     then return []
     else case (txnf, tynf) of
       (Var x, Var y) | x == y -> return []
-      (Var y, yty) | y `notElem` ns -> return [Def y yty]
-      (yty, Var y) | y `notElem` ns -> return [Def y yty]
+      (Var y, yty) | y `notElem` ns && y `notElem` fv yty -> return [Def y yty]
+      (yty, Var y) | y `notElem` ns && y `notElem` fv yty -> return [Def y yty]
       (Prod a1 a2, Prod b1 b2) -> unifyArgs [Arg Rel a1, Arg Rel a2] [Arg Rel b1, Arg Rel b2]  
 
       (TyEq a1 a2, TyEq b1 b2) -> (++) <$> unify ns a1 b1 <*> unify ns a2 b2 

full/src/PrettyPrint.hs

@@ -1,7 +1,7 @@
 {- pi-forall language -}
 
 -- | A Pretty Printer.
-module PrettyPrint (Disp (..), D (..), SourcePos, PP.Doc, PP.render, pp) where
+module PrettyPrint (Disp (..), D (..), SourcePos, PP.Doc, PP.render, pp, debug) where
 
 import Control.Monad.Reader (MonadReader (ask, local), asks)
 import Data.Set qualified as S
@@ -71,7 +71,8 @@ initDI :: DispInfo
 initDI = DI {showAnnots = False,
                           dispAvoid = S.empty,
                           prec = 0,
-                          showLongNames = True}
+                          showLongNames = False
+                          }
 
 
 -------------------------------------------------------------------------
@@ -128,6 +129,8 @@ instance Disp Sig
 
 instance Disp Arg
 
+instance Disp [Arg]
+
 
 instance Disp Pattern
 
@@ -334,7 +337,13 @@ brackets :: Bool -> Doc -> Doc
 brackets b = if b then PP.brackets else id
 
 instance Display (Unbound.Name Term) where
-  display = return . disp
+  display n = do
+    b <- ask showLongNames
+    return (if b then debugDisp n else disp n)
+
+instance Display [Arg] where
+   display a = PP.sep <$> mapM display a
+
 
 instance Display Term where
   display TyType = return $ PP.text "Type"

full/src/Syntax.hs

@@ -10,6 +10,8 @@ import Data.Typeable (Typeable)
 import GHC.Generics (Generic,from)
 import Text.ParserCombinators.Parsec.Pos (SourcePos, initialPos, newPos)
 import Unbound.Generics.LocallyNameless qualified as Unbound
+import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound
+
 import Data.Function (on)
 
 -----------------------------------------
@@ -380,7 +382,11 @@ pi2 = TyPi Rel TyBool (Unbound.bind yName (Var yName))
 -- True
 -- 
 
+---------------
+-- | Bridge function to calculate the free variables of a term
 
+fv :: Term -> [Unbound.Name Term]
+fv = Unbound.toListOf Unbound.fv
 
 -----------------
 

full/src/TypeCheck.hs

@@ -12,7 +12,7 @@ import Data.Maybe ( catMaybes )
 import Environment (D (..), TcMonad)
 import Environment qualified as Env
 import Equal qualified
-import PrettyPrint (Disp (disp))
+import PrettyPrint (Disp (disp), pp, debug)
 import Syntax
 import Debug.Trace
 
@@ -535,7 +535,7 @@ tcEntry (Def n term) = do
                   ]
            in do
                 Env.extendCtx (TypeSig sig) $ checkType term (sigType sig) `catchError` handler
-                if n `elem` Unbound.toListOf Unbound.fv term
+                if n `elem` fv term
                   then return $ AddCtx [TypeSig sig, RecDef n term]
                   else return $ AddCtx [TypeSig sig, Def n term]
     die term' =

main/pi/Hurkens.pi

@@ -1,26 +1,38 @@
 -- from Jonathan Chan
 module Hurkens where
 
-data Void : Type where {}
+Void : Type
+Void = (x:Type) -> x
+
 neg : Type -> Type
 neg = \X. X -> Void
+
 P : Type -> Type
 P = \S. S -> Type
+
 U : Type
 U = (x : Type) -> ((P (P x)) -> x) -> P (P x)
+
 tau : (P (P U)) -> U
 tau = \t. \x. \f. \p. t (\s. p (f (s x f)))
+
 sigma : U -> P (P U)
 sigma = \s. s U (\t. tau t)
+
 Delta : P U
 Delta = \y. neg ((p : P U) -> sigma y p -> p (tau (sigma y)))
+
 Omega : U
 Omega = tau (\p. (x : U) -> sigma x p -> p x)
+
 R : (p : P U) -> ((x : U) -> sigma x p -> p x) -> p Omega
 R = \zero. \one. one Omega (\x. one (tau (sigma x)))
+
 M : (x : U) -> sigma x Delta -> Delta x
 M = \x. \two. \three. three Delta two (\p. three (\y. p (tau (sigma y))))
+
 L : neg ((p : P U) -> ((x : U) -> sigma x p -> p x) -> p Omega)
 L = \zero. zero Delta M (\p. zero (\y. p (tau (sigma y))))
+
 false : Void
 false = L R

main/src/Equal.hs

@@ -254,8 +254,8 @@ unify ns tx ty = do
     then return []
     else case (txnf, tynf) of
       (Var x, Var y) | x == y -> return []
-      (Var y, yty) | y `notElem` ns -> return [Def y yty]
-      (yty, Var y) | y `notElem` ns -> return [Def y yty]
+      (Var y, yty) | y `notElem` ns && y `notElem` fv yty -> return [Def y yty]
+      (yty, Var y) | y `notElem` ns && y `notElem` fv yty -> return [Def y yty]
       (Prod a1 a2, Prod b1 b2) -> {- SOLN EP -} unifyArgs [Arg Rel a1, Arg Rel a2] [Arg Rel b1, Arg Rel b2] {- STUBWITH (++) <$> unify ns a1 b1 <*> unify ns a2 b2 -} 
 
 {- SOLN EQUAL -}

main/src/PrettyPrint.hs

@@ -1,7 +1,7 @@
 {- pi-forall language -}
 
 -- | A Pretty Printer.
-module PrettyPrint (Disp (..), D (..), SourcePos, PP.Doc, PP.render, pp) where
+module PrettyPrint (Disp (..), D (..), SourcePos, PP.Doc, PP.render, pp, debug) where
 
 import Control.Monad.Reader (MonadReader (ask, local), asks)
 import Data.Set qualified as S
@@ -71,7 +71,8 @@ initDI :: DispInfo
 initDI = DI {showAnnots = False,
                           dispAvoid = S.empty,
                           prec = 0,
-                          showLongNames = True}
+                          showLongNames = False
+                          }
 
 
 -------------------------------------------------------------------------
@@ -128,6 +129,8 @@ instance Disp Sig
 
 {- SOLN EP -}
 instance Disp Arg
+
+instance Disp [Arg]
 {- STUBWITH -}
 
 {- SOLN DATA -}
@@ -341,7 +344,14 @@ brackets :: Bool -> Doc -> Doc
 brackets b = if b then PP.brackets else id
 
 instance Display (Unbound.Name Term) where
-  display = return . disp
+  display n = do
+    b <- ask showLongNames
+    return (if b then debugDisp n else disp n)
+
+{- SOLN EP -}
+instance Display [Arg] where
+   display a = PP.sep <$> mapM display a
+{- STUBWITH -}
 
 instance Display Term where
   display TyType = return $ PP.text "Type"

main/src/Syntax.hs

@@ -10,6 +10,8 @@ import Data.Typeable (Typeable)
 import GHC.Generics (Generic,from)
 import Text.ParserCombinators.Parsec.Pos (SourcePos, initialPos, newPos)
 import Unbound.Generics.LocallyNameless qualified as Unbound
+import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound
+
 import Data.Function (on)
 
 -----------------------------------------
@@ -394,7 +396,11 @@ pi2 = TyPi {- SOLN EP -} Rel {- STUBWITH -}TyBool (Unbound.bind yName (Var yName
 -- True
 -- 
 
+---------------
+-- | Bridge function to calculate the free variables of a term
 
+fv :: Term -> [Unbound.Name Term]
+fv = Unbound.toListOf Unbound.fv
 
 -----------------
 

main/src/TypeCheck.hs

@@ -13,7 +13,7 @@ import Data.Maybe ( catMaybes )
 import Environment (D (..), TcMonad)
 import Environment qualified as Env
 import Equal qualified
-import PrettyPrint (Disp (disp))
+import PrettyPrint (Disp (disp), pp, debug)
 import Syntax
 import Debug.Trace
 
@@ -558,7 +558,7 @@ tcEntry (Def n term) = do
                   ]
            in do
                 Env.extendCtx (TypeSig sig) $ checkType term (sigType sig) `catchError` handler
-                if n `elem` Unbound.toListOf Unbound.fv term
+                if n `elem` fv term
                   then return $ AddCtx [TypeSig sig, RecDef n term]
                   else return $ AddCtx [TypeSig sig, Def n term]
     die term' =

version1/pi/Lec1.pi

@@ -2,10 +2,13 @@
 
 module Lec1 where
 
-id : (x:Type) -> x -> x
+ida : Type -> Type
+ida = \y . y
+
+id : (x:Type) -> ((y : x) -> x)
 id = \x y . y 
 
-idid : ((x:Type) -> (y : x) -> x) 
+idid : ((x:Type) ->  x -> x) 
 idid = id ((x:Type) -> (y : x) -> x) id
 
 compose : (A : Type) -> (B : Type) -> (C:Type) ->

version1/src/Equal.hs

@@ -140,8 +140,8 @@ unify ns tx ty = do
     then return []
     else case (txnf, tynf) of
       (Var x, Var y) | x == y -> return []
-      (Var y, yty) | y `notElem` ns -> return [Def y yty]
-      (yty, Var y) | y `notElem` ns -> return [Def y yty]
+      (Var y, yty) | y `notElem` ns && y `notElem` fv yty -> return [Def y yty]
+      (yty, Var y) | y `notElem` ns && y `notElem` fv yty -> return [Def y yty]
       (Prod a1 a2, Prod b1 b2) -> (++) <$> unify ns a1 b1 <*> unify ns a2 b2
       (Lam bnd1, Lam bnd2) -> do
         (x, b1, _, b2) <- Unbound.unbind2Plus bnd1 bnd2

version1/src/PrettyPrint.hs

@@ -1,7 +1,7 @@
 {- pi-forall language -}
 
 -- | A Pretty Printer.
-module PrettyPrint (Disp (..), D (..), SourcePos, PP.Doc, PP.render, pp) where
+module PrettyPrint (Disp (..), D (..), SourcePos, PP.Doc, PP.render, pp, debug) where
 
 import Control.Monad.Reader (MonadReader (ask, local), asks)
 import Data.Set qualified as S
@@ -71,7 +71,7 @@ initDI =
     { showAnnots = False,
       dispAvoid = S.empty,
       prec = 0,
-      showLongNames = True
+      showLongNames = False
     }
 
 -------------------------------------------------------------------------
@@ -286,7 +286,9 @@ brackets :: Bool -> Doc -> Doc
 brackets b = if b then PP.brackets else id
 
 instance Display (Unbound.Name Term) where
-  display = return . disp
+  display n = do
+    b <- ask showLongNames
+    return (if b then debugDisp n else disp n)
 
 instance Display Term where
   display TyType = return $ PP.text "Type"

version1/src/Syntax.hs

@@ -10,6 +10,7 @@ import Data.Typeable (Typeable)
 import GHC.Generics (Generic, from)
 import Text.ParserCombinators.Parsec.Pos (SourcePos, initialPos, newPos)
 import Unbound.Generics.LocallyNameless qualified as Unbound
+import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound
 
 -----------------------------------------
 
@@ -223,6 +224,12 @@ pi2 = TyPi TyBool (Unbound.bind yName (Var yName))
 -- True
 --
 
+---------------
+
+-- | Bridge function to calculate the free variables of a term
+fv :: Term -> [Unbound.Name Term]
+fv = Unbound.toListOf Unbound.fv
+
 -----------------
 
 -- * Source Positions

version1/src/TypeCheck.hs

@@ -9,7 +9,7 @@ import Debug.Trace
 import Environment (D (..), TcMonad)
 import Environment qualified as Env
 import Equal qualified
-import PrettyPrint (Disp (disp))
+import PrettyPrint (Disp (disp), debug, pp)
 import Syntax
 import Text.PrettyPrint.HughesPJ (render, ($$))
 import Unbound.Generics.LocallyNameless qualified as Unbound
@@ -186,7 +186,7 @@ tcEntry (Def n term) = do
                   ]
            in do
                 Env.extendCtx (TypeSig sig) $ checkType term (sigType sig) `catchError` handler
-                if n `elem` Unbound.toListOf Unbound.fv term
+                if n `elem` fv term
                   then return $ AddCtx [TypeSig sig, RecDef n term]
                   else return $ AddCtx [TypeSig sig, Def n term]
     die term' =

version2/src/Equal.hs

@@ -184,8 +184,8 @@ unify ns tx ty = do
     then return []
     else case (txnf, tynf) of
       (Var x, Var y) | x == y -> return []
-      (Var y, yty) | y `notElem` ns -> return [Def y yty]
-      (yty, Var y) | y `notElem` ns -> return [Def y yty]
+      (Var y, yty) | y `notElem` ns && y `notElem` fv yty -> return [Def y yty]
+      (yty, Var y) | y `notElem` ns && y `notElem` fv yty -> return [Def y yty]
       (Prod a1 a2, Prod b1 b2) -> (++) <$> unify ns a1 b1 <*> unify ns a2 b2 
 
       (TyEq a1 a2, TyEq b1 b2) -> (++) <$> unify ns a1 b1 <*> unify ns a2 b2