trying out new lightweight Automathy function syntax

examples/category.pg

@@ -25,8 +25,8 @@ section Category
     def × (A B C : Obj) (piA : C ~> A) (piB : C ~> B) :=
         forall (D : Obj) (f : D ~> A) (g : D ~> B),
             exists_uniq (D ~> C) (fun (fxg : D ~> C) =>
-                (eq (D ~> A) (comp D C A fxg piA) f)
+                eq (D ~> A) (comp D C A fxg piA) f
-                ∧ (eq (D ~> B) (comp D C B fxg piB) g));
+              ∧ eq (D ~> B) (comp D C B fxg piB) g);
 
     section Inverses
         variable
@@ -40,9 +40,7 @@ section Category
         def inv := inv_l ∧ inv_r;
     end Inverses
 
-    def ≅ (A B : Obj) :=
+    def ≅ (A B : Obj) := exists (A ~> B) (fun (f : A ~> B) => exists (B ~> A) (inv A B f));
-        exists (A ~> B) (fun (f : A ~> B) =>
-            exists (B ~> A) (inv A B f));
 
     infixl 20 ≅;
 

examples/logic.pg

@@ -13,7 +13,7 @@ def false_elim (A : ★) (contra : false) : A := contra A;
 
 def true : ★ := forall (A : ★), A → A;
 
-def true_intro : true := fun (A : ★) (x : A) => x;
+def true_intro : true := [A : ★][x : A] x;
 
 -- --------------------------------------------------------------------------------------------------------------
 
@@ -150,8 +150,8 @@ section Theorems
     -- ~(A ∨ B) => ~A ∧ ~B
     def de_morgan1 (h : not (A ∨ B)) : not A ∧ not B :=
         and_intro (not A) (not B)
-            (fun (a : A) => h (or_intro_l A B a))
+            ([a : A] h (or_intro_l A B a))
-            (fun (b : B) => h (or_intro_r A B b));
+            ([b : B] h (or_intro_r A B b));
 
     -- ~A ∧ ~B => ~(A ∨ B)
     def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) :=
@@ -178,8 +178,8 @@ section Theorems
     -- A ∨ B => B ∨ A
     def or_comm (h : A ∨ B) : B ∨ A :=
         or_elim A B (B ∨ A) h
-            (fun (a : A) => or_intro_r B A a)
+            ([a : A] or_intro_r B A a)
-            (fun (b : B) => or_intro_l B A b);
+            ([b : B] or_intro_l B A b);
 
     -- A ∧ (B ∧ C) => (A ∧ B) ∧ C
     def and_assoc_l (h : A ∧ (B ∧ C)) : (A ∧ B) ∧ C :=
@@ -240,7 +240,7 @@ section Theorems
     -- Thanks Quinn!
     -- A ∨ B => ~B => A
     def disj_syllog (nb : not B) (hor : A ∨ B) : A :=
-        or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);
+        or_elim A B A hor ([a : A] a) ([b : B] nb b A);
 
     -- (A => B) => ~B => ~A
     def contrapositive (f : A → B) (nb : not B) : not A :=

examples/peano.pg

@@ -478,7 +478,7 @@ def one_plus_one_two : one + one = two :=
 
 -- First, associativity, namely that n + (m + p) = (n + m) + p.
 def plus_assoc : forall (n m p : nat), n + (m + p) = n + m + p
-  := fun (n m : nat) =>
+  := [n m : nat]
   -- We prove this via induction on p for any fixed n and m.
   nat_ind
     (fun (p : nat) => n + (m + p) = n + m + p)
@@ -524,7 +524,7 @@ def plus_assoc : forall (n m p : nat), n + (m + p) = n + m + p
 -- First, we will show that 0 + n = n.
 def plus_0_l : forall (n : nat), zero + n = n :=
   -- We prove this by induction on n.
-  nat_ind (fun (n : nat) => zero + n = n)
+  nat_ind ([n : nat] zero + n = n)
     -- base case: WTS 0 + 0 = 0
     -- This is just plus_0_r 0
     (plus_0_r zero)
