update to lts-21.25 to play nice with hls

README.md

@@ -34,11 +34,11 @@ History
 -------
 
 This is a revised version of lecture notes originally presented at OPLSS
-during 2022, 2014, and 2013.
+during 2023, 2022, 2014, and 2013.
 
 Videos from the [2022](https://www.cs.uoregon.edu/research/summerschool/summer22/topics.php) and [2014](https://www.cs.uoregon.edu/research/summerschool/summer14/curriculum.html) lectures are available from the
 OPLSS website. If you watch these videos, you should look at the
-corresponding branch of this repository.
+corresponding branch of this repository. Unfortunately, the [2023](https://www.cs.uoregon.edu/research/summerschool/summer23/topics.php) recordings include only audio, and only for part of the lectures.
 
 An abridged version of these lectures was also given at the Compose
 Conference, January 2015. [Notes](old/compose.md) from this version are also available.

full/stack.yaml

@@ -1,4 +1,4 @@
-resolver: lts-21.1
+resolver: lts-21.25
 
 # Local packages, usually specified by relative directory name
 packages:

main/stack.yaml

@@ -1,4 +1,4 @@
-resolver: lts-21.1
+resolver: lts-21.25
 
 # Local packages, usually specified by relative directory name
 packages:

version1/src/Syntax.hs

@@ -204,11 +204,9 @@ instance Unbound.Alpha Term where
 
 -- '(Bool : Type)' is alpha-equivalent to 'Bool'
 -- >>> aeq (Ann TyBool TyType) TyBool
--- True
 
 -- '(Bool, Bool:Type)' is alpha-equivalent to (Bool, Bool)
 -- >>> aeq (Prod TyBool (Ann TyBool TyType)) (Prod TyBool TyBool)
--- True
 
 -- At the same time, the generic operation equates terms that differ only
 -- in the names of bound variables.
@@ -230,7 +228,6 @@ idy :: Term
 idy = Lam (Unbound.bind yName (Var yName))
 
 -- >>> aeq idx idy
--- True
 
 ---------------
 
@@ -255,12 +252,6 @@ pi2 :: Term
 pi2 = TyPi TyBool (Unbound.bind yName (Var yName))
 
 -- >>> Unbound.aeq (Unbound.subst xName TyBool pi1) pi2
--- True
-
--- '(y : x) -> (y : Type) -> y'
-pi3 :: Term
-pi3 = TyPi (Var xName) (Unbound.bind yName 
-         (TyPi TyType (Unbound.bind yName (Var yName))))
 
 -----------------
 

version1/src/TypeCheck.hs

@@ -1,3 +1,6 @@
+{- pi-forall -}
+
+{-# HLINT ignore "Use forM_" #-}
 
 -- | The main routines for type-checking
 module TypeCheck (tcModules, inferType, checkType) where
@@ -25,29 +28,28 @@ inferType a = case a of
 
   -- i-type
   TyType -> return TyType
-
   -- i-pi
   (TyPi tyA bnd) -> do
-      (x, tyB) <- unbind bnd
-      --checkType tyA TyType
-      tcType tyA
-      Env.extendCtx (mkDecl x tyA) (checkType tyB TyType)
-      return TyType
+    (x, tyB) <- unbind bnd
+    tcType tyA
+    Env.extendCtx (mkDecl x tyA) (tcType tyB)
+    return TyType
 
   -- i-app
   (App a b) -> do
-      ty <- inferType a
-      case (strip ty) of 
-        TyPi tyA bnd -> do
-          checkType b tyA
-          return (instantiate bnd b)
-        _ -> Env.err [DS "application of non function", DD ty]
+    ty1 <- inferType a
+    let ty1' = strip ty1
+    case ty1' of
+      (TyPi tyA bnd) -> do
+        checkType b tyA
+        return (instantiate bnd b)
+      _ -> Env.err [DS "Expected a function type but found ", DD ty1]
 
   -- i-ann
-  (Ann a tyA) -> do 
-     tcType tyA
-     checkType a tyA
-     return tyA
+  (Ann a tyA) -> do
+    tcType tyA
+    checkType a tyA
+    return tyA
 
   -- Practicalities
   -- remember the current position in the type checking monad
@@ -85,8 +87,11 @@ checkType tm ty = do
     -- c-lam: check the type of a function
     (Lam bnd) -> case ty' of
       (TyPi tyA bnd2) -> do
-        (x, a, tyB) <- unbind2 bnd bnd2
-        Env.extendCtx (mkDecl x tyA) (checkType a tyB)
+        -- unbind the variables in the lambda expression and pi type
+        (x, body, tyB) <- unbind2 bnd bnd2
+
+        -- check the type of the body of the lambda expression
+        Env.extendCtx (mkDecl x tyA) (checkType body tyB)
       _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty']
     -- Practicalities
     (Pos p a) ->

version1/stack.yaml

@@ -1,4 +1,4 @@
-resolver: lts-21.1
+resolver: lts-21.25
 
 # Local packages, usually specified by relative directory name
 packages:

version2/stack.yaml

@@ -1,4 +1,4 @@
-resolver: lts-21.1
+resolver: lts-21.25
 
 # Local packages, usually specified by relative directory name
 packages:

version3/stack.yaml

@@ -1,4 +1,4 @@
-resolver: lts-21.1
+resolver: lts-21.25
 
 # Local packages, usually specified by relative directory name
 packages: