From 095151216b12dbd9f10e2ea81f05d6e76f1266f1 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Mon, 17 Jun 2024 15:58:56 +0300
Subject: [PATCH 1/2] Extend TH support to parametrised term/scope/pattern
 types

---
 haskell/free-foil/free-foil.cabal             |   1 +
 .../src/Control/Monad/Foil/TH/MkFoilData.hs   |  57 ++++---
 .../src/Control/Monad/Foil/TH/MkFromFoil.hs   |  52 ++++---
 .../Control/Monad/Foil/TH/MkInstancesFoil.hs  |  17 ++-
 .../src/Control/Monad/Foil/TH/MkToFoil.hs     | 118 +++++++++------
 .../src/Control/Monad/Foil/TH/Util.hs         |  26 ++++
 haskell/lambda-pi/Setup.hs                    |   2 +-
 .../src/Language/LambdaPi/Impl/Foil.hs        |  58 ++++----
 .../src/Language/LambdaPi/Impl/FoilTH.hs      |  76 +++++-----
 .../src/Language/LambdaPi/Impl/FreeFoil.hs    |  56 +++----
 .../src/Language/LambdaPi/Syntax/Abs.hs       | 115 ++++++++++----
 .../src/Language/LambdaPi/Syntax/Par.hs       | 130 +++++++++-------
 .../src/Language/LambdaPi/Syntax/Par.y        | 140 +++++++++++-------
 .../src/Language/LambdaPi/Syntax/Print.hs     |  46 +++---
 .../src/Language/LambdaPi/Syntax/Skel.hs      |  44 +++---
 15 files changed, 566 insertions(+), 372 deletions(-)
 create mode 100644 haskell/free-foil/src/Control/Monad/Foil/TH/Util.hs

diff --git a/haskell/free-foil/free-foil.cabal b/haskell/free-foil/free-foil.cabal
index 3d7be268..f3ff255c 100644
--- a/haskell/free-foil/free-foil.cabal
+++ b/haskell/free-foil/free-foil.cabal
@@ -36,6 +36,7 @@ library
       Control.Monad.Foil.TH.MkFromFoil
       Control.Monad.Foil.TH.MkInstancesFoil
       Control.Monad.Foil.TH.MkToFoil
+      Control.Monad.Foil.TH.Util
       Control.Monad.Free.Foil
       Control.Monad.Free.Foil.Example
   other-modules:
diff --git a/haskell/free-foil/src/Control/Monad/Foil/TH/MkFoilData.hs b/haskell/free-foil/src/Control/Monad/Foil/TH/MkFoilData.hs
index cacd3878..3cc713dc 100644
--- a/haskell/free-foil/src/Control/Monad/Foil/TH/MkFoilData.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil/TH/MkFoilData.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE LambdaCase            #-}
 {-# LANGUAGE QuasiQuotes           #-}
 {-# LANGUAGE TemplateHaskellQuotes #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
@@ -9,6 +8,7 @@ module Control.Monad.Foil.TH.MkFoilData (mkFoilData) where
 import           Language.Haskell.TH
 
 import qualified Control.Monad.Foil.Internal as Foil
+import Control.Monad.Foil.TH.Util
 
 -- | Generate scope-safe variants given names of types for the raw representation.
 mkFoilData
@@ -20,20 +20,18 @@ mkFoilData
 mkFoilData termT nameT scopeT patternT = do
   n <- newName "n"
   l <- newName "l"
-  TyConI (DataD _ctx _name _tvars _kind patternCons _deriv) <- reify patternT
-  TyConI (DataD _ctx _name _tvars _kind scopeCons _deriv) <- reify scopeT
-  TyConI (DataD _ctx _name _tvars _kind termCons _deriv) <- reify termT
+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT
+  TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT
+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT
 
-  foilPatternCons <- mapM (toPatternCon n) patternCons
-  let foilScopeCons = map (toScopeCon n) scopeCons
-  let foilTermCons = map (toTermCon n l) termCons
+  foilPatternCons <- mapM (toPatternCon patternTVars n) patternCons
+  let foilScopeCons = map (toScopeCon scopeTVars n) scopeCons
+  let foilTermCons = map (toTermCon termTVars n l) termCons
 
   return
-    [ DataD [] foilTermT [PlainTV n ()] Nothing foilTermCons []
-    , StandaloneDerivD Nothing [] (AppT (ConT ''Show) (AppT (ConT foilTermT) (VarT n)))
-    , DataD [] foilScopeT [PlainTV n ()] Nothing foilScopeCons [DerivClause Nothing [ConT ''Show]]
-    , DataD [] foilPatternT [PlainTV n (), PlainTV l ()] Nothing foilPatternCons []
-    , StandaloneDerivD Nothing [] (AppT (ConT ''Show) (AppT (AppT (ConT foilPatternT) (VarT n)) (VarT l)))
+    [ DataD [] foilTermT (termTVars ++ [KindedTV n () (PromotedT ''Foil.S)]) Nothing foilTermCons []
+    , DataD [] foilScopeT (scopeTVars ++ [KindedTV n () (PromotedT ''Foil.S)]) Nothing foilScopeCons []
+    , DataD [] foilPatternT (patternTVars ++ [KindedTV n () (PromotedT ''Foil.S), KindedTV l () (PromotedT ''Foil.S)]) Nothing foilPatternCons []
     ]
   where
     foilTermT = mkName ("Foil" ++ nameBase termT)
@@ -43,13 +41,14 @@ mkFoilData termT nameT scopeT patternT = do
     -- | Convert a constructor declaration for a raw pattern type
     -- into a constructor for the scope-safe pattern type.
     toPatternCon
-      :: Name   -- ^ Name for the starting scope type variable.
+      :: [TyVarBndr ()]
+      -> Name   -- ^ Name for the starting scope type variable.
       -> Con    -- ^ Raw pattern constructor.
       -> Q Con
-    toPatternCon n (NormalC conName params) = do
+    toPatternCon tvars n (NormalC conName params) = do
       (lastScopeName, foilParams) <- toPatternConParams 1 n params
       let foilConName = mkName ("Foil" ++ nameBase conName)
-      return (GadtC [foilConName] foilParams (AppT (AppT (ConT foilPatternT) (VarT n)) (VarT lastScopeName)))
+      return (GadtC [foilConName] foilParams (PeelConT foilPatternT (map (VarT . tvarName) tvars ++ [VarT n, VarT lastScopeName])))
       where
         -- | Process type parameters of a pattern,
         -- introducing (existential) type variables for the intermediate scopes,
@@ -64,16 +63,16 @@ mkFoilData termT nameT scopeT patternT = do
           case type_ of
             -- if the current component is a variable identifier
             -- then treat it as a single name binder (see 'Foil.NameBinder')
-            ConT tyName | tyName == nameT -> do
+            PeelConT tyName _tyParams | tyName == nameT -> do
               l <- newName ("n" <> show i)
               let type' = AppT (AppT (ConT ''Foil.NameBinder) (VarT p)) (VarT l)
               (l', conParams') <- toPatternConParams (i+1) l conParams
               return (l', (bang_, type') : conParams')
             -- if the current component is a raw pattern
             -- then convert it into a scope-safe pattern
-            ConT tyName | tyName == patternT -> do
+            PeelConT tyName tyParams | tyName == patternT -> do
               l <- newName ("n" <> show i)
-              let type' = AppT (AppT (ConT foilPatternT) (VarT p)) (VarT l)
+              let type' = PeelConT foilPatternT (tyParams ++ [VarT p, VarT l])
               (l', conParams') <- toPatternConParams (i+1) l conParams
               return (l', (bang_, type') : conParams')
             -- otherwise, ignore the component as non-binding
@@ -83,26 +82,26 @@ mkFoilData termT nameT scopeT patternT = do
 
     -- | Convert a constructor declaration for a raw scoped term
     -- into a constructor for the scope-safe scoped term.
-    toScopeCon :: Name -> Con -> Con
-    toScopeCon n (NormalC conName params) =
+    toScopeCon :: [TyVarBndr ()] -> Name -> Con -> Con
+    toScopeCon _tvars n (NormalC conName params) =
       NormalC foilConName (map toScopeParam params)
       where
         foilConName = mkName ("Foil" ++ nameBase conName)
-        toScopeParam (_bang, ConT tyName)
-          | tyName == termT = (_bang, AppT (ConT foilTermT) (VarT n))
+        toScopeParam (_bang, PeelConT tyName tyParams)
+          | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n]))
         toScopeParam _bangType = _bangType
 
     -- | Convert a constructor declaration for a raw term
     -- into a constructor for the scope-safe term.
-    toTermCon :: Name -> Name -> Con -> Con
-    toTermCon n l (NormalC conName params) =
-      GadtC [foilConName] (map toTermParam params) (AppT (ConT foilTermT) (VarT n))
+    toTermCon :: [TyVarBndr ()] -> Name -> Name -> Con -> Con
+    toTermCon tvars n l (NormalC conName params) =
+      GadtC [foilConName] (map toTermParam params) (PeelConT foilTermT (map (VarT . tvarName) tvars ++ [VarT n]))
       where
         foilNames = [n, l]
         foilConName = mkName ("Foil" ++ nameBase conName)
-        toTermParam (_bang, ConT tyName)
-          | tyName == patternT = (_bang, foldl AppT (ConT foilPatternT) (map VarT foilNames))
+        toTermParam (_bang, PeelConT tyName tyParams)
+          | tyName == patternT = (_bang, PeelConT foilPatternT (tyParams ++ map VarT foilNames))
           | tyName == nameT = (_bang, AppT (ConT ''Foil.Name) (VarT n))
-          | tyName == scopeT = (_bang, AppT (ConT foilScopeT) (VarT l))
-          | tyName == termT = (_bang, AppT (ConT foilTermT) (VarT n))
+          | tyName == scopeT = (_bang, PeelConT foilScopeT (tyParams ++ [VarT l]))
+          | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n]))
         toTermParam _bangType = _bangType
diff --git a/haskell/free-foil/src/Control/Monad/Foil/TH/MkFromFoil.hs b/haskell/free-foil/src/Control/Monad/Foil/TH/MkFromFoil.hs
index a9015a81..0362b57c 100644
--- a/haskell/free-foil/src/Control/Monad/Foil/TH/MkFromFoil.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil/TH/MkFromFoil.hs
@@ -10,6 +10,7 @@ import           Language.Haskell.TH
 import Language.Haskell.TH.Syntax (addModFinalizer)
 
 import qualified Control.Monad.Foil  as Foil
+import Control.Monad.Foil.TH.Util
 
 -- | Generate conversion functions from raw to scope-safe representation.
 mkFromFoil
@@ -19,34 +20,41 @@ mkFromFoil
   -> Name -- ^ Type name for raw patterns.
   -> Q [Dec]
 mkFromFoil termT nameT scopeT patternT = do
-  TyConI (DataD _ctx _name _tvars _kind patternCons _deriv) <- reify patternT
-  TyConI (DataD _ctx _name _tvars _kind scopeCons _deriv) <- reify scopeT
-  TyConI (DataD _ctx _name _tvars _kind termCons _deriv) <- reify termT
+  n <- newName "n"
+  let ntype = return (VarT n)
+  l <- newName "l"
+  let ltype = return (VarT l)
+  r <- newName "r"
+  let rtype = return (VarT r)
+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT
+  TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT
+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT
+
+  let termParams = map (VarT . tvarName) termTVars
+  let scopeParams = map (VarT . tvarName) scopeTVars
+  let patternParams = map (VarT . tvarName) patternTVars
 
   fromFoilTermSignature <-
     SigD fromFoilTermT <$>