@@ -543,7 +543,7 @@ def plus_0_l : forall (n : nat), zero + n = n :=
 -- Next, we will show that (suc n) + m = suc (n + m).
 def plus_s_l (n : nat) : forall (m : nat), suc n + m = suc (n + m) :=
   -- We proceed by induction on m.
-  nat_ind (fun (m : nat) => suc n + m = suc (n + m))
+  nat_ind ([m : nat] suc n + m = suc (n + m))
     -- base case: (suc n) + 0 = suc (n + 0)
     -- suc n + 0 = suc n = suc (n + 0)
     (eq_trans nat (suc n + zero) (suc n) (suc (n + zero))
@@ -579,7 +579,7 @@ def plus_s_l (n : nat) : forall (m : nat), suc n + m = suc (n + m) :=
 -- Finally, we can prove commutativity.
 def plus_comm (n : nat) : forall (m : nat), n + m = m + n :=
   -- As usual, we proceed by induction.
-  nat_ind (fun (m : nat) => n + m = m + n)
+  nat_ind ([m : nat] n + m = m + n)
 
   -- Base case: WTS n + 0 = 0 + n
   -- n + 0 = n = 0 + n

lib/Check.hs

@@ -13,7 +13,7 @@ type Context = [Expr]
 matchPi :: Expr -> Expr -> ReaderT Env Result (Expr, Expr)
 matchPi x mt =
     whnf mt >>= \case
-        (Pi _ a _ b) -> pure (a, b)
+        (Pi _ a b) -> pure (a, b)
         t -> throwError $ ExpectedPiType x t
 
 findLevel :: Context -> Expr -> ReaderT Env Result Integer
@@ -57,16 +57,14 @@ findType g e@(App m n) = do
     a' <- findType g n
     betaEquiv' e a a'
     pure $ subst 0 n b
-findType g f@(Abs x a asc m) = do
+findType g (Abs x a m) = do
     validateType g a
     b <- findType (incIndices a : map incIndices g) m
-    whenJust asc (void . liftA2 ($>) (findType g) (betaEquiv' f b))
+    validateType g (Pi x a b)
-    validateType g (Pi x a Nothing b)
+    pure $ if occursFree 0 b then Pi x a b else Pi "" a b
-    pure $ if occursFree 0 b then Pi x a Nothing b else Pi "" a Nothing b
+findType g (Pi _ a b) = do
-findType g f@(Pi _ a asc b) = do
     aSort <- findType g a
     bSort <- findType (incIndices a : map incIndices g) b
-    whenJust asc (void . liftA2 ($>) (findType g) (betaEquiv' f bSort))
     liftEither $ compSort a b aSort bSort
 findType g (Let _ Nothing v b) = findType g (subst 0 v b)
 findType g e@(Let _ (Just t) v b) = do

lib/Elaborator.hs

@@ -102,16 +102,14 @@ usedVars (I.Var name) = do
 usedVars I.Star = pure S.empty
 usedVars (I.Level _) = pure S.empty
 usedVars (I.App m n) = S.union <$> usedVars m <*> usedVars n
-usedVars (I.Abs name ty ascr body) = saveState $ do
+usedVars (I.Abs name ty body) = saveState $ do
     ty' <- usedVars ty
-    ascr' <- traverse usedVars ascr
     removeName name
-    S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
+    S.union ty' <$> usedVars body
-usedVars (I.Pi name ty ascr body) = saveState $ do
+usedVars (I.Pi name ty body) = saveState $ do
     ty' <- usedVars ty
-    ascr' <- traverse usedVars ascr
     removeName name
-    S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
+    S.union ty' <$> usedVars body
 usedVars (I.Let name ascr value body) = saveState $ do
     ty' <- usedVars value
     ascr' <- traverse usedVars ascr
@@ -129,16 +127,14 @@ traverseBody (I.Var name) = do
 traverseBody I.Star = pure I.Star
 traverseBody (I.Level k) = pure $ I.Level k
 traverseBody (I.App m n) = I.App <$> traverseBody m <*> traverseBody n
-traverseBody (I.Abs name ty ascr body) = saveState $ do
+traverseBody (I.Abs name ty body) = saveState $ do
     ty' <- traverseBody ty
-    ascr' <- traverse traverseBody ascr
     removeName name
-    I.Abs name ty' ascr' <$> traverseBody body
+    I.Abs name ty' <$> traverseBody body
-traverseBody (I.Pi name ty ascr body) = saveState $ do
+traverseBody (I.Pi name ty body) = saveState $ do
     ty' <- traverseBody ty
-    ascr' <- traverse traverseBody ascr
     removeName name
-    I.Pi name ty' ascr' <$> traverseBody body
+    I.Pi name ty' <$> traverseBody body
 traverseBody (I.Let name ascr value body) = saveState $ do
     ascr' <- traverse traverseBody ascr
     value' <- traverseBody value
@@ -146,10 +142,10 @@ traverseBody (I.Let name ascr value body) = saveState $ do
     I.Let name ascr' value' <$> traverseBody body
 
 mkPi :: (Text, IRExpr) -> IRExpr -> IRExpr
-mkPi (param, typ) = I.Pi param typ Nothing
+mkPi (param, typ) = I.Pi param typ
 
 mkAbs :: (Text, IRExpr) -> IRExpr -> IRExpr
-mkAbs (param, typ) = I.Abs param typ Nothing
+mkAbs (param, typ) = I.Abs param typ
 
 generalizeType :: IRExpr -> [(Text, IRExpr)] -> IRExpr
 generalizeType = foldr mkPi
@@ -190,16 +186,14 @@ elaborate ir = evalState (elaborate' ir) []
     elaborate' I.Star = pure E.Star
     elaborate' (I.Level level) = pure $ E.Level level
     elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
-    elaborate' (I.Abs x t a b) = saveBinders $ do
+    elaborate' (I.Abs x t b) = saveBinders $ do
         t' <- elaborate' t
-        a' <- traverse elaborate' a
         modify (x :)
-        E.Abs x t' a' <$> elaborate' b
+        E.Abs x t' <$> elaborate' b
-    elaborate' (I.Pi x t a b) = saveBinders $ do
+    elaborate' (I.Pi x t b) = saveBinders $ do
         t' <- elaborate' t
-        a' <- traverse elaborate' a
         modify (x :)
-        E.Pi x t' a' <$> elaborate' b
+        E.Pi x t' <$> elaborate' b
     elaborate' (I.Let name Nothing val body) = saveBinders $ do
         val' <- elaborate' val
         modify (name :)

lib/Eval.hs

@@ -42,8 +42,8 @@ subst _ _ (Axiom s) = Axiom s
 subst _ _ Star = Star
 subst _ _ (Level i) = Level i
 subst k s (App m n) = App (subst k s m) (subst k s n)
-subst k s (Abs x m a n) = Abs x (subst k s m) a (subst (k + 1) (incIndices s) n)
+subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
-subst k s (Pi x m a n) = Pi x (subst k s m) a (subst (k + 1) (incIndices s) n)
+subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Let x t v b) = Let x t (subst k s v) (subst (k + 1) (incIndices s) b)
 
 envLookupVal :: Text -> ReaderT Env Result Expr
@@ -53,10 +53,10 @@ envLookupTy :: Text -> ReaderT Env Result Expr
 envLookupTy n = asks ((_ty <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
 
 reduce :: Expr -> ReaderT Env Result Expr
-reduce (App (Abs _ _ _ v) n) = pure $ subst 0 n v
+reduce (App (Abs _ _ v) n) = pure $ subst 0 n v
 reduce (App m n) = App <$> reduce m <*> reduce n
-reduce (Abs x t a v) = Abs x <$> reduce t <*> pure a <*> reduce v
+reduce (Abs x t v) = Abs x <$> reduce t <*> reduce v
-reduce (Pi x t a v) = Pi x <$> reduce t <*> pure a <*> reduce v
+reduce (Pi x t v) = Pi x <$> reduce t <*> reduce v
 reduce (Free n) = envLookupVal n
 reduce (Let _ _ v b) = pure $ subst 0 v b
 reduce e = pure e
@@ -70,7 +70,7 @@ normalize e = do
 
 -- reduce until β reducts or let simplifications are impossible in head position
 whnf :: Expr -> ReaderT Env Result Expr
-whnf (App (Abs _ _ _ v) n) = whnf $ subst 0 n v
+whnf (App (Abs _ _ v) n) = whnf $ subst 0 n v
 whnf (App m n) = do
     m' <- whnf m
     if m == m'
@@ -95,8 +95,8 @@ betaEquiv e1 e2
             (Star, Star) -> pure True
             (Level i, Level j) -> pure $ i == j
             (App m1 n1, App m2 n2) -> (&&) <$> betaEquiv m1 m2 <*> betaEquiv n1 n2
-            (Abs _ t1 _ v1, Abs _ t2 _ v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
+            (Abs _ t1 v1, Abs _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
-            (Pi _ t1 _ v1, Pi _ t2 _ v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
+            (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
             (Let _ _ v b, e) -> betaEquiv (subst 0 v b) e
             (e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
             _ -> pure False -- remaining cases impossible, false, or redundant

lib/Expr.hs

@@ -12,8 +12,8 @@ data Expr where
     Star :: Expr
     Level :: Integer -> Expr
     App :: Expr -> Expr -> Expr
-    Abs :: Text -> Expr -> Maybe Expr -> Expr -> Expr
+    Abs :: Text -> Expr -> Expr -> Expr
-    Pi :: Text -> Expr -> Maybe Expr -> Expr -> Expr
+    Pi :: Text -> Expr -> Expr -> Expr
     Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr
     deriving (Show, Ord)
 
@@ -27,8 +27,8 @@ instance Eq Expr where
     Star == Star = True
     (Level i) == (Level j) = i == j
     (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2
-    (Abs _ t1 _ b1) == (Abs _ t2 _ b2) = t1 == t2 && b1 == b2
+    (Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2
-    (Pi _ t1 _ b1) == (Pi _ t2 _ b2) = t1 == t2 && b1 == b2
+    (Pi _ t1 b1) == (Pi _ t2 b2) = t1 == t2 && b1 == b2
     (Let _ _ v1 b1) == (Let _ _ v2 b2) = v1 == v2 && b1 == b2
     _ == _ = False
 
@@ -39,8 +39,8 @@ occursFree _ (Axiom _) = False
 occursFree _ Star = False
 occursFree _ (Level _) = False
 occursFree n (App a b) = on (||) (occursFree n) a b
-occursFree n (Abs _ a _ b) = occursFree n a || occursFree (n + 1) b
+occursFree n (Abs _ a b) = occursFree n a || occursFree (n + 1) b
-occursFree n (Pi _ a _ b) = occursFree n a || occursFree (n + 1) b
+occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b
 occursFree n (Let _ _ v b) = occursFree n v || occursFree (n + 1) b
 
 shiftIndices :: Integer -> Integer -> Expr -> Expr
@@ -52,8 +52,8 @@ shiftIndices _ _ (Axiom s) = Axiom s
 shiftIndices _ _ Star = Star
 shiftIndices _ _ (Level i) = Level i
 shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
-shiftIndices d c (Abs x m a n) = Abs x (shiftIndices d c m) a (shiftIndices d (c + 1) n)
+shiftIndices d c (Abs x m n) = Abs x (shiftIndices d c m) (shiftIndices d (c + 1) n)
-shiftIndices d c (Pi x m a n) = Pi x (shiftIndices d c m) a (shiftIndices d (c + 1) n)
+shiftIndices d c (Pi x m n) = Pi x (shiftIndices d c m) (shiftIndices d (c + 1) n)
 shiftIndices d c (Let x t v b) = Let x t (shiftIndices d c v) (shiftIndices d (c + 1) b)
 
 incIndices :: Expr -> Expr
@@ -79,8 +79,8 @@ dedupNames = go []
     go :: [Text] -> Expr -> Expr
     go bs (Var x k) = Var (varName bs x (fromIntegral k)) k
     go bs (App m n) = App (go bs m) (go bs n)
-    go bs (Abs x ty ascr b) = Abs (varName (x : bs) x 0) (go bs ty) (go bs <$> ascr) (go (x : bs) b)
+    go bs (Abs x ty b) = Abs (varName (x : bs) x 0) (go bs ty) (go (x : bs) b)
-    go bs (Pi x ty ascr b) = Pi (varName (x : bs) x 0) (go bs ty) (go bs <$> ascr) (go (x : bs) b)
+    go bs (Pi x ty b) = Pi (varName (x : bs) x 0) (go bs ty) (go (x : bs) b)
     go bs (Let x ascr val b) = Let (varName (x : bs) x 0) (go bs <$> ascr) (go bs val) (go (x : bs) b)
     go _ e = e
 
@@ -99,7 +99,7 @@ instance Pretty Binding where
     pretty (Binding var params body) = group $ parens $ pretty var <+> align (sep (map pretty params)) <+> ":=" <+> pretty body
 
 collectLambdas :: Expr -> ([Param], Expr)
-collectLambdas (Abs x ty _ body) = (Param x ty : params, final)
+collectLambdas (Abs x ty body) = (Param x ty : params, final)
   where
     (params, final) = collectLambdas body
 collectLambdas e = ([], e)
@@ -113,14 +113,14 @@ collectLets (Let x _ val body) = (Binding x params' val' : bindings, final)
 collectLets e = ([], e)
 
 collectPis :: Expr -> ([Param], Expr)
-collectPis p@(Pi "" _ _ _) = ([], p)
+collectPis p@(Pi "" _ _) = ([], p)
-collectPis (Pi x ty _ body) = (Param x ty : params, final)
+collectPis (Pi x ty body) = (Param x ty : params, final)
   where
     (params, final) = collectPis body
 collectPis e = ([], e)
 
 collectArrows :: Expr -> NonEmpty Expr
-collectArrows (Pi "" t1 _ t2) = t1 :| toList rest
+collectArrows (Pi "" t1 t2) = t1 :| toList rest
   where
     rest = collectArrows t2
 collectArrows e = pure e
@@ -133,10 +133,10 @@ collectApps e = pure e
 
 cleanNames :: Expr -> Expr
 cleanNames (App m n) = App (cleanNames m) (cleanNames n)
-cleanNames (Abs x ty a body) = Abs x (cleanNames ty) a (cleanNames body)
+cleanNames (Abs x ty body) = Abs x (cleanNames ty) (cleanNames body)
-cleanNames (Pi x ty a body)
+cleanNames (Pi x ty body)
-    | occursFree 0 body = Pi x (cleanNames ty) a (cleanNames body)
+    | occursFree 0 body = Pi x (cleanNames ty) (cleanNames body)
-    | otherwise = Pi "" ty a (cleanNames body)
+    | otherwise = Pi "" ty (cleanNames body)
 cleanNames e = e
 
 groupParams :: [Param] -> [ParamGroup]
@@ -178,7 +178,7 @@ prettyExpr k expr = case expr of
       where
         (top :| rest) = NE.reverse $ collectApps expr
         application = group $ hang 4 $ prettyExpr 3 top <> line <> align (sep $ map (prettyExpr 4) rest)
-    Pi "" _ _ _
+    Pi "" _ _
         | k > 2 -> parens piType
         | otherwise -> piType
       where

lib/IR.hs

@@ -13,13 +13,11 @@ data IRExpr
     | Abs
         { absParamName :: Text
         , absParamType :: IRExpr
-        , absAscription :: Maybe IRExpr
         , absBody :: IRExpr
         }
     | Pi
         { piParamName :: Text
         , piParamType :: IRExpr
-        , piAscription :: Maybe IRExpr
         , piBody :: IRExpr
         }
     | Let

lib/Parser.hs

@@ -10,7 +10,7 @@ import qualified Data.Text as T
 import Errors (Error (..))
 import IR
 import Preprocessor
-import Text.Megaparsec (MonadParsec (..), ParsecT, ShowErrorComponent (..), choice, errorBundlePretty, label, runParserT, try, between)
+import Text.Megaparsec (MonadParsec (..), ParsecT, ShowErrorComponent (..), between, choice, errorBundlePretty, label, runParserT, try)
 import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
 
@@ -79,29 +79,37 @@ pSomeParams ident = lexeme $ concat <$> some (pParamGroup ident)
 pManyParams :: Parser Text -> Parser [Param]
 pManyParams ident = lexeme $ concat <$> many (pParamGroup ident)
 
-mkAbs :: Maybe IRExpr -> (Text, IRExpr) -> IRExpr -> IRExpr
+mkAbs :: (Text, IRExpr) -> IRExpr -> IRExpr
-mkAbs ascription (param, typ) = Abs param typ ascription
+mkAbs (param, typ) = Abs param typ
 
-mkPi :: Maybe IRExpr -> (Text, IRExpr) -> IRExpr -> IRExpr
+mkPi :: (Text, IRExpr) -> IRExpr -> IRExpr
-mkPi ascription (param, typ) = Pi param typ ascription
+mkPi (param, typ) = Pi param typ
 
 pLAbs :: Parser IRExpr
 pLAbs = lexeme $ label "λ-abstraction" $ do
     _ <- pKeyword "fun" <|> symbol "λ"
     params <- pSomeParams pIdentifier
-    ascription <- optional pAscription
     _ <- symbol "=>" <|> symbol "⇒"
     body <- pIRExpr
-    pure $ foldr (mkAbs ascription) body params
+    pure $ foldr mkAbs body params
+
+pALAbs :: Parser IRExpr
+pALAbs = lexeme $ label "λ-abstraction" $ do
+    _ <- symbol "["
+    args <- some pIdentifier
+    _ <- symbol ":"
+    typ <- pIRExpr
+    _ <- symbol "]"
+    body <- pIRExpr
+    pure $ foldr (mkAbs . (,typ)) body args
 
 pPAbs :: Parser IRExpr
 pPAbs = lexeme $ label "Π-abstraction" $ do
     _ <- pKeyword "forall" <|> symbol "∏" <|> symbol "∀"
     params <- pSomeParams pIdentifier
-    ascription <- optional pAscription
     symbol ","
     body <- pIRExpr
-    pure $ foldr (mkPi ascription) body params
+    pure $ foldr mkPi body params
 
 pBinding :: Parser (Text, Maybe IRExpr, IRExpr)
 pBinding = lexeme $ label "binding" $ do
@@ -114,8 +122,8 @@ pBinding = lexeme $ label "binding" $ do
     symbol ")"
     pure
         ( ident
-        , flip (foldr (mkPi Nothing)) params <$> ascription
+        , flip (foldr mkPi) params <$> ascription
-        , foldr (mkAbs Nothing) value params
+        , foldr mkAbs value params
         )
 
 pLet :: Parser IRExpr
@@ -190,12 +198,12 @@ pInfix = parseWithPrec 0
             Nothing -> fail $ "unknown operator '" ++ toString op ++ "'"
 
 pAppTerm :: Parser IRExpr
-pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pInfix]
+pAppTerm = lexeme $ choice [pLAbs, pALAbs, pPAbs, pLet, pInfix]
 
 pIRExpr :: Parser IRExpr
 pIRExpr = lexeme $ do
     e <- pAppTerm
-    option e $ (symbol "->" <|> symbol "→") >> Pi "" e Nothing <$> pIRExpr
+    option e $ (symbol "->" <|> symbol "→") >> Pi "" e <$> pIRExpr
 
 pAscription :: Parser IRExpr
 pAscription = lexeme $ try $ symbol ":" >> label "type" pIRExpr
@@ -205,7 +213,7 @@ pAxiom = lexeme $ label "axiom" $ do
     pKeyword "axiom"
     ident <- pIdentifier
     params <- pManyParams (pIdentifier <|> pSymbol)
-    ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription
+    ascription <- fmap (flip (foldr mkPi) params) pAscription
     symbol ";"
     pure $ Axiom ident ascription
 
@@ -221,11 +229,11 @@ pDef = lexeme $ label "definition" $ do
     pKeyword "def"
     ident <- pIdentifier <|> pSymbol
     params <- pManyParams pIdentifier
-    ascription <- fmap (flip (foldr (mkPi Nothing)) params) <$> optional pAscription
+    ascription <- fmap (flip (foldr mkPi) params) <$> optional pAscription
     symbol ":="
     body <- pIRExpr
     symbol ";"
-    pure $ Def ident ascription $ foldr (mkAbs Nothing) body params
+    pure $ Def ident ascription $ foldr mkAbs body params
 
 pFixityDec :: Parser ()
 pFixityDec = do