-      [t| forall n.
-          [$(return (ConT nameT))]
-          -> Foil.NameMap n $(return (ConT nameT))
-          -> $(return (ConT foilTermT)) n
-          -> $(return (ConT termT))
+      [t| [$(return (ConT nameT))]
+          -> Foil.NameMap $ntype $(return (ConT nameT))
+          -> $(return (PeelConT foilTermT termParams)) $ntype
+          -> $(return (PeelConT termT termParams))
         |]
   fromFoilScopedSignature <-
     SigD fromFoilScopedT <$>
-      [t| forall n.
-          [$(return (ConT nameT))]
-          -> Foil.NameMap n $(return (ConT nameT))
-          -> $(return (ConT foilScopeT)) n
-          -> $(return (ConT scopeT))
+      [t| [$(return (ConT nameT))]
+          -> Foil.NameMap $ntype $(return (ConT nameT))
+          -> $(return (PeelConT foilScopeT scopeParams)) $ntype
+          -> $(return (PeelConT scopeT scopeParams))
         |]
   fromFoilPatternSignature <-
     SigD fromFoilPatternT <$>
-      [t| forall n l r.
-          [$(return (ConT nameT))]
-          -> Foil.NameMap n $(return (ConT nameT))
-          -> $(return (ConT foilPatternT)) n l
-          -> ([$(return (ConT nameT))] -> Foil.NameMap l $(return (ConT nameT)) -> $(return (ConT patternT)) -> r)
-          -> r
+      [t| [$(return (ConT nameT))]
+          -> Foil.NameMap $ntype $(return (ConT nameT))
+          -> $(return (PeelConT foilPatternT patternParams)) $ntype $ltype
+          -> ([$(return (ConT nameT))] -> Foil.NameMap $ltype $(return (ConT nameT)) -> $(return (PeelConT patternT patternParams)) -> $rtype)
+          -> $rtype
         |]
 
   addModFinalizer $ putDoc (DeclDoc fromFoilTermT)
@@ -86,7 +94,7 @@ mkFromFoil termT nameT scopeT patternT = do
             conMatchBody = go 1 (VarE freshVars) (VarE env) (ConE conName) params
 
             go _i _freshVars' _env' p [] = p
-            go i freshVars' env' p ((_bang, ConT tyName) : conParams)
+            go i freshVars' env' p ((_bang, PeelConT tyName _tyParams) : conParams)
               | tyName == nameT =
                   go (i+1) freshVars' env' (AppE p (AppE (AppE (VarE 'Foil.lookupName) (VarE xi)) env')) conParams
               | tyName == termT =
@@ -135,7 +143,7 @@ mkFromFoil termT nameT scopeT patternT = do
             conMatchBody = go 1 (VarE freshVars) (VarE env) (ConE conName) params
 
             go _i freshVars' env' p [] = AppE (AppE (AppE (VarE cont) freshVars') env') p
-            go i freshVars' env' p ((_bang, ConT tyName) : conParams)
+            go i freshVars' env' p ((_bang, PeelConT tyName _tyParams) : conParams)
               | tyName == nameT =
                   CaseE freshVars'
                     [ Match (ListP []) (NormalB (AppE (VarE 'error) (LitE (StringL "not enough fresh variables")))) []
@@ -188,7 +196,7 @@ mkFromFoil termT nameT scopeT patternT = do
             conMatchBody = go 1 (VarE freshVars) (VarE env) (ConE conName) params
 
             go _i _freshVars' _env' p [] = p
-            go i freshVars' env' p ((_bang, ConT tyName) : conParams)
+            go i freshVars' env' p ((_bang, PeelConT tyName _tyParams) : conParams)
               | tyName == nameT =
                   go (i+1) freshVars' env' (AppE p (AppE (AppE (VarE 'Foil.lookupName) (VarE xi)) env')) conParams
               | tyName == termT =
diff --git a/haskell/free-foil/src/Control/Monad/Foil/TH/MkInstancesFoil.hs b/haskell/free-foil/src/Control/Monad/Foil/TH/MkInstancesFoil.hs
index 4ed4b24f..b45a9321 100644
--- a/haskell/free-foil/src/Control/Monad/Foil/TH/MkInstancesFoil.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil/TH/MkInstancesFoil.hs
@@ -8,6 +8,7 @@ module Control.Monad.Foil.TH.MkInstancesFoil (mkInstancesFoil) where
 import           Language.Haskell.TH
 
 import qualified Control.Monad.Foil  as Foil
+import Control.Monad.Foil.TH.Util
 
 -- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.
 mkInstancesFoil
@@ -17,18 +18,18 @@ mkInstancesFoil
   -> Name -- ^ Type name for raw patterns.
   -> Q [Dec]
 mkInstancesFoil termT nameT scopeT patternT = do
-  TyConI (DataD _ctx _name _tvars _kind patternCons _deriv) <- reify patternT
-  TyConI (DataD _ctx _name _tvars _kind scopeCons _deriv) <- reify scopeT
-  TyConI (DataD _ctx _name _tvars _kind termCons _deriv) <- reify termT
+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT
+  TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT
+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT
 
   return
-    [ InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (ConT foilScopeT))
+    [ InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars)))
         [ FunD 'Foil.sinkabilityProof (map clauseScopedTerm scopeCons) ]
 
-    , InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (ConT foilPatternT))
+    , InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars)))
         [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons) ]
 
-    , InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (ConT foilTermT))
+    , InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilTermT (map (VarT . tvarName) termTVars)))
         [ FunD 'Foil.sinkabilityProof (map clauseTerm termCons)]
     ]
 
@@ -58,7 +59,7 @@ mkInstancesFoil termT nameT scopeT patternT = do
         mkConParamPattern _ i = VarP (mkName ("x" ++ show i))
 
         go _i _rename' p [] = p
-        go i rename' p ((_bang, ConT tyName) : conParams)
+        go i rename' p ((_bang, PeelConT tyName _tyParams) : conParams)
           | tyName == nameT =
               go (i + 1) rename' (AppE p (AppE (VarE rename) (VarE xi))) conParams
           | tyName == termT =
@@ -98,7 +99,7 @@ mkInstancesFoil termT nameT scopeT patternT = do
         mkConParamPattern _ i = VarP (mkName ("x" ++ show i))
 
         go _i rename' p [] = AppE (AppE (VarE cont) rename') p
-        go i rename' p ((_bang, ConT tyName) : conParams)
+        go i rename' p ((_bang, PeelConT tyName _tyParams) : conParams)
           | tyName == nameT || tyName == patternT =
               AppE
                 (AppE (AppE (VarE 'Foil.coSinkabilityProof) rename') (VarE xi))
diff --git a/haskell/free-foil/src/Control/Monad/Foil/TH/MkToFoil.hs b/haskell/free-foil/src/Control/Monad/Foil/TH/MkToFoil.hs
index 40734572..8df46f3c 100644
--- a/haskell/free-foil/src/Control/Monad/Foil/TH/MkToFoil.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil/TH/MkToFoil.hs
@@ -13,6 +13,7 @@ import qualified Control.Monad.Foil  as Foil
 import           Data.Maybe          (catMaybes)
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Control.Monad.Foil.TH.Util
 
 -- | Generate conversion functions from raw to scope-safe representation.
 mkToFoil
@@ -37,11 +38,18 @@ mkExtendScopeFoilPattern
   -> Name -- ^ Type name for raw patterns.
   -> Q [Dec]
 mkExtendScopeFoilPattern nameT patternT = do
-  TyConI (DataD _ctx _name _tvars _kind patternCons _deriv) <- reify patternT
-
-  extendScopePatternSignature <-
-    SigD extendScopePatternFunName <$>
-      [t| forall n l. $(return (ConT foilPatternT)) n l -> Foil.Scope n -> Foil.Scope l |]
+  n <- newName "n"
+  l <- newName "l"
+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT
+
+  let extendScopePatternSignature =
+        SigD extendScopePatternFunName $
+          ForallT ([ PlainTV name SpecifiedSpec | name <- (map tvarName patternTVars ++ [n, l]) ]) []
+            (AppT (AppT ArrowT
+              (PeelConT foilPatternT [ VarT name | name <- (map tvarName patternTVars ++ [n, l]) ]))
+              (AppT (AppT ArrowT
+                (AppT (ConT ''Foil.Scope) (VarT n)))
+                (AppT (ConT ''Foil.Scope) (VarT l))))
 
   composefun <- [e| (.) |]
   idfun <- [e| id |]
@@ -76,7 +84,7 @@ mkExtendScopeFoilPattern nameT patternT = do
             conParamVars = zipWith mkConParamVar conParams [1..]
 
             mkConParamVar :: BangType -> Int -> Maybe (Name, Exp)
-            mkConParamVar (_bang, ConT tyName) i
+            mkConParamVar (_bang, PeelConT tyName _tyParams) i
               | tyName == nameT    = Just (x, AppE extendScopeFun (VarE x))
               | tyName == patternT = Just (x, AppE (VarE extendScopePatternFunName) (VarE x))
               where
@@ -94,20 +102,40 @@ mkWithRefreshedFoilPattern
   -> Name -- ^ Type name for raw patterns.
   -> Q [Dec]
 mkWithRefreshedFoilPattern nameT patternT = do
-  TyConI (DataD _ctx _name _tvars _kind patternCons _deriv) <- reify patternT
-
-  withRefreshedFoilPatternSignature <-
-    SigD withRefreshedFoilPatternFunName <$>
-      [t| forall o e n l r.
-            ( Foil.Distinct o, Foil.InjectName e, Foil.Sinkable e )
-            => Foil.Scope o
-            -> $(return (ConT foilPatternT)) n l
-            -> (forall o'. Foil.DExt o o'
-                  => (Foil.Substitution e n o -> Foil.Substitution e l o')
-                  -> $(return (ConT foilPatternT)) o o'
-                  -> r)
-            -> r
-        |]
+  o <- newName "o"
+  o' <- newName "o'"
+  e <- newName "e"
+  n <- newName "n"
+  l <- newName "l"
+  r <- newName "r"
+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT
+
+  let withRefreshedFoilPatternSignature =
+        SigD withRefreshedFoilPatternFunName $
+          ForallT
+            [ PlainTV name SpecifiedSpec | name <- map tvarName patternTVars ++ [o, e, n, l, r] ]
+            [ AppT (ConT ''Foil.Distinct) (VarT o)
+            , AppT (ConT ''Foil.InjectName) (VarT e)
+            , AppT (ConT ''Foil.Sinkable) (VarT e)
+            ]
+            (AppT (AppT ArrowT (PeelConT ''Foil.Scope [VarT o]))
+              (AppT (AppT ArrowT (PeelConT foilPatternT (map (VarT . tvarName) patternTVars ++ [VarT n, VarT l])))
+                (AppT (AppT ArrowT
+                  (ForallT [PlainTV o' SpecifiedSpec] [PeelConT ''Foil.DExt [VarT o, VarT o']]
+                    (AppT (AppT ArrowT (AppT (AppT ArrowT (PeelConT ''Foil.Substitution [VarT e, VarT n, VarT o])) (PeelConT ''Foil.Substitution [VarT e, VarT l, VarT o'])))
+                      (AppT (AppT ArrowT (PeelConT foilPatternT (map (VarT . tvarName) patternTVars ++ [VarT o, VarT o'])))
+                        (VarT r)))))
+                  (VarT r))))
+
+        --           [t| ( Foil.Distinct o, Foil.InjectName e, Foil.Sinkable e )
+        --     => Foil.Scope o
+        --     -> $(return (PeelConT foilPatternT (map (VarT . tyName patternTVars)))) n l
+        --     -> (forall o'. Foil.DExt o o'
+        --           => (Foil.Substitution e n o -> Foil.Substitution e l o')
+        --           -> $(return (ConT foilPatternT)) o o'
+        --           -> r)
+        --     -> r
+        -- |]
 
   composefun <- [e| (.) |]
   addRenameFun <- [e| Foil.addRename |]
@@ -145,7 +173,7 @@ mkWithRefreshedFoilPattern nameT patternT = do
             conMatchBody = go 1 (VarE scope) sinkFun (ConE foilConName) params
 
             go _i _scope' f p [] = AppE (AppE (VarE cont) f) p
-            go i scope' f p ((_bang, ConT tyName) : conParams)
+            go i scope' f p ((_bang, PeelConT tyName _tyParams) : conParams)
               | tyName == nameT =
                   AppE
                     (AppE (AppE withRefreshedFun scope') (AppE nameOfFun (VarE xi)))
@@ -196,34 +224,38 @@ mkToFoilTerm
   -> Name -- ^ Type name for raw patterns.
   -> Q [Dec]
 mkToFoilTerm termT nameT scopeT patternT = do
-  TyConI (DataD _ctx _name _tvars _kind patternCons _deriv) <- reify patternT
-  TyConI (DataD _ctx _name _tvars _kind scopeCons _deriv) <- reify scopeT
-  TyConI (DataD _ctx _name _tvars _kind termCons _deriv) <- reify termT
+  n <- newName "n"
+  let ntype = return (VarT n)
+  r <- newName "r"
+  let rtype = return (VarT r)
+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT
+  TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT
+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT
 
   toFoilTermSignature <-
     SigD toFoilTermT <$>
-      [t| forall n. Foil.Distinct n
-          => Foil.Scope n
-          -> Map $(return (ConT nameT)) (Foil.Name n)
-          -> $(return (ConT termT))
-          -> $(return (ConT foilTermT)) n
+      [t| Foil.Distinct $ntype
+          => Foil.Scope $ntype
+          -> Map $(return (ConT nameT)) (Foil.Name $ntype)
+          -> $(return (PeelConT termT (map (VarT . tvarName) termTVars )))
+          -> $(return (PeelConT foilTermT (map (VarT . tvarName) termTVars))) $ntype
         |]
   toFoilScopedSignature <-
     SigD toFoilScopedT <$>
-      [t| forall n. Foil.Distinct n
-          => Foil.Scope n
-          -> Map $(return (ConT nameT)) (Foil.Name n)
-          -> $(return (ConT scopeT))
-          -> $(return (ConT foilScopeT)) n
+      [t| Foil.Distinct $ntype
+          => Foil.Scope $ntype
+          -> Map $(return (ConT nameT)) (Foil.Name $ntype)
+          -> $(return (PeelConT scopeT (map (VarT . tvarName) scopeTVars)))
+          -> $(return (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars))) $ntype
         |]
   toFoilPatternSignature <-
     SigD toFoilPatternT <$>
-      [t| forall n r. Foil.Distinct n
-          => Foil.Scope n
-          -> Map $(return (ConT nameT)) (Foil.Name n)
-          -> $(return (ConT patternT))
-          -> (forall l. Foil.DExt n l => $(return (ConT foilPatternT)) n l -> Map $(return (ConT nameT)) (Foil.Name l) -> r)
-          -> r
+      [t| Foil.Distinct $ntype
+          => Foil.Scope $ntype
+          -> Map $(return (ConT nameT)) (Foil.Name $ntype)
+          -> $(return (PeelConT patternT (map (VarT . tvarName) patternTVars)))
+          -> (forall l. Foil.DExt $ntype l => $(return (PeelConT foilPatternT (map (VarT . tvarName) patternTVars))) $ntype l -> Map $(return (ConT nameT)) (Foil.Name l) -> $rtype)
+          -> $rtype
         |]
 
   addModFinalizer $ putDoc (DeclDoc toFoilTermT)
@@ -276,7 +308,7 @@ mkToFoilTerm termT nameT scopeT patternT = do
             conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params
 
             go _i _scope' _env' p [] = p
-            go i scope' env' p ((_bang, ConT tyName) : conParams)
+            go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams)
               | tyName == nameT =
                   go (i+1) scope' env' (AppE p (AppE toFoilVarFun (VarE xi))) conParams
               | tyName == termT =
@@ -326,7 +358,7 @@ mkToFoilTerm termT nameT scopeT patternT = do
             conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params
 
             go _i _scope' env' p [] = AppE (AppE (VarE cont) p) env'
-            go i scope' env' p ((_bang, ConT tyName) : conParams)
+            go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams)
               | tyName == nameT =
                   AppE (AppE (VarE 'Foil.withFresh) scope')
                     (LamE [VarP xi']
@@ -388,7 +420,7 @@ mkToFoilTerm termT nameT scopeT patternT = do
             conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params
 
             go _i _scope' _env' p [] = p
-            go i scope' env' p ((_bang, ConT tyName) : conParams)
+            go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams)
               | tyName == nameT =
                   go (i+1) scope' env' (AppE p (AppE toFoilVarFun (VarE xi))) conParams
               | tyName == termT =
diff --git a/haskell/free-foil/src/Control/Monad/Foil/TH/Util.hs b/haskell/free-foil/src/Control/Monad/Foil/TH/Util.hs
new file mode 100644
index 00000000..f177bd3e
--- /dev/null
+++ b/haskell/free-foil/src/Control/Monad/Foil/TH/Util.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE PatternSynonyms                 #-}
+{-# LANGUAGE ViewPatterns                 #-}
+{-# LANGUAGE LambdaCase            #-}
+module Control.Monad.Foil.TH.Util where
+
+import Language.Haskell.TH
+
+peelConT :: Type -> Maybe (Name, [Type])
+peelConT (ConT name) = Just (name, [])
+peelConT (AppT f x) =
+  case peelConT f of
+    Just (g, xs) -> Just (g, xs ++ [x])
+    Nothing -> Nothing
+peelConT _ = Nothing
+
+unpeelConT :: Name -> [Type] -> Type
+unpeelConT = foldl AppT . ConT
+
+pattern PeelConT :: Name -> [Type] -> Type
+pattern PeelConT name types <- (peelConT -> Just (name, types)) where
+  PeelConT name types = unpeelConT name types
+
+tvarName :: TyVarBndr a -> Name
+tvarName = \case
+  PlainTV name _ -> name
+  KindedTV name _ _ -> name
diff --git a/haskell/lambda-pi/Setup.hs b/haskell/lambda-pi/Setup.hs
index 95a44090..3f8f59ca 100644
--- a/haskell/lambda-pi/Setup.hs
+++ b/haskell/lambda-pi/Setup.hs
@@ -35,7 +35,7 @@ main =
                 [ "set -ex" ] <>
                 [ "chcp.com" | isWindows ] <>
                 [ "chcp.com 65001" | isWindows ] <>
-                [ "bnfc --haskell -d -p Language.LambdaPi --generic -o src/ grammar/LambdaPi/Syntax.cf"
+                [ "bnfc --haskell -d -p Language.LambdaPi --functor --generic -o src/ grammar/LambdaPi/Syntax.cf"
                 , "cd src/Language/LambdaPi/Syntax"
                 , "alex Lex.x"
                 , "happy Par.y"
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs
index 3b071b8b..e68b58b8 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs
@@ -199,10 +199,10 @@ toFoilPattern
   -> r
 toFoilPattern scope env pattern cont =
   case pattern of
-    Raw.PatternWildcard -> cont PatternWildcard env
-    Raw.PatternVar x -> withFresh scope $ \binder ->
+    Raw.PatternWildcard _loc -> cont PatternWildcard env
+    Raw.PatternVar _loc x -> withFresh scope $ \binder ->
       cont (PatternVar binder) (Map.insert x (nameOf binder) (sink <$> env))
-    Raw.PatternPair l r ->
+    Raw.PatternPair _loc l r ->
       toFoilPattern scope env l $ \l' env' ->
         let scope' = extendScopePattern l' scope
          in toFoilPattern scope' env' r $ \r' env'' ->
@@ -218,15 +218,17 @@ fromFoilPattern
   -> r
 fromFoilPattern freshVars env pattern cont =
   case pattern of
-    PatternWildcard -> cont freshVars env Raw.PatternWildcard
+    PatternWildcard -> cont freshVars env (Raw.PatternWildcard loc)
     PatternVar z ->
       case freshVars of
         []   -> error "not enough fresh variables!"
-        x:xs -> cont xs (addNameBinder z x env) (Raw.PatternVar x)
+        x:xs -> cont xs (addNameBinder z x env) (Raw.PatternVar loc x)
     PatternPair l r ->
       fromFoilPattern freshVars env l $ \freshVars' env' l' ->
         fromFoilPattern freshVars' env' r $ \freshVars'' env'' r' ->
-          cont freshVars'' env'' (Raw.PatternPair l' r')
+          cont freshVars'' env'' (Raw.PatternPair loc l' r')
+    where
+      loc = error "location information is lost when converting from AST"
 
 -- | Convert a scope-safe term into a raw term.
 fromFoilTerm
@@ -235,19 +237,21 @@ fromFoilTerm
   -> Expr n                 -- ^ A scope safe term in scope @n@.
   -> Raw.Term
 fromFoilTerm freshVars env = \case
-  VarE name -> Raw.Var (lookupName name env)
-  AppE t1 t2 -> Raw.App (fromFoilTerm freshVars env t1) (fromFoilTerm freshVars env t2)
+  VarE name -> Raw.Var loc (lookupName name env)
+  AppE t1 t2 -> Raw.App loc (fromFoilTerm freshVars env t1) (fromFoilTerm freshVars env t2)
   LamE pattern body ->
     fromFoilPattern freshVars env pattern $ \freshVars' env' pattern' ->
-      Raw.Lam pattern' (Raw.AScopedTerm (fromFoilTerm freshVars' env' body))
+      Raw.Lam loc pattern' (Raw.AScopedTerm loc (fromFoilTerm freshVars' env' body))
   PiE pattern a b ->
     fromFoilPattern freshVars env pattern $ \freshVars' env' pattern' ->
-      Raw.Pi pattern' (fromFoilTerm freshVars env a) (Raw.AScopedTerm (fromFoilTerm freshVars' env' b))
-  PairE t1 t2 -> Raw.Pair (fromFoilTerm freshVars env t1) (fromFoilTerm freshVars env t2)
-  FirstE t -> Raw.First (fromFoilTerm freshVars env t)
-  SecondE t -> Raw.Second (fromFoilTerm freshVars env t)
-  ProductE t1 t2 -> Raw.Product (fromFoilTerm freshVars env t1) (fromFoilTerm freshVars env t2)
-  UniverseE -> Raw.Universe
+      Raw.Pi loc pattern' (fromFoilTerm freshVars env a) (Raw.AScopedTerm loc (fromFoilTerm freshVars' env' b))
+  PairE t1 t2 -> Raw.Pair loc (fromFoilTerm freshVars env t1) (fromFoilTerm freshVars env t2)
+  FirstE t -> Raw.First loc (fromFoilTerm freshVars env t)
+  SecondE t -> Raw.Second loc (fromFoilTerm freshVars env t)
+  ProductE t1 t2 -> Raw.Product loc (fromFoilTerm freshVars env t1) (fromFoilTerm freshVars env t2)
+  UniverseE -> Raw.Universe loc
+  where
+    loc = error "location information is lost when converting from AST"
 
 -- | Convert a /closed/ scope-safe term into a raw term.
 fromFoilTermClosed
@@ -264,35 +268,35 @@ toFoilTerm
   -> Raw.Term                   -- ^ A raw term.
   -> Expr n
 toFoilTerm scope env = \case
-  Raw.Var x ->
+  Raw.Var _loc x ->
     case Map.lookup x env of
       Just name -> VarE name
       Nothing   -> error $ "unknown free variable: " <> show x
 
-  Raw.App t1 t2 ->
+  Raw.App _loc t1 t2 ->
     AppE (toFoilTerm scope env t1) (toFoilTerm scope env t2)
 
-  Raw.Lam pattern (Raw.AScopedTerm body) ->
+  Raw.Lam _loc pattern (Raw.AScopedTerm _loc' body) ->
     toFoilPattern scope env pattern $ \pattern' env' ->
       let scope' = extendScopePattern pattern' scope
        in LamE pattern' (toFoilTerm scope' env' body)
 
-  Raw.Pi pattern a (Raw.AScopedTerm b) ->
+  Raw.Pi _loc pattern a (Raw.AScopedTerm _loc' b) ->
     toFoilPattern scope env pattern $ \pattern' env' ->
       let scope' = extendScopePattern pattern' scope
        in PiE pattern' (toFoilTerm scope env a) (toFoilTerm scope' env' b)
 
-  Raw.Pair t1 t2 ->
+  Raw.Pair _loc t1 t2 ->
     PairE (toFoilTerm scope env t1) (toFoilTerm scope env t2)
-  Raw.First t ->
+  Raw.First _loc t ->
     FirstE (toFoilTerm scope env t)
-  Raw.Second t ->
+  Raw.Second _loc t ->
     SecondE (toFoilTerm scope env t)
 
-  Raw.Product t1 t2 ->
+  Raw.Product _loc t1 t2 ->
     ProductE (toFoilTerm scope env t1) (toFoilTerm scope env t2)
 
-  Raw.Universe -> UniverseE
+  Raw.Universe _loc -> UniverseE
 
 -- | Match a pattern against an expression.
 matchPattern :: Pattern n l -> Expr n -> Substitution Expr l n
@@ -324,15 +328,15 @@ whnf scope = \case
 
 -- | Interpret a λΠ command.
 interpretCommand :: Raw.Command -> IO ()
-interpretCommand (Raw.CommandCompute term _type) =
+interpretCommand (Raw.CommandCompute _loc term _type) =
   putStrLn ("  ↦ " ++ printExpr (whnf emptyScope (toFoilTerm emptyScope Map.empty term)))
 -- #TODO: add typeCheck
-interpretCommand (Raw.CommandCheck _term _type) =
+interpretCommand (Raw.CommandCheck _loc _term _type) =
   putStrLn "Not yet implemented"
 
 -- | Interpret a λΠ program.
 interpretProgram :: Raw.Program -> IO ()
-interpretProgram (Raw.AProgram typedTerms) = mapM_ interpretCommand typedTerms
+interpretProgram (Raw.AProgram _loc typedTerms) = mapM_ interpretCommand typedTerms
 
 -- | Default interpreter program.
 -- Reads a λΠ program from the standard input and runs the commands.
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs
index 5d75cc0a..e7ac3bef 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs
@@ -1,5 +1,6 @@
 -- {-# OPTIONS_GHC -ddump-splices #-}
 {-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE KindSignatures         #-}
 {-# LANGUAGE DataKinds         #-}
 {-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
@@ -46,24 +47,27 @@ import qualified Data.Map as Map
 -- * Generated code
 
 -- ** Scope-safe AST
-mkFoilData ''Raw.Term ''Raw.VarIdent ''Raw.ScopedTerm ''Raw.Pattern
-mkInstancesFoil ''Raw.Term ''Raw.VarIdent ''Raw.ScopedTerm ''Raw.Pattern
+mkFoilData ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
+mkInstancesFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
 
 -- ** Conversion from raw to scope-safe AST
-mkToFoil ''Raw.Term ''Raw.VarIdent ''Raw.ScopedTerm ''Raw.Pattern
+mkToFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
 
 -- ** Conversion from scope-safe to raw AST
-mkFromFoil ''Raw.Term ''Raw.VarIdent ''Raw.ScopedTerm ''Raw.Pattern
+mkFromFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
+
+type FoilTerm = FoilTerm' Raw.BNFC'Position
+type FoilPattern = FoilPattern' Raw.BNFC'Position
 
 -- | Convert a /closed/ scope-safe term into a raw term.
 fromFoilTermClosed
   :: [Raw.VarIdent]   -- ^ A stream of fresh variable identifiers.
   -> FoilTerm VoidS       -- ^ A scope safe term in scope @n@.
   -> Raw.Term
-fromFoilTermClosed freshVars = fromFoilTerm freshVars emptyNameMap
+fromFoilTermClosed freshVars = fromFoilTerm' freshVars emptyNameMap
 
-instance InjectName FoilTerm where
-  injectName = FoilVar
+instance InjectName (FoilTerm' a) where
+  injectName = FoilVar (error "undefined location")
 
 -- * User-defined
 
@@ -72,24 +76,24 @@ instance InjectName FoilTerm where
 -- | Perform substitution in a \(\lambda\Pi\)-term.
 substitute :: Distinct o => Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
 substitute scope subst = \case
-    FoilVar name -> lookupSubst subst name
-    FoilApp f x -> FoilApp (substitute scope subst f) (substitute scope subst x)
-    FoilLam pattern (FoilAScopedTerm body) -> withRefreshedFoilPattern scope pattern $ \extendSubst pattern' ->
+    FoilVar _loc name -> lookupSubst subst name
+    FoilApp loc f x -> FoilApp loc (substitute scope subst f) (substitute scope subst x)
+    FoilLam loc1 pattern (FoilAScopedTerm loc2 body) -> withRefreshedFoilPattern' scope pattern $ \extendSubst pattern' ->
       let subst' = extendSubst subst
-          scope' = extendScopeFoilPattern pattern' scope
+          scope' = extendScopeFoilPattern' pattern' scope
           body' = substitute scope' subst' body
-       in FoilLam pattern' (FoilAScopedTerm body')
-    FoilPi pattern a (FoilAScopedTerm b) -> withRefreshedFoilPattern scope pattern $ \extendSubst pattern' ->
+       in FoilLam loc1 pattern' (FoilAScopedTerm loc2 body')
+    FoilPi loc1 pattern a (FoilAScopedTerm loc2 b) -> withRefreshedFoilPattern' scope pattern $ \extendSubst pattern' ->
       let subst' = extendSubst subst
-          scope' = extendScopeFoilPattern pattern' scope
+          scope' = extendScopeFoilPattern' pattern' scope
           a' = substitute scope subst a
           b' = substitute scope' subst' b
-       in FoilPi pattern' a' (FoilAScopedTerm b')
-    FoilPair l r -> FoilPair (substitute scope subst l) (substitute scope subst r)
-    FoilFirst t -> FoilFirst (substitute scope subst t)
-    FoilSecond t -> FoilSecond (substitute scope subst t)
-    FoilProduct l r -> FoilProduct (substitute scope subst l) (substitute scope subst r)
-    FoilUniverse -> FoilUniverse
+       in FoilPi loc1 pattern' a' (FoilAScopedTerm loc2 b')
+    FoilPair loc l r -> FoilPair loc (substitute scope subst l) (substitute scope subst r)
+    FoilFirst loc t -> FoilFirst loc (substitute scope subst t)
+    FoilSecond loc t -> FoilSecond loc (substitute scope subst t)
+    FoilProduct loc l r -> FoilProduct loc (substitute scope subst l) (substitute scope subst r)
+    FoilUniverse loc -> FoilUniverse loc
 
 -- ** Computation
 
@@ -98,42 +102,42 @@ matchPattern :: FoilPattern n l -> FoilTerm n -> Substitution FoilTerm l n
 matchPattern pattern expr = go pattern expr identitySubst
   where
     go :: FoilPattern i l -> FoilTerm n -> Substitution FoilTerm i n -> Substitution FoilTerm l n
-    go FoilPatternWildcard _   = id
-    go (FoilPatternVar x) e    = \subst -> addSubst subst x e
-    go (FoilPatternPair l r) e = go r (FoilSecond e) . go l (FoilFirst e)
+    go FoilPatternWildcard{} _   = id
+    go (FoilPatternVar _loc x) e    = \subst -> addSubst subst x e
+    go (FoilPatternPair loc l r) e = go r (FoilSecond loc e) . go l (FoilFirst loc e)
 
 -- | Compute weak head normal form (WHNF).
 whnf :: Distinct n => Scope n -> FoilTerm n -> FoilTerm n
 whnf scope = \case
-  FoilApp f arg ->
+  FoilApp loc f arg ->
     case whnf scope f of
-      FoilLam pat (FoilAScopedTerm body) ->
+      FoilLam _loc pat (FoilAScopedTerm _loc' body) ->
         let subst = matchPattern pat arg
          in whnf scope (substitute scope subst body)
-      f' -> FoilApp f' arg
-  FoilFirst t ->
+      f' -> FoilApp loc f' arg
+  FoilFirst loc t ->
     case whnf scope t of
-      FoilPair l _r -> whnf scope l
-      t'         -> FoilFirst t'
-  FoilSecond t ->
+      FoilPair _loc l _r -> whnf scope l
+      t'         -> FoilFirst loc t'
+  FoilSecond loc t ->
     case whnf scope t of
-      FoilPair _l r -> whnf scope r
-      t'         -> FoilSecond t'
+      FoilPair _loc _l r -> whnf scope r
+      t'         -> FoilSecond loc t'
   t -> t
 
 -- ** Interpreter
 
 -- | Interpret a λΠ command.
 interpretCommand :: Raw.Command -> IO ()
-interpretCommand (Raw.CommandCompute term _type) =
-  putStrLn ("  ↦ " ++ printFoilTerm (whnf emptyScope (toFoilTerm emptyScope Map.empty term)))
+interpretCommand (Raw.CommandCompute _loc term _type) =
+  putStrLn ("  ↦ " ++ printFoilTerm (whnf emptyScope (toFoilTerm' emptyScope Map.empty term)))
 -- #TODO: add typeCheck
-interpretCommand (Raw.CommandCheck _term _type) =
+interpretCommand (Raw.CommandCheck _loc _term _type) =
   putStrLn "Not yet implemented"
 
 -- | Interpret a λΠ program.
 interpretProgram :: Raw.Program -> IO ()
-interpretProgram (Raw.AProgram typedTerms) = mapM_ interpretCommand typedTerms
+interpretProgram (Raw.AProgram _loc typedTerms) = mapM_ interpretCommand typedTerms
 
 -- | Default interpreter program.
 -- Reads a λΠ program from the standard input and runs the commands.
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs
index db2db446..89de91f7 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs
@@ -140,13 +140,13 @@ toLambdaPiLam
   -> Raw.Pattern                    -- ^ Raw pattern (argument) of the \(\lambda\)-abstraction.
   -> Raw.ScopedTerm                 -- ^ Raw body of the \(\lambda\)-abstraction.
   -> LambdaPi n
-toLambdaPiLam scope env pat (Raw.AScopedTerm body) =
+toLambdaPiLam scope env pat (Raw.AScopedTerm _loc body) =
   case pat of
-    Raw.PatternWildcard -> Foil.withFresh scope $ \binder ->
+    Raw.PatternWildcard _loc -> Foil.withFresh scope $ \binder ->
       let scope' = Foil.extendScope binder scope
        in Lam binder (toLambdaPi scope' (Foil.sink <$> env) body)
 
-    Raw.PatternVar x -> Foil.withFresh scope $ \binder ->
+    Raw.PatternVar _loc x -> Foil.withFresh scope $ \binder ->
       let scope' = Foil.extendScope binder scope
           env' = Map.insert x (Foil.nameOf binder) (Foil.sink <$> env)
        in Lam binder (toLambdaPi scope' env' body)
@@ -162,13 +162,13 @@ toLambdaPiPi
   -> Raw.Term                       -- ^ Raw argument type of the \(\Pi\)-type.
   -> Raw.ScopedTerm                 -- ^ Raw body (result type family) of the \(\Pi\)-type.
   -> LambdaPi n
-toLambdaPiPi scope env pat a (Raw.AScopedTerm b) =
+toLambdaPiPi scope env pat a (Raw.AScopedTerm _loc b) =
   case pat of
-    Raw.PatternWildcard -> Foil.withFresh scope $ \binder ->
+    Raw.PatternWildcard _loc -> Foil.withFresh scope $ \binder ->
       let scope' = Foil.extendScope binder scope
        in Pi binder (toLambdaPi scope env a) (toLambdaPi scope' (Foil.sink <$> env) b)
 
-    Raw.PatternVar x -> Foil.withFresh scope $ \binder ->
+    Raw.PatternVar _loc x -> Foil.withFresh scope $ \binder ->
       let scope' = Foil.extendScope binder scope
           env' = Map.insert x (Foil.nameOf binder) (Foil.sink <$> env)
        in Pi binder (toLambdaPi scope env a) (toLambdaPi scope' env' b)
@@ -183,23 +183,23 @@ toLambdaPi
   -> Raw.Term                       -- ^ Raw expression or type.
   -> LambdaPi n
 toLambdaPi scope env = \case
-  Raw.Var x ->
+  Raw.Var _loc x ->
     case Map.lookup x env of
       Just name -> Var name
       Nothing   -> error ("unbound variable: " ++ Raw.printTree x)
 
-  Raw.App fun arg ->
+  Raw.App _loc fun arg ->
     App (toLambdaPi scope env fun) (toLambdaPi scope env arg)
 
-  Raw.Lam pat body -> toLambdaPiLam scope env pat body
-  Raw.Pi pat a b -> toLambdaPiPi scope env pat a b
+  Raw.Lam _loc pat body -> toLambdaPiLam scope env pat body
+  Raw.Pi _loc pat a b -> toLambdaPiPi scope env pat a b
 
-  Raw.Pair l r -> Pair (toLambdaPi scope env l) (toLambdaPi scope env r)
-  Raw.First t -> First (toLambdaPi scope env t)
-  Raw.Second t -> Second (toLambdaPi scope env t)
-  Raw.Product l r -> Product (toLambdaPi scope env l) (toLambdaPi scope env r)
+  Raw.Pair _loc l r -> Pair (toLambdaPi scope env l) (toLambdaPi scope env r)
+  Raw.First _loc t -> First (toLambdaPi scope env t)
+  Raw.Second _loc t -> Second (toLambdaPi scope env t)
+  Raw.Product _loc l r -> Product (toLambdaPi scope env l) (toLambdaPi scope env r)
 
-  Raw.Universe -> Universe
+  Raw.Universe _loc -> Universe
 
 -- | Convert a raw expression into a /closed/ scope-safe \(\lambda\Pi\)-term.
 toLambdaPiClosed :: Raw.Term -> LambdaPi Foil.VoidS
@@ -212,25 +212,27 @@ fromLambdaPi
   -> LambdaPi n                   -- ^ A scope-safe \(\lambda\Pi\)-term.
   -> Raw.Term
 fromLambdaPi freshVars env = \case
-  Var name -> Raw.Var (Foil.lookupName name env)
-  App fun arg -> Raw.App (fromLambdaPi freshVars env fun) (fromLambdaPi freshVars env arg)
+  Var name -> Raw.Var loc (Foil.lookupName name env)
+  App fun arg -> Raw.App loc (fromLambdaPi freshVars env fun) (fromLambdaPi freshVars env arg)
   Lam binder body ->
     case freshVars of
       [] -> error "not enough fresh variables"
       x:freshVars' ->
         let env' = Foil.addNameBinder binder x env
-         in Raw.Lam (Raw.PatternVar x) (Raw.AScopedTerm (fromLambdaPi freshVars' env' body))
+         in Raw.Lam loc (Raw.PatternVar loc x) (Raw.AScopedTerm loc (fromLambdaPi freshVars' env' body))
   Pi binder a b ->
     case freshVars of
       [] -> error "not enough fresh variables"
       x:freshVars' ->
         let env' = Foil.addNameBinder binder x env
-         in Raw.Pi (Raw.PatternVar x) (fromLambdaPi freshVars env a) (Raw.AScopedTerm (fromLambdaPi freshVars' env' b))
-  Pair l r -> Raw.Pair (fromLambdaPi freshVars env l) (fromLambdaPi freshVars env r)
-  First t -> Raw.First (fromLambdaPi freshVars env t)
-  Second t -> Raw.Second (fromLambdaPi freshVars env t)
-  Product l r -> Raw.Product (fromLambdaPi freshVars env l) (fromLambdaPi freshVars env r)
-  Universe -> Raw.Universe
+         in Raw.Pi loc (Raw.PatternVar loc x) (fromLambdaPi freshVars env a) (Raw.AScopedTerm loc (fromLambdaPi freshVars' env' b))
+  Pair l r -> Raw.Pair loc (fromLambdaPi freshVars env l) (fromLambdaPi freshVars env r)
+  First t -> Raw.First loc (fromLambdaPi freshVars env t)
+  Second t -> Raw.Second loc (fromLambdaPi freshVars env t)
+  Product l r -> Raw.Product loc (fromLambdaPi freshVars env l) (fromLambdaPi freshVars env r)
+  Universe -> Raw.Universe loc
+  where
+    loc = error "no location info available when converting from an AST"
 
 -- | Pretty-print a /closed/ \(\lambda\Pi\)-term.
 ppLambdaPi :: LambdaPi Foil.VoidS -> String
@@ -238,14 +240,14 @@ ppLambdaPi = Raw.printTree . fromLambdaPi [ Raw.VarIdent ("x" <> show i) | i <-
 
 -- | Interpret a λΠ command.
 interpretCommand :: Raw.Command -> IO ()
-interpretCommand (Raw.CommandCompute term _type) =
+interpretCommand (Raw.CommandCompute _loc term _type) =
       putStrLn ("  ↦ " ++ ppLambdaPi (whnf Foil.emptyScope (toLambdaPi Foil.emptyScope Map.empty term)))
 -- #TODO: add typeCheck
-interpretCommand (Raw.CommandCheck _term _type) = putStrLn "check is not yet implemented"
+interpretCommand (Raw.CommandCheck _loc _term _type) = putStrLn "check is not yet implemented"
 
 -- | Interpret a λΠ program.
 interpretProgram :: Raw.Program -> IO ()
-interpretProgram (Raw.AProgram typedTerms) = mapM_ interpretCommand typedTerms
+interpretProgram (Raw.AProgram _loc typedTerms) = mapM_ interpretCommand typedTerms
 
 -- | A \(\lambda\Pi\) interpreter implemented via the free foil.
 defaultMain :: IO ()
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Abs.hs b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Abs.hs
index 439fc5e1..a524f770 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Abs.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Abs.hs
@@ -2,46 +2,107 @@
 
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
 
 -- | The abstract syntax of language Syntax.
 
 module Language.LambdaPi.Syntax.Abs where
 
 import Prelude (String)
-import qualified Prelude as C (Eq, Ord, Show, Read)
+import qualified Prelude as C
+  ( Eq, Ord, Show, Read
+  , Functor, Foldable, Traversable
+  , Int, Maybe(..)
+  )
 import qualified Data.String
 
 import qualified Data.Data    as C (Data, Typeable)
 import qualified GHC.Generics as C (Generic)
 
-data Program = AProgram [Command]
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
-
-data Command = CommandCheck Term Term | CommandCompute Term Term
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
-
-data Term
-    = Var VarIdent
-    | Pi Pattern Term ScopedTerm
-    | Lam Pattern ScopedTerm
-    | App Term Term
-    | Product Term Term
-    | Pair Term Term
-    | First Term
-    | Second Term
-    | Universe
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
-
-data ScopedTerm = AScopedTerm Term
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
-
-data Pattern
-    = PatternWildcard
-    | PatternVar VarIdent
-    | PatternPair Pattern Pattern
-  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
+type Program = Program' BNFC'Position
+data Program' a = AProgram a [Command' a]
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+
+type Command = Command' BNFC'Position
+data Command' a
+    = CommandCheck a (Term' a) (Term' a)
+    | CommandCompute a (Term' a) (Term' a)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+
+type Term = Term' BNFC'Position
+data Term' a
+    = Var a VarIdent
+    | Pi a (Pattern' a) (Term' a) (ScopedTerm' a)
+    | Lam a (Pattern' a) (ScopedTerm' a)
+    | App a (Term' a) (Term' a)
+    | Product a (Term' a) (Term' a)
+    | Pair a (Term' a) (Term' a)
+    | First a (Term' a)
+    | Second a (Term' a)
+    | Universe a
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+
+type ScopedTerm = ScopedTerm' BNFC'Position
+data ScopedTerm' a = AScopedTerm a (Term' a)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+
+type Pattern = Pattern' BNFC'Position
+data Pattern' a
+    = PatternWildcard a
+    | PatternVar a VarIdent
+    | PatternPair a (Pattern' a) (Pattern' a)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
 
 newtype VarIdent = VarIdent String
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
 
+-- | Start position (line, column) of something.
+
+type BNFC'Position = C.Maybe (C.Int, C.Int)
+
+pattern BNFC'NoPosition :: BNFC'Position
+pattern BNFC'NoPosition = C.Nothing
+
+pattern BNFC'Position :: C.Int -> C.Int -> BNFC'Position
+pattern BNFC'Position line col = C.Just (line, col)
+
+-- | Get the start position of something.
+
+class HasPosition a where
+  hasPosition :: a -> BNFC'Position
+
+instance HasPosition Program where
+  hasPosition = \case
+    AProgram p _ -> p
+
+instance HasPosition Command where
+  hasPosition = \case
+    CommandCheck p _ _ -> p
+    CommandCompute p _ _ -> p
+
+instance HasPosition Term where
+  hasPosition = \case
+    Var p _ -> p
+    Pi p _ _ _ -> p
+    Lam p _ _ -> p
+    App p _ _ -> p
+    Product p _ _ -> p
+    Pair p _ _ -> p
+    First p _ -> p
+    Second p _ -> p
+    Universe p -> p
+
+instance HasPosition ScopedTerm where
+  hasPosition = \case
+    AScopedTerm p _ -> p
+
+instance HasPosition Pattern where
+  hasPosition = \case
+    PatternWildcard p -> p
+    PatternVar p _ -> p
+    PatternPair p _ _ -> p
+
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.hs b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.hs
index 9a15269c..3c7a01d2 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.hs
@@ -29,13 +29,13 @@ import Control.Monad (ap)
 data HappyAbsSyn 
 	= HappyTerminal (Token)
 	| HappyErrorToken Prelude.Int
-	| HappyAbsSyn11 (Language.LambdaPi.Syntax.Abs.VarIdent)
-	| HappyAbsSyn12 (Language.LambdaPi.Syntax.Abs.Program)
-	| HappyAbsSyn13 (Language.LambdaPi.Syntax.Abs.Command)
-	| HappyAbsSyn14 ([Language.LambdaPi.Syntax.Abs.Command])
-	| HappyAbsSyn15 (Language.LambdaPi.Syntax.Abs.Term)
-	| HappyAbsSyn18 (Language.LambdaPi.Syntax.Abs.ScopedTerm)
-	| HappyAbsSyn19 (Language.LambdaPi.Syntax.Abs.Pattern)
+	| HappyAbsSyn11 ((Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.VarIdent))
+	| HappyAbsSyn12 ((Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Program))
+	| HappyAbsSyn13 ((Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Command))
+	| HappyAbsSyn14 ((Language.LambdaPi.Syntax.Abs.BNFC'Position, [Language.LambdaPi.Syntax.Abs.Command]))
+	| HappyAbsSyn15 ((Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Term))
+	| HappyAbsSyn18 ((Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.ScopedTerm))
+	| HappyAbsSyn19 ((Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Pattern))
 
 {- to allow type-synonyms as our monads (likely
  - with explicitly-specified bind and return)
@@ -168,7 +168,7 @@ happyExpList = Happy_Data_Array.listArray (0,149) ([0,3072,0,32768,1,0,48,0,4,4,
 {-# NOINLINE happyExpListPerState #-}
 happyExpListPerState st =
     token_strs_expected
-  where token_strs = ["error","%dummy","%start_pProgram","%start_pCommand","%start_pListCommand","%start_pTerm2","%start_pTerm","%start_pTerm1","%start_pScopedTerm","%start_pPattern","VarIdent","Program","Command","ListCommand","Term2","Term","Term1","ScopedTerm","Pattern","'('","')'","','","'.'","':'","';'","'_'","'check'","'compute'","'\215'","'\928'","'\955'","'\960\8321'","'\960\8322'","'\8594'","'\120140'","L_VarIdent","%eof"]
+  where token_strs = ["error","%dummy","%start_pProgram_internal","%start_pCommand_internal","%start_pListCommand_internal","%start_pTerm2_internal","%start_pTerm_internal","%start_pTerm1_internal","%start_pScopedTerm_internal","%start_pPattern_internal","VarIdent","Program","Command","ListCommand","Term2","Term","Term1","ScopedTerm","Pattern","'('","')'","','","'.'","':'","';'","'_'","'check'","'compute'","'\215'","'\928'","'\955'","'\960\8321'","'\960\8322'","'\8594'","'\120140'","L_VarIdent","%eof"]
         bit_start = st Prelude.* 37
         bit_end = (st Prelude.+ 1) Prelude.* 37
         read_bit = readArrayBit happyExpList
@@ -577,16 +577,16 @@ action_71 _ = happyFail (happyExpListPerState 71)
 action_72 _ = happyReduce_16
 
 happyReduce_8 = happySpecReduce_1  11 happyReduction_8
-happyReduction_8 (HappyTerminal (PT _ (T_VarIdent happy_var_1)))
+happyReduction_8 (HappyTerminal happy_var_1)
 	 =  HappyAbsSyn11
-		 (Language.LambdaPi.Syntax.Abs.VarIdent happy_var_1
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.VarIdent (tokenText happy_var_1))
 	)
 happyReduction_8 _  = notHappyAtAll 
 
 happyReduce_9 = happySpecReduce_1  12 happyReduction_9
 happyReduction_9 (HappyAbsSyn14  happy_var_1)
 	 =  HappyAbsSyn12
-		 (Language.LambdaPi.Syntax.Abs.AProgram happy_var_1
+		 ((fst happy_var_1, Language.LambdaPi.Syntax.Abs.AProgram (fst happy_var_1) (snd happy_var_1))
 	)
 happyReduction_9 _  = notHappyAtAll 
 
@@ -594,25 +594,25 @@ happyReduce_10 = happyReduce 4 13 happyReduction_10
 happyReduction_10 ((HappyAbsSyn15  happy_var_4) `HappyStk`
 	_ `HappyStk`
 	(HappyAbsSyn15  happy_var_2) `HappyStk`
-	_ `HappyStk`
+	(HappyTerminal happy_var_1) `HappyStk`
 	happyRest)
 	 = HappyAbsSyn13
-		 (Language.LambdaPi.Syntax.Abs.CommandCheck happy_var_2 happy_var_4
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.CommandCheck (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)) (snd happy_var_2) (snd happy_var_4))
 	) `HappyStk` happyRest
 
 happyReduce_11 = happyReduce 4 13 happyReduction_11
 happyReduction_11 ((HappyAbsSyn15  happy_var_4) `HappyStk`
 	_ `HappyStk`
 	(HappyAbsSyn15  happy_var_2) `HappyStk`
-	_ `HappyStk`
+	(HappyTerminal happy_var_1) `HappyStk`
 	happyRest)
 	 = HappyAbsSyn13
-		 (Language.LambdaPi.Syntax.Abs.CommandCompute happy_var_2 happy_var_4
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.CommandCompute (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)) (snd happy_var_2) (snd happy_var_4))
 	) `HappyStk` happyRest
 
 happyReduce_12 = happySpecReduce_0  14 happyReduction_12
 happyReduction_12  =  HappyAbsSyn14
-		 ([]
+		 ((Language.LambdaPi.Syntax.Abs.BNFC'NoPosition, [])
 	)
 
 happyReduce_13 = happySpecReduce_3  14 happyReduction_13
@@ -620,23 +620,23 @@ happyReduction_13 (HappyAbsSyn14  happy_var_3)
 	_
 	(HappyAbsSyn13  happy_var_1)
 	 =  HappyAbsSyn14
-		 ((:) happy_var_1 happy_var_3
+		 ((fst happy_var_1, (:) (snd happy_var_1) (snd happy_var_3))
 	)
 happyReduction_13 _ _ _  = notHappyAtAll 
 
 happyReduce_14 = happySpecReduce_1  15 happyReduction_14
 happyReduction_14 (HappyAbsSyn11  happy_var_1)
 	 =  HappyAbsSyn15
-		 (Language.LambdaPi.Syntax.Abs.Var happy_var_1
+		 ((fst happy_var_1, Language.LambdaPi.Syntax.Abs.Var (fst happy_var_1) (snd happy_var_1))
 	)
 happyReduction_14 _  = notHappyAtAll 
 
 happyReduce_15 = happySpecReduce_3  15 happyReduction_15
 happyReduction_15 _
 	(HappyAbsSyn15  happy_var_2)
-	_
+	(HappyTerminal happy_var_1)
 	 =  HappyAbsSyn15
-		 (happy_var_2
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), (snd happy_var_2))
 	)
 happyReduction_15 _ _ _  = notHappyAtAll 
 
@@ -648,20 +648,20 @@ happyReduction_16 ((HappyAbsSyn18  happy_var_8) `HappyStk`
 	_ `HappyStk`
 	(HappyAbsSyn19  happy_var_3) `HappyStk`
 	_ `HappyStk`
-	_ `HappyStk`
+	(HappyTerminal happy_var_1) `HappyStk`
 	happyRest)
 	 = HappyAbsSyn15
-		 (Language.LambdaPi.Syntax.Abs.Pi happy_var_3 happy_var_5 happy_var_8
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.Pi (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)) (snd happy_var_3) (snd happy_var_5) (snd happy_var_8))
 	) `HappyStk` happyRest
 
 happyReduce_17 = happyReduce 4 16 happyReduction_17
 happyReduction_17 ((HappyAbsSyn18  happy_var_4) `HappyStk`
 	_ `HappyStk`
 	(HappyAbsSyn19  happy_var_2) `HappyStk`
-	_ `HappyStk`
+	(HappyTerminal happy_var_1) `HappyStk`
 	happyRest)
 	 = HappyAbsSyn15
-		 (Language.LambdaPi.Syntax.Abs.Lam happy_var_2 happy_var_4
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.Lam (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)) (snd happy_var_2) (snd happy_var_4))
 	) `HappyStk` happyRest
 
 happyReduce_18 = happySpecReduce_3  16 happyReduction_18
@@ -669,7 +669,7 @@ happyReduction_18 (HappyAbsSyn15  happy_var_3)
 	_
 	(HappyAbsSyn15  happy_var_1)
 	 =  HappyAbsSyn15
-		 (Language.LambdaPi.Syntax.Abs.Product happy_var_1 happy_var_3
+		 ((fst happy_var_1, Language.LambdaPi.Syntax.Abs.Product (fst happy_var_1) (snd happy_var_1) (snd happy_var_3))
 	)
 happyReduction_18 _ _ _  = notHappyAtAll 
 
@@ -678,42 +678,43 @@ happyReduction_19 (_ `HappyStk`
 	(HappyAbsSyn15  happy_var_4) `HappyStk`
 	_ `HappyStk`
 	(HappyAbsSyn15  happy_var_2) `HappyStk`
-	_ `HappyStk`
+	(HappyTerminal happy_var_1) `HappyStk`
 	happyRest)
 	 = HappyAbsSyn15
-		 (Language.LambdaPi.Syntax.Abs.Pair happy_var_2 happy_var_4
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.Pair (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)) (snd happy_var_2) (snd happy_var_4))
 	) `HappyStk` happyRest
 
 happyReduce_20 = happyReduce 4 16 happyReduction_20
 happyReduction_20 (_ `HappyStk`
 	(HappyAbsSyn15  happy_var_3) `HappyStk`
 	_ `HappyStk`
-	_ `HappyStk`
+	(HappyTerminal happy_var_1) `HappyStk`
 	happyRest)
 	 = HappyAbsSyn15
-		 (Language.LambdaPi.Syntax.Abs.First happy_var_3
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.First (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)) (snd happy_var_3))
 	) `HappyStk` happyRest
 
 happyReduce_21 = happyReduce 4 16 happyReduction_21
 happyReduction_21 (_ `HappyStk`
 	(HappyAbsSyn15  happy_var_3) `HappyStk`
 	_ `HappyStk`
-	_ `HappyStk`
+	(HappyTerminal happy_var_1) `HappyStk`
 	happyRest)
 	 = HappyAbsSyn15
-		 (Language.LambdaPi.Syntax.Abs.Second happy_var_3
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.Second (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)) (snd happy_var_3))
 	) `HappyStk` happyRest
 
 happyReduce_22 = happySpecReduce_1  16 happyReduction_22
-happyReduction_22 _
+happyReduction_22 (HappyTerminal happy_var_1)
 	 =  HappyAbsSyn15
-		 (Language.LambdaPi.Syntax.Abs.Universe
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.Universe (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)))
 	)
+happyReduction_22 _  = notHappyAtAll 
 
 happyReduce_23 = happySpecReduce_1  16 happyReduction_23
 happyReduction_23 (HappyAbsSyn15  happy_var_1)
 	 =  HappyAbsSyn15
-		 (happy_var_1
+		 ((fst happy_var_1, (snd happy_var_1))
 	)
 happyReduction_23 _  = notHappyAtAll 
 
@@ -721,34 +722,35 @@ happyReduce_24 = happySpecReduce_2  17 happyReduction_24
 happyReduction_24 (HappyAbsSyn15  happy_var_2)
 	(HappyAbsSyn15  happy_var_1)
 	 =  HappyAbsSyn15
-		 (Language.LambdaPi.Syntax.Abs.App happy_var_1 happy_var_2
+		 ((fst happy_var_1, Language.LambdaPi.Syntax.Abs.App (fst happy_var_1) (snd happy_var_1) (snd happy_var_2))
 	)
 happyReduction_24 _ _  = notHappyAtAll 
 
 happyReduce_25 = happySpecReduce_1  17 happyReduction_25
 happyReduction_25 (HappyAbsSyn15  happy_var_1)
 	 =  HappyAbsSyn15
-		 (happy_var_1
+		 ((fst happy_var_1, (snd happy_var_1))
 	)
 happyReduction_25 _  = notHappyAtAll 
 
 happyReduce_26 = happySpecReduce_1  18 happyReduction_26
 happyReduction_26 (HappyAbsSyn15  happy_var_1)
 	 =  HappyAbsSyn18
-		 (Language.LambdaPi.Syntax.Abs.AScopedTerm happy_var_1
+		 ((fst happy_var_1, Language.LambdaPi.Syntax.Abs.AScopedTerm (fst happy_var_1) (snd happy_var_1))
 	)
 happyReduction_26 _  = notHappyAtAll 
 
 happyReduce_27 = happySpecReduce_1  19 happyReduction_27
-happyReduction_27 _
+happyReduction_27 (HappyTerminal happy_var_1)
 	 =  HappyAbsSyn19
-		 (Language.LambdaPi.Syntax.Abs.PatternWildcard
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.PatternWildcard (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)))
 	)
+happyReduction_27 _  = notHappyAtAll 
 
 happyReduce_28 = happySpecReduce_1  19 happyReduction_28
 happyReduction_28 (HappyAbsSyn11  happy_var_1)
 	 =  HappyAbsSyn19
-		 (Language.LambdaPi.Syntax.Abs.PatternVar happy_var_1
+		 ((fst happy_var_1, Language.LambdaPi.Syntax.Abs.PatternVar (fst happy_var_1) (snd happy_var_1))
 	)
 happyReduction_28 _  = notHappyAtAll 
 
@@ -757,10 +759,10 @@ happyReduction_29 (_ `HappyStk`
 	(HappyAbsSyn19  happy_var_4) `HappyStk`
 	_ `HappyStk`
 	(HappyAbsSyn19  happy_var_2) `HappyStk`
-	_ `HappyStk`
+	(HappyTerminal happy_var_1) `HappyStk`
 	happyRest)
 	 = HappyAbsSyn19
-		 (Language.LambdaPi.Syntax.Abs.PatternPair happy_var_2 happy_var_4
+		 ((uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1), Language.LambdaPi.Syntax.Abs.PatternPair (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol happy_var_1)) (snd happy_var_2) (snd happy_var_4))
 	) `HappyStk` happyRest
 
 happyNewToken action sts stk [] =
@@ -785,7 +787,7 @@ happyNewToken action sts stk (tk:tks) =
 	PT _ (TS _ 14) -> cont 33;
 	PT _ (TS _ 15) -> cont 34;
 	PT _ (TS _ 16) -> cont 35;
-	PT _ (T_VarIdent happy_dollar_dollar) -> cont 36;
+	PT _ (T_VarIdent _) -> cont 36;
 	_ -> happyError' ((tk:tks), [])
 	}
 
@@ -801,28 +803,28 @@ happyReturn1 :: () => a -> b -> Err a
 happyReturn1 = \a tks -> (return) a
 happyError' :: () => ([(Token)], [Prelude.String]) -> Err a
 happyError' = (\(tokens, _) -> happyError tokens)
-pProgram tks = happySomeParser where
+pProgram_internal tks = happySomeParser where
  happySomeParser = happyThen (happyParse action_0 tks) (\x -> case x of {HappyAbsSyn12 z -> happyReturn z; _other -> notHappyAtAll })
 
-pCommand tks = happySomeParser where
+pCommand_internal tks = happySomeParser where
  happySomeParser = happyThen (happyParse action_1 tks) (\x -> case x of {HappyAbsSyn13 z -> happyReturn z; _other -> notHappyAtAll })
 
-pListCommand tks = happySomeParser where
+pListCommand_internal tks = happySomeParser where
  happySomeParser = happyThen (happyParse action_2 tks) (\x -> case x of {HappyAbsSyn14 z -> happyReturn z; _other -> notHappyAtAll })
 
-pTerm2 tks = happySomeParser where
+pTerm2_internal tks = happySomeParser where
  happySomeParser = happyThen (happyParse action_3 tks) (\x -> case x of {HappyAbsSyn15 z -> happyReturn z; _other -> notHappyAtAll })
 
-pTerm tks = happySomeParser where
+pTerm_internal tks = happySomeParser where
  happySomeParser = happyThen (happyParse action_4 tks) (\x -> case x of {HappyAbsSyn15 z -> happyReturn z; _other -> notHappyAtAll })
 
-pTerm1 tks = happySomeParser where
+pTerm1_internal tks = happySomeParser where
  happySomeParser = happyThen (happyParse action_5 tks) (\x -> case x of {HappyAbsSyn15 z -> happyReturn z; _other -> notHappyAtAll })
 
-pScopedTerm tks = happySomeParser where
+pScopedTerm_internal tks = happySomeParser where
  happySomeParser = happyThen (happyParse action_6 tks) (\x -> case x of {HappyAbsSyn18 z -> happyReturn z; _other -> notHappyAtAll })
 
-pPattern tks = happySomeParser where
+pPattern_internal tks = happySomeParser where
  happySomeParser = happyThen (happyParse action_7 tks) (\x -> case x of {HappyAbsSyn19 z -> happyReturn z; _other -> notHappyAtAll })
 
 happySeq = happyDontSeq
@@ -840,6 +842,32 @@ happyError ts = Left $
 
 myLexer :: String -> [Token]
 myLexer = tokens
+
+-- Entrypoints
+
+pProgram :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Program
+pProgram = fmap snd . pProgram_internal
+
+pCommand :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Command
+pCommand = fmap snd . pCommand_internal
+
+pListCommand :: [Token] -> Err [Language.LambdaPi.Syntax.Abs.Command]
+pListCommand = fmap snd . pListCommand_internal
+
+pTerm2 :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Term
+pTerm2 = fmap snd . pTerm2_internal
+
+pTerm :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Term
+pTerm = fmap snd . pTerm_internal
+
+pTerm1 :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Term
+pTerm1 = fmap snd . pTerm1_internal
+
+pScopedTerm :: [Token] -> Err Language.LambdaPi.Syntax.Abs.ScopedTerm
+pScopedTerm = fmap snd . pScopedTerm_internal
+
+pPattern :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Pattern
+pPattern = fmap snd . pPattern_internal
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 -- $Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp $
 
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.y b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.y
index e0486cfe..210e5cb9 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.y
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.y
@@ -25,82 +25,85 @@ import Language.LambdaPi.Syntax.Lex
 
 }
 
-%name pProgram Program
-%name pCommand Command
-%name pListCommand ListCommand
-%name pTerm2 Term2
-%name pTerm Term
-%name pTerm1 Term1
-%name pScopedTerm ScopedTerm
-%name pPattern Pattern
+%name pProgram_internal Program
+%name pCommand_internal Command
+%name pListCommand_internal ListCommand
+%name pTerm2_internal Term2
+%name pTerm_internal Term
+%name pTerm1_internal Term1
+%name pScopedTerm_internal ScopedTerm
+%name pPattern_internal Pattern
 -- no lexer declaration
 %monad { Err } { (>>=) } { return }
 %tokentype {Token}
 %token
-  '('        { PT _ (TS _ 1)        }
-  ')'        { PT _ (TS _ 2)        }
-  ','        { PT _ (TS _ 3)        }
-  '.'        { PT _ (TS _ 4)        }
-  ':'        { PT _ (TS _ 5)        }
-  ';'        { PT _ (TS _ 6)        }
-  '_'        { PT _ (TS _ 7)        }
-  'check'    { PT _ (TS _ 8)        }
-  'compute'  { PT _ (TS _ 9)        }
-  '×'        { PT _ (TS _ 10)       }
-  'Π'        { PT _ (TS _ 11)       }
-  'λ'        { PT _ (TS _ 12)       }
-  'π₁'       { PT _ (TS _ 13)       }
-  'π₂'       { PT _ (TS _ 14)       }
-  '→'        { PT _ (TS _ 15)       }
-  '𝕌'        { PT _ (TS _ 16)       }
-  L_VarIdent { PT _ (T_VarIdent $$) }
+  '('        { PT _ (TS _ 1)       }
+  ')'        { PT _ (TS _ 2)       }
+  ','        { PT _ (TS _ 3)       }
+  '.'        { PT _ (TS _ 4)       }
+  ':'        { PT _ (TS _ 5)       }
+  ';'        { PT _ (TS _ 6)       }
+  '_'        { PT _ (TS _ 7)       }
+  'check'    { PT _ (TS _ 8)       }
+  'compute'  { PT _ (TS _ 9)       }
+  '×'        { PT _ (TS _ 10)      }
+  'Π'        { PT _ (TS _ 11)      }
+  'λ'        { PT _ (TS _ 12)      }
+  'π₁'       { PT _ (TS _ 13)      }
+  'π₂'       { PT _ (TS _ 14)      }
+  '→'        { PT _ (TS _ 15)      }
+  '𝕌'        { PT _ (TS _ 16)      }
+  L_VarIdent { PT _ (T_VarIdent _) }
 
 %%
 
-VarIdent :: { Language.LambdaPi.Syntax.Abs.VarIdent }
-VarIdent  : L_VarIdent { Language.LambdaPi.Syntax.Abs.VarIdent $1 }
+VarIdent :: { (Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.VarIdent) }
+VarIdent  : L_VarIdent { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.VarIdent (tokenText $1)) }
 
-Program :: { Language.LambdaPi.Syntax.Abs.Program }
-Program : ListCommand { Language.LambdaPi.Syntax.Abs.AProgram $1 }
+Program :: { (Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Program) }
+Program
+  : ListCommand { (fst $1, Language.LambdaPi.Syntax.Abs.AProgram (fst $1) (snd $1)) }
 
-Command :: { Language.LambdaPi.Syntax.Abs.Command }
+Command :: { (Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Command) }
 Command
-  : 'check' Term ':' Term { Language.LambdaPi.Syntax.Abs.CommandCheck $2 $4 }
-  | 'compute' Term ':' Term { Language.LambdaPi.Syntax.Abs.CommandCompute $2 $4 }
+  : 'check' Term ':' Term { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.CommandCheck (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | 'compute' Term ':' Term { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.CommandCompute (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
 
-ListCommand :: { [Language.LambdaPi.Syntax.Abs.Command] }
+ListCommand :: { (Language.LambdaPi.Syntax.Abs.BNFC'Position, [Language.LambdaPi.Syntax.Abs.Command]) }
 ListCommand
-  : {- empty -} { [] } | Command ';' ListCommand { (:) $1 $3 }
+  : {- empty -} { (Language.LambdaPi.Syntax.Abs.BNFC'NoPosition, []) }
+  | Command ';' ListCommand { (fst $1, (:) (snd $1) (snd $3)) }
 
-Term2 :: { Language.LambdaPi.Syntax.Abs.Term }
+Term2 :: { (Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Term) }
 Term2
-  : VarIdent { Language.LambdaPi.Syntax.Abs.Var $1 }
-  | '(' Term ')' { $2 }
+  : VarIdent { (fst $1, Language.LambdaPi.Syntax.Abs.Var (fst $1) (snd $1)) }
+  | '(' Term ')' { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), (snd $2)) }
 
-Term :: { Language.LambdaPi.Syntax.Abs.Term }
+Term :: { (Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Term) }
 Term
-  : 'Π' '(' Pattern ':' Term ')' '→' ScopedTerm { Language.LambdaPi.Syntax.Abs.Pi $3 $5 $8 }
-  | 'λ' Pattern '.' ScopedTerm { Language.LambdaPi.Syntax.Abs.Lam $2 $4 }
-  | Term1 '×' Term1 { Language.LambdaPi.Syntax.Abs.Product $1 $3 }
-  | '(' Term ',' Term ')' { Language.LambdaPi.Syntax.Abs.Pair $2 $4 }
-  | 'π₁' '(' Term ')' { Language.LambdaPi.Syntax.Abs.First $3 }
-  | 'π₂' '(' Term ')' { Language.LambdaPi.Syntax.Abs.Second $3 }
-  | '𝕌' { Language.LambdaPi.Syntax.Abs.Universe }
-  | Term1 { $1 }
-
-Term1 :: { Language.LambdaPi.Syntax.Abs.Term }
+  : 'Π' '(' Pattern ':' Term ')' '→' ScopedTerm { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.Pi (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | 'λ' Pattern '.' ScopedTerm { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.Lam (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | Term1 '×' Term1 { (fst $1, Language.LambdaPi.Syntax.Abs.Product (fst $1) (snd $1) (snd $3)) }
+  | '(' Term ',' Term ')' { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.Pair (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | 'π₁' '(' Term ')' { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.First (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }
+  | 'π₂' '(' Term ')' { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.Second (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }
+  | '𝕌' { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.Universe (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | Term1 { (fst $1, (snd $1)) }
+
+Term1 :: { (Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Term) }
 Term1
-  : Term1 Term2 { Language.LambdaPi.Syntax.Abs.App $1 $2 }
-  | Term2 { $1 }
+  : Term1 Term2 { (fst $1, Language.LambdaPi.Syntax.Abs.App (fst $1) (snd $1) (snd $2)) }
+  | Term2 { (fst $1, (snd $1)) }
 
-ScopedTerm :: { Language.LambdaPi.Syntax.Abs.ScopedTerm }
-ScopedTerm : Term { Language.LambdaPi.Syntax.Abs.AScopedTerm $1 }
+ScopedTerm :: { (Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.ScopedTerm) }
+ScopedTerm
+  : Term { (fst $1, Language.LambdaPi.Syntax.Abs.AScopedTerm (fst $1) (snd $1)) }
 
-Pattern :: { Language.LambdaPi.Syntax.Abs.Pattern }
+Pattern :: { (Language.LambdaPi.Syntax.Abs.BNFC'Position, Language.LambdaPi.Syntax.Abs.Pattern) }
 Pattern
-  : '_' { Language.LambdaPi.Syntax.Abs.PatternWildcard }
-  | VarIdent { Language.LambdaPi.Syntax.Abs.PatternVar $1 }
-  | '(' Pattern ',' Pattern ')' { Language.LambdaPi.Syntax.Abs.PatternPair $2 $4 }
+  : '_' { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.PatternWildcard (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | VarIdent { (fst $1, Language.LambdaPi.Syntax.Abs.PatternVar (fst $1) (snd $1)) }
+  | '(' Pattern ',' Pattern ')' { (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.LambdaPi.Syntax.Abs.PatternPair (uncurry Language.LambdaPi.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
 
 {
 
@@ -117,5 +120,30 @@ happyError ts = Left $
 myLexer :: String -> [Token]
 myLexer = tokens
 
+-- Entrypoints
+
+pProgram :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Program
+pProgram = fmap snd . pProgram_internal
+
+pCommand :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Command
+pCommand = fmap snd . pCommand_internal
+
+pListCommand :: [Token] -> Err [Language.LambdaPi.Syntax.Abs.Command]
+pListCommand = fmap snd . pListCommand_internal
+
+pTerm2 :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Term
+pTerm2 = fmap snd . pTerm2_internal
+
+pTerm :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Term
+pTerm = fmap snd . pTerm_internal
+
+pTerm1 :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Term
+pTerm1 = fmap snd . pTerm1_internal
+
+pScopedTerm :: [Token] -> Err Language.LambdaPi.Syntax.Abs.ScopedTerm
+pScopedTerm = fmap snd . pScopedTerm_internal
+
+pPattern :: [Token] -> Err Language.LambdaPi.Syntax.Abs.Pattern
+pPattern = fmap snd . pPattern_internal
 }
 
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Print.hs b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Print.hs
index 6d98a8f4..630e928b 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Print.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Print.hs
@@ -139,37 +139,37 @@ instance Print Double where
 
 instance Print Language.LambdaPi.Syntax.Abs.VarIdent where
   prt _ (Language.LambdaPi.Syntax.Abs.VarIdent i) = doc $ showString i
-instance Print Language.LambdaPi.Syntax.Abs.Program where
+instance Print (Language.LambdaPi.Syntax.Abs.Program' a) where
   prt i = \case
-    Language.LambdaPi.Syntax.Abs.AProgram commands -> prPrec i 0 (concatD [prt 0 commands])
+    Language.LambdaPi.Syntax.Abs.AProgram _ commands -> prPrec i 0 (concatD [prt 0 commands])
 
-instance Print Language.LambdaPi.Syntax.Abs.Command where
+instance Print (Language.LambdaPi.Syntax.Abs.Command' a) where
   prt i = \case
-    Language.LambdaPi.Syntax.Abs.CommandCheck term1 term2 -> prPrec i 0 (concatD [doc (showString "check"), prt 0 term1, doc (showString ":"), prt 0 term2])
-    Language.LambdaPi.Syntax.Abs.CommandCompute term1 term2 -> prPrec i 0 (concatD [doc (showString "compute"), prt 0 term1, doc (showString ":"), prt 0 term2])
+    Language.LambdaPi.Syntax.Abs.CommandCheck _ term1 term2 -> prPrec i 0 (concatD [doc (showString "check"), prt 0 term1, doc (showString ":"), prt 0 term2])
+    Language.LambdaPi.Syntax.Abs.CommandCompute _ term1 term2 -> prPrec i 0 (concatD [doc (showString "compute"), prt 0 term1, doc (showString ":"), prt 0 term2])
 
-instance Print [Language.LambdaPi.Syntax.Abs.Command] where
+instance Print [Language.LambdaPi.Syntax.Abs.Command' a] where
   prt _ [] = concatD []
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
 
-instance Print Language.LambdaPi.Syntax.Abs.Term where
+instance Print (Language.LambdaPi.Syntax.Abs.Term' a) where
   prt i = \case
-    Language.LambdaPi.Syntax.Abs.Var varident -> prPrec i 2 (concatD [prt 0 varident])
-    Language.LambdaPi.Syntax.Abs.Pi pattern_ term scopedterm -> prPrec i 0 (concatD [doc (showString "\928"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term, doc (showString ")"), doc (showString "\8594"), prt 0 scopedterm])
-    Language.LambdaPi.Syntax.Abs.Lam pattern_ scopedterm -> prPrec i 0 (concatD [doc (showString "\955"), prt 0 pattern_, doc (showString "."), prt 0 scopedterm])
-    Language.LambdaPi.Syntax.Abs.App term1 term2 -> prPrec i 1 (concatD [prt 1 term1, prt 2 term2])
-    Language.LambdaPi.Syntax.Abs.Product term1 term2 -> prPrec i 0 (concatD [prt 1 term1, doc (showString "\215"), prt 1 term2])
-    Language.LambdaPi.Syntax.Abs.Pair term1 term2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ")")])
-    Language.LambdaPi.Syntax.Abs.First term -> prPrec i 0 (concatD [doc (showString "\960\8321"), doc (showString "("), prt 0 term, doc (showString ")")])
-    Language.LambdaPi.Syntax.Abs.Second term -> prPrec i 0 (concatD [doc (showString "\960\8322"), doc (showString "("), prt 0 term, doc (showString ")")])
-    Language.LambdaPi.Syntax.Abs.Universe -> prPrec i 0 (concatD [doc (showString "\120140")])
-
-instance Print Language.LambdaPi.Syntax.Abs.ScopedTerm where
+    Language.LambdaPi.Syntax.Abs.Var _ varident -> prPrec i 2 (concatD [prt 0 varident])
+    Language.LambdaPi.Syntax.Abs.Pi _ pattern_ term scopedterm -> prPrec i 0 (concatD [doc (showString "\928"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term, doc (showString ")"), doc (showString "\8594"), prt 0 scopedterm])
+    Language.LambdaPi.Syntax.Abs.Lam _ pattern_ scopedterm -> prPrec i 0 (concatD [doc (showString "\955"), prt 0 pattern_, doc (showString "."), prt 0 scopedterm])
+    Language.LambdaPi.Syntax.Abs.App _ term1 term2 -> prPrec i 1 (concatD [prt 1 term1, prt 2 term2])
+    Language.LambdaPi.Syntax.Abs.Product _ term1 term2 -> prPrec i 0 (concatD [prt 1 term1, doc (showString "\215"), prt 1 term2])
+    Language.LambdaPi.Syntax.Abs.Pair _ term1 term2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ")")])
+    Language.LambdaPi.Syntax.Abs.First _ term -> prPrec i 0 (concatD [doc (showString "\960\8321"), doc (showString "("), prt 0 term, doc (showString ")")])
+    Language.LambdaPi.Syntax.Abs.Second _ term -> prPrec i 0 (concatD [doc (showString "\960\8322"), doc (showString "("), prt 0 term, doc (showString ")")])
+    Language.LambdaPi.Syntax.Abs.Universe _ -> prPrec i 0 (concatD [doc (showString "\120140")])
+
+instance Print (Language.LambdaPi.Syntax.Abs.ScopedTerm' a) where
   prt i = \case
-    Language.LambdaPi.Syntax.Abs.AScopedTerm term -> prPrec i 0 (concatD [prt 0 term])
+    Language.LambdaPi.Syntax.Abs.AScopedTerm _ term -> prPrec i 0 (concatD [prt 0 term])
 
-instance Print Language.LambdaPi.Syntax.Abs.Pattern where
+instance Print (Language.LambdaPi.Syntax.Abs.Pattern' a) where
   prt i = \case
-    Language.LambdaPi.Syntax.Abs.PatternWildcard -> prPrec i 0 (concatD [doc (showString "_")])
-    Language.LambdaPi.Syntax.Abs.PatternVar varident -> prPrec i 0 (concatD [prt 0 varident])
-    Language.LambdaPi.Syntax.Abs.PatternPair pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])
+    Language.LambdaPi.Syntax.Abs.PatternWildcard _ -> prPrec i 0 (concatD [doc (showString "_")])
+    Language.LambdaPi.Syntax.Abs.PatternVar _ varident -> prPrec i 0 (concatD [prt 0 varident])
+    Language.LambdaPi.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Skel.hs b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Skel.hs
index 35fb20ee..d4125cdf 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Skel.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Syntax/Skel.hs
@@ -19,33 +19,33 @@ transVarIdent :: Language.LambdaPi.Syntax.Abs.VarIdent -> Result
 transVarIdent x = case x of
   Language.LambdaPi.Syntax.Abs.VarIdent string -> failure x
 
-transProgram :: Language.LambdaPi.Syntax.Abs.Program -> Result
+transProgram :: Show a => Language.LambdaPi.Syntax.Abs.Program' a -> Result
 transProgram x = case x of
-  Language.LambdaPi.Syntax.Abs.AProgram commands -> failure x
+  Language.LambdaPi.Syntax.Abs.AProgram _ commands -> failure x
 
-transCommand :: Language.LambdaPi.Syntax.Abs.Command -> Result
+transCommand :: Show a => Language.LambdaPi.Syntax.Abs.Command' a -> Result
 transCommand x = case x of
-  Language.LambdaPi.Syntax.Abs.CommandCheck term1 term2 -> failure x
-  Language.LambdaPi.Syntax.Abs.CommandCompute term1 term2 -> failure x
+  Language.LambdaPi.Syntax.Abs.CommandCheck _ term1 term2 -> failure x
+  Language.LambdaPi.Syntax.Abs.CommandCompute _ term1 term2 -> failure x
 
-transTerm :: Language.LambdaPi.Syntax.Abs.Term -> Result
+transTerm :: Show a => Language.LambdaPi.Syntax.Abs.Term' a -> Result
 transTerm x = case x of
-  Language.LambdaPi.Syntax.Abs.Var varident -> failure x
-  Language.LambdaPi.Syntax.Abs.Pi pattern_ term scopedterm -> failure x
-  Language.LambdaPi.Syntax.Abs.Lam pattern_ scopedterm -> failure x
-  Language.LambdaPi.Syntax.Abs.App term1 term2 -> failure x
-  Language.LambdaPi.Syntax.Abs.Product term1 term2 -> failure x
-  Language.LambdaPi.Syntax.Abs.Pair term1 term2 -> failure x
-  Language.LambdaPi.Syntax.Abs.First term -> failure x
-  Language.LambdaPi.Syntax.Abs.Second term -> failure x
-  Language.LambdaPi.Syntax.Abs.Universe -> failure x
-
-transScopedTerm :: Language.LambdaPi.Syntax.Abs.ScopedTerm -> Result
+  Language.LambdaPi.Syntax.Abs.Var _ varident -> failure x
+  Language.LambdaPi.Syntax.Abs.Pi _ pattern_ term scopedterm -> failure x
+  Language.LambdaPi.Syntax.Abs.Lam _ pattern_ scopedterm -> failure x
+  Language.LambdaPi.Syntax.Abs.App _ term1 term2 -> failure x
+  Language.LambdaPi.Syntax.Abs.Product _ term1 term2 -> failure x
+  Language.LambdaPi.Syntax.Abs.Pair _ term1 term2 -> failure x
+  Language.LambdaPi.Syntax.Abs.First _ term -> failure x
+  Language.LambdaPi.Syntax.Abs.Second _ term -> failure x
+  Language.LambdaPi.Syntax.Abs.Universe _ -> failure x
+
+transScopedTerm :: Show a => Language.LambdaPi.Syntax.Abs.ScopedTerm' a -> Result
 transScopedTerm x = case x of
-  Language.LambdaPi.Syntax.Abs.AScopedTerm term -> failure x
+  Language.LambdaPi.Syntax.Abs.AScopedTerm _ term -> failure x
 
-transPattern :: Language.LambdaPi.Syntax.Abs.Pattern -> Result
+transPattern :: Show a => Language.LambdaPi.Syntax.Abs.Pattern' a -> Result
 transPattern x = case x of
-  Language.LambdaPi.Syntax.Abs.PatternWildcard -> failure x
-  Language.LambdaPi.Syntax.Abs.PatternVar varident -> failure x
-  Language.LambdaPi.Syntax.Abs.PatternPair pattern_1 pattern_2 -> failure x
+  Language.LambdaPi.Syntax.Abs.PatternWildcard _ -> failure x
+  Language.LambdaPi.Syntax.Abs.PatternVar _ varident -> failure x
+  Language.LambdaPi.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> failure x

From 01204891c1d824af38996b460c00dbcd4b4aa611 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Mon, 17 Jun 2024 19:49:34 +0300
Subject: [PATCH 2/2] Update workflow

---
 .github/workflows/haskell.yml | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

diff --git a/.github/workflows/haskell.yml b/.github/workflows/haskell.yml
index 8510c4dc..6b47778c 100644
--- a/.github/workflows/haskell.yml
+++ b/.github/workflows/haskell.yml
@@ -37,21 +37,12 @@ jobs:
             haskell/lambda-pi/src/Language/LambdaPi/Syntax/Lex.hs
             haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.hs
 
-      - name: Check Syntax files exist
-        if: steps.restore-syntax-files.outputs.cache-hit == 'true'
-        shell: bash
-        id: check-syntax-files
-        run: |
-          source scripts/lib.sh
-          check_syntax_files_exist
-          printf "SYNTAX_FILES_EXIST=$SYNTAX_FILES_EXIST\n" >> $GITHUB_OUTPUT
-
       - name: 🧰 Setup Stack
         uses: freckle/stack-action@v5
         with:
           stack-build-arguments: --pedantic
           stack-build-arguments-build: --dry-run
-          stack-build-arguments-test: --ghc-options -O2 ${{ steps.check-syntax-files.outputs.SYNTAX_FILES_EXIST == 'true' && ' ' || '--reconfigure --force-dirty --ghc-options -fforce-recomp' }}
+          stack-build-arguments-test: --ghc-options -O2 ${{ steps.restore-syntax-files.outputs.cache-hit == 'true' && ' ' || '--reconfigure --force-dirty --ghc-options -fforce-recomp' }}
 
       - name: Save Syntax files
         uses: actions/cache/save@v4