system F

almost done
pretty-printing
2024-02-29 09:52:08 -07:00 · 2024-02-27 14:48:02 -07:00 · 2024-02-27 07:56:25 -07:00 · 2024-02-27 06:14:02 -07:00 · 2024-02-27 05:12:19 -07:00 · 2024-02-26 18:18:02 -07:00
32 changed files with 1724 additions and 839 deletions
--- a/3
+++ b/3
@@ -1,10 +1,11 @@
+GHC_VERSION = $(shell ghc --numeric-version)
 HAPPY = happy
 HAPPY_OPTS = -a -g -c -i/tmp/t.info
 ALEX = alex
 ALEX_OPTS = -g

 SRC = src
-CABAL_BUILD = dist-newstyle/build/x86_64-osx/ghc-9.6.2/rlp-0.1.0.0/build
+CABAL_BUILD = $(shell ./find-build.cl)

 all: parsers lexers

--- a/examples/Core/factorial.cr
+++ b/examples/Core/factorial.cr
@@ -1,7 +1,9 @@
+fac : Int# -> Int#
 fac n = case (==#) n 0 of
    { <1> -> 1
    ; <0> -> *# n (fac (-# n 1))
    };

+main : IO ()
 main = fac 3;

--- a/find-build.cl
+++ b/find-build.cl
@@ -0,0 +1,8 @@
+#!/usr/bin/env sbcl --script
+
+(let* ((paths (directory "dist-newstyle/build/*/*/rlp-*/build/"))
+       (n (length paths)))
+  (cond ((< 1 n) (error ">1 build directories found. run `cabal clean`."))
+        ((< n 1) (error "no build directories found. this shouldn't happen lol"))
+        (t       (format t "~A" (car paths)))))
+
--- a/rlp.cabal
+++ b/rlp.cabal
@@ -32,6 +32,8 @@ library
                    , Core.HindleyMilner
                    , Control.Monad.Errorful
                    , Rlp.Syntax
+                    , Rlp.Syntax.Backstage
+                    , Rlp.Syntax.Types
                    -- , Rlp.Parse.Decls
                    , Rlp.Parse
                    , Rlp.Parse.Associate
@@ -42,10 +44,14 @@ library
                    , Data.Heap
                    , Data.Pretty
                    , Core.Parse
+                    , Core.Parse.Types
                    , Core.Lex
                    , Core2Core
                    , Rlp2Core
                    , Control.Monad.Utils
+                    , Misc
+                    , Misc.Lift1
+                    , Core.SystemF

    build-tool-depends: happy:happy, alex:alex

@@ -60,7 +66,7 @@ library
                    , data-default-class >= 0.1.2 && < 0.2
                    , hashable >= 1.4.3 && < 1.5
                    , mtl >= 2.3.1 && < 2.4
-                    , text >= 2.0.2 && < 2.1
+                    , text >= 2.0.2 && < 2.2
                    , unordered-containers >= 0.2.20 && < 0.3
                    , recursion-schemes >= 5.2.2 && < 5.3
                    , data-fix >= 0.3.2 && < 0.4
@@ -73,6 +79,8 @@ library
                    , effectful-core ^>=2.3.0.0
                    , deriving-compat ^>=0.6.0
                    , these >=0.2 && <2.0
+                    , free >=5.2
+                    , bifunctors >=5.2

    hs-source-dirs:   src
    default-language: GHC2021
@@ -86,6 +94,7 @@ library
        DerivingVia
        StandaloneDeriving
        DerivingStrategies
+        BlockArguments

 executable rlpc
    import:           warnings
@@ -99,7 +108,7 @@ executable rlpc
                 , mtl >= 2.3.1 && < 2.4
                 , unordered-containers >= 0.2.20 && < 0.3
                 , lens >=5.2.3 && <6.0
-                 , text >= 2.0.2 && < 2.1
+                 , text >= 2.0.2 && < 2.2

    hs-source-dirs:   app
    default-language: GHC2021
@@ -116,8 +125,10 @@ test-suite rlp-test
                 , QuickCheck
                 , hspec            ==2.*
                 , microlens
+                 , lens >=5.2.3 && <6.0
    other-modules: Arith
                 , GMSpec
                 , Core.HindleyMilnerSpec
+                 , Compiler.TypesSpec
    build-tool-depends: hspec-discover:hspec-discover

--- a/src/Compiler/JustRun.hs
+++ b/src/Compiler/JustRun.hs
@@ -12,13 +12,14 @@ module Compiler.JustRun
    , justParseCore
    , justTypeCheckCore
    , justHdbg
+    , makeItPretty, makeItPretty'
    )
    where
 ----------------------------------------------------------------------------------
 import Core.Lex
 import Core.Parse
 import Core.HindleyMilner
-import Core.Syntax                      (Program')
+import Core.Syntax
 import Compiler.RLPC
 import Control.Arrow                    ((>>>))
 import Control.Monad                    ((>=>), void)
@@ -30,6 +31,7 @@ import System.IO
 import GM
 import Rlp.Parse
 import Rlp2Core
+import Data.Pretty
 ----------------------------------------------------------------------------------

 justHdbg :: String -> IO GmState
@@ -42,16 +44,22 @@ justLexCore s = lexCoreR (T.pack s)
              & mapped . each %~ extract
              & rlpcToEither

-justParseCore :: String -> Either [MsgEnvelope RlpcError] Program'
+justParseCore :: String -> Either [MsgEnvelope RlpcError] (Program Var)
 justParseCore s = parse (T.pack s)
                & rlpcToEither
-    where parse = lexCoreR >=> parseCoreProgR
+    where parse = lexCoreR @Identity >=> parseCoreProgR

 justTypeCheckCore :: String -> Either [MsgEnvelope RlpcError] Program'
 justTypeCheckCore s = typechk (T.pack s)
                    & rlpcToEither
    where typechk = lexCoreR >=> parseCoreProgR >=> checkCoreProgR

+makeItPretty :: (Pretty a) => Either e a -> Either e Doc
+makeItPretty = fmap pretty
+
+makeItPretty' :: (Pretty (WithTerseBinds a)) => Either e a -> Either e Doc
+makeItPretty' = fmap (pretty . WithTerseBinds)
+
 rlpcToEither :: RLPC a -> Either [MsgEnvelope RlpcError] a
 rlpcToEither r = case evalRLPC def r of
    (Just a,   _) -> Right a
--- a/src/Compiler/RLPC.hs
+++ b/src/Compiler/RLPC.hs
@@ -27,7 +27,7 @@ module Compiler.RLPC
    -- ** Lenses
    , rlpcLogFile, rlpcDFlags, rlpcEvaluator, rlpcInputFiles, rlpcLanguage
    -- * Misc. MTL-style functions
-    , liftErrorful, hoistRlpcT
+    , liftErrorful, liftMaybe, hoistRlpcT
    -- * Misc. Rlpc Monad -related types
    , RLPCOptions(RLPCOptions), IsRlpcError(..), RlpcError(..)
    , MsgEnvelope(..), Severity(..)
@@ -108,6 +108,9 @@ evalRLPCT opt r = runRLPCT r
 liftErrorful :: (Monad m, IsRlpcError e) => ErrorfulT (MsgEnvelope e) m a -> RLPCT m a
 liftErrorful e = RLPCT $ lift (fmap liftRlpcError `mapErrorful` e)

+liftMaybe :: (Monad m) => Maybe a -> RLPCT m a
+liftMaybe m = RLPCT . lift . ErrorfulT . pure $ (m, [])
+
 hoistRlpcT :: (forall a. m a -> n a)
         -> RLPCT m a -> RLPCT n a
 hoistRlpcT f rma = RLPCT $ ReaderT $ \opt ->
@@ -220,9 +223,9 @@ docRlpcErr msg = header
                rule = repeat (ttext . Ansi.blue . Ansi.bold $ "|")
                srclines = ["", "<problematic source code>", ""]
        filename = msgColour "<input>"
-        pos = msgColour $ tshow (msg ^. msgSpan . srcspanLine)
+        pos = msgColour $ tshow (msg ^. msgSpan . srcSpanLine)
                       <> ":"
-                       <> tshow (msg ^. msgSpan . srcspanColumn)
+                       <> tshow (msg ^. msgSpan . srcSpanColumn)

        header = ttext $ filename <> msgColour ":" <> pos <> msgColour ": "
                        <> errorColour "error" <> msgColour ":"
--- a/src/Compiler/RlpcError.hs
+++ b/src/Compiler/RlpcError.hs
@@ -14,6 +14,9 @@ module Compiler.RlpcError
    -- * Located Comonad
    , Located(..)
    , SrcSpan(..)
+
+    -- * Common error messages
+    , undefinedVariableErr
    )
    where
 ----------------------------------------------------------------------------------
@@ -74,3 +77,8 @@ debugMsg tag e = MsgEnvelope
    , _msgSeverity = SevDebug tag
    }

+undefinedVariableErr :: Text -> RlpcError
+undefinedVariableErr n = Text
+    [ "Variable not in scope: `" <> n <> "'."
+    ]
+
--- a/src/Compiler/Types.hs
+++ b/src/Compiler/Types.hs
@@ -1,33 +1,81 @@
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances, QuantifiedConstraints #-}
+{-# LANGUAGE PatternSynonyms #-}
 module Compiler.Types
    ( SrcSpan(..)
-    , srcspanLine, srcspanColumn, srcspanAbs, srcspanLen
+    , srcSpanLine, srcSpanColumn, srcSpanAbs, srcSpanLen
+    , pattern (:<$)
    , Located(..)
+    , HasLocation(..)
    , _Located
-    , located
-    , nolo
-    , (<<~), (<~>), (<#>)
+    , nolo, nolo'
+
+    , (<~>), (~>), (~~>), (<~~)
+
+    , comb2, comb3, comb4
+    , lochead

    -- * Re-exports
-    , Comonad
+    , Comonad(extract)
    , Apply
    , Bind
    )
    where
 --------------------------------------------------------------------------------
+import Language.Haskell.TH.Syntax   (Lift)
+
 import Control.Comonad
+import Control.Comonad.Cofree
+import Control.Comonad.Trans.Cofree qualified as Trans.Cofree
+import Control.Comonad.Trans.Cofree (CofreeF)
 import Data.Functor.Apply
 import Data.Functor.Bind
-import Control.Lens             hiding ((<<~))
-import Language.Haskell.TH.Syntax   (Lift)
+import Data.Functor.Compose
+import Data.Functor.Foldable
+import Data.Semigroup.Foldable
+import Data.Fix                     hiding (cata, ana)
+import Data.Kind
+import Control.Lens                 hiding ((<<~), (:<))
+
+import Data.List.NonEmpty           (NonEmpty)
+import Data.Function                (on)
 --------------------------------------------------------------------------------

 -- | Token wrapped with a span (line, column, absolute, length)
 data Located a = Located SrcSpan a
    deriving (Show, Lift, Functor)

-located :: Lens (Located a) (Located b) a b
-located = lens extract ($>)
+data Floc f = Floc SrcSpan (f (Floc f))
+
+pattern (:<$) :: a -> f b -> Trans.Cofree.CofreeF f a b
+pattern a :<$ b = a Trans.Cofree.:< b
+
+(<~>) :: a -> b -> SrcSpan
+(<~>) = undefined
+
+infixl 5 <~>
+
+-- (~>) :: (CanGet k, CanSet k', HasLocation k a, HasLocation k' b)
+--      => a -> b -> b
+-- a ~> b = 
+(~>) = undefined
+
+infixl 4 ~>
+
+-- (~~>) :: (CanGet k, HasLocation k a, CanSet k', HasLocation k' b)
+--       => (a -> b) -> a -> b
+-- (~~>) :: (f SrcSpan -> b) -> Cofree f SrcSpan -> Cofree f SrcSpan
+-- f ~~> (ss :< as) = ss :< f as
+(~~>) = undefined
+
+infixl 3 ~~>
+
+-- (<~~) :: (GetLocation a, HasLocation b) => (a -> b) -> a -> b
+-- a <~~ b = a b & location <>~ srcspan b
+(<~~) = undefined
+
+infixr 2 <~~

 instance Apply Located where
    liftF2 f (Located sa p) (Located sb q)
@@ -47,53 +95,136 @@ data SrcSpan = SrcSpan
    !Int -- ^ Column
    !Int -- ^ Absolute
    !Int -- ^ Length
-    deriving (Show, Lift)
+    deriving (Show, Eq, Lift)

 tupling :: Iso' SrcSpan (Int, Int, Int, Int)
 tupling = iso (\ (SrcSpan a b c d) -> (a,b,c,d))
              (\ (a,b,c,d) -> SrcSpan a b c d)

-srcspanLine, srcspanColumn, srcspanAbs, srcspanLen :: Lens' SrcSpan Int
-srcspanLine = tupling . _1
-srcspanColumn = tupling . _2
-srcspanAbs = tupling . _3
-srcspanLen = tupling . _4
+srcSpanLine, srcSpanColumn, srcSpanAbs, srcSpanLen :: Lens' SrcSpan Int
+srcSpanLine = tupling . _1
+srcSpanColumn = tupling . _2
+srcSpanAbs = tupling . _3
+srcSpanLen = tupling . _4

 -- | debug tool
 nolo :: a -> Located a
 nolo = Located (SrcSpan 0 0 0 0)

+nolo' :: f (Cofree f SrcSpan) -> Cofree f SrcSpan
+nolo' as = SrcSpan 0 0 0 0 :< as
+
 instance Semigroup SrcSpan where
+    -- multiple identities? what are the consequences of this...?
+    SrcSpan _ _ _ 0 <> SrcSpan l c a s = SrcSpan l c a s
+    SrcSpan l c a s <> SrcSpan _ _ _ 0 = SrcSpan l c a s
+
    SrcSpan la ca aa sa <> SrcSpan lb cb ab sb = SrcSpan l c a s where
        l = min la lb
        c = min ca cb
        a = min aa ab
        s = case aa `compare` ab of
            EQ -> max sa sb
-            LT -> max sa (ab + lb - aa)
-            GT -> max sb (aa + la - ab)
+            LT -> max sa (ab + sb - aa)
+            GT -> max sb (aa + sa - ab)

-- | A synonym for '(<<=)' with a tighter precedence and left-associativity for
-- use with '(<~>)' in a sort of, comonadic pseudo-applicative style.
+--------------------------------------------------------------------------------

-(<<~) :: (Comonad w) => (w a -> b) -> w a -> w b
-(<<~) = (<<=)
+data GetOrSet = Get | Set | GetSet

-infixl 4 <<~
+class CanGet (k :: GetOrSet)
+class CanSet (k :: GetOrSet) where

-- | Similar to '(<*>)', but with a cokleisli arrow.
+instance CanGet Get
+instance CanGet GetSet
+instance CanSet Set
+instance CanSet GetSet

-(<~>) :: (Comonad w, Bind w) => w (w a -> b) -> w a -> w b
-mc <~> ma = mc >>- \f -> ma =>> f
+data GetSetLens (k :: GetOrSet) s t a b :: Type where
+    Getter_      :: (s -> a)             -> GetSetLens Get s t a b
+    Setter_      :: ((a -> b) -> s -> t) -> GetSetLens Set s t a b
+    GetterSetter :: (CanGet k', CanSet k')
+                 => (s -> a) -> (s -> b -> t) -> GetSetLens k' s t a b

-infixl 4 <~>
+type GetSetLens' k s a = GetSetLens k s s a a

-- this is getting silly
+class HasLocation k s | s -> k where
+    -- location :: (Access k f, Functor f) => LensLike' f s SrcSpan
+    getSetLocation :: GetSetLens' k s SrcSpan

-(<#>) :: (Functor f) => f (a -> b) -> a -> f b
-fab <#> a = fmap ($ a) fab
+type family Access (k :: GetOrSet) f where
+    Access GetSet f = Functor f
+    Access Set f = Settable f
+    Access Get f = (Functor f, Contravariant f)

-infixl 4 <#>
+instance HasLocation GetSet SrcSpan where
+    getSetLocation = GetterSetter id (flip const)
+    -- location = fromGetSetLens getSetLocation
+
+instance (CanSet k, HasLocation k a) => HasLocation Set (r -> a) where
+    getSetLocation = Setter_ $ \ss ra r -> ra r & fromSet getSetLocation %~ ss
+    -- location = fromSet getSetLocation
+
+instance (HasLocation k a) => HasLocation k (Cofree f a) where
+    getSetLocation = case getSetLocation @_ @a of
+        Getter_ sa -> Getter_ $ \ (s :< _) -> sa s
+        Setter_ abst -> Setter_ $ \ss (s :< as) -> abst ss s :< as
+        GetterSetter sa sbt -> GetterSetter sa' sbt' where
+            sa' (s :< _) = sa s
+            sbt' (s :< as) b = sbt s b :< as
+
+location :: (Access k f, Functor f, HasLocation k s)
+         => LensLike' f s SrcSpan
+location = fromGetSetLens getSetLocation
+
+fromGetSetLens :: (Access k f, Functor f) => GetSetLens' k s a -> LensLike' f s a
+fromGetSetLens gsl = case gsl of
+    Getter_ sa          -> to sa
+    Setter_ abst        -> setting abst
+    GetterSetter sa sbt -> lens sa sbt
+
+fromGet :: (CanGet k) => GetSetLens k s t a b -> Getter s a
+fromGet (Getter_ sa)        = to sa
+fromGet (GetterSetter sa _) = to sa
+
+fromSet :: (CanSet k) => GetSetLens k s t a b -> Setter s t a b
+fromSet (Setter_ abst)        = setting abst
+fromSet (GetterSetter sa sbt) = lens sa sbt
+
+fromGetSet :: (CanGet k, CanSet k) => GetSetLens k s t a b -> Lens s t a b
+fromGetSet (GetterSetter sa sbt) = lens sa sbt
+
+--------------------------------------------------------------------------------
+
+comb2 :: (Functor f, Semigroup m)
+      => (Cofree f m -> Cofree f m -> f (Cofree f m))
+      -> Cofree f m -> Cofree f m -> Cofree f m
+comb2 f a b = ss :< f a b
+    where ss = a `mextract` b
+
+comb3 :: (Functor f, Semigroup m)
+      => (Cofree f m -> Cofree f m -> Cofree f m -> f (Cofree f m))
+      -> Cofree f m -> Cofree f m -> Cofree f m -> Cofree f m
+comb3 f a b c = ss :< f a b c
+    where ss = a `mapply` b `mextract` c
+
+comb4 :: (Functor f, Semigroup m)
+      => (Cofree f m -> Cofree f m -> Cofree f m -> Cofree f m
+         -> f (Cofree f m))
+      -> Cofree f m -> Cofree f m -> Cofree f m -> Cofree f m -> Cofree f m
+comb4 f a b c d = ss :< f a b c d
+    where ss = a `mapply` b `mapply` c `mextract` d
+
+mextract :: (Comonad w, Semigroup m) => w m -> w m -> m
+mextract = (<>) `on` extract
+
+mapply :: (Comonad w, Semigroup m) => w m -> w m -> w m
+mapply a b = b <&> (<> extract a)
+
+lochead :: Functor f
+        => (f SrcSpan -> f SrcSpan) -> Located (f SrcSpan) -> Cofree f SrcSpan
+lochead afs (Located ss fss) = ss :< unwrap (lochead afs $ Located ss fss)
+
+--------------------------------------------------------------------------------

 makePrisms ''Located
-
--- a/src/Core.hs
+++ b/src/Core.hs
@@ -1,6 +1,5 @@
 module Core
    ( module Core.Syntax
-    , parseCore
    , parseCoreProg
    , parseCoreExpr
    , lexCore
--- a/src/Core/Examples.hs
+++ b/src/Core/Examples.hs
@@ -10,12 +10,9 @@ import Core.Syntax
 import Core.TH
 ----------------------------------------------------------------------------------

-- fac3 = undefined
-- sumList = undefined
-- constDivZero = undefined
-- idCase = undefined
+letRecExample = undefined

---
+{--

 letrecExample :: Program'
 letrecExample = [coreProg|
--- a/src/Core/HindleyMilner.hs
+++ b/src/Core/HindleyMilner.hs
@@ -35,6 +35,12 @@ import Text.Printf
 import Core.Syntax
 ----------------------------------------------------------------------------------

+infer = undefined
+check = undefined
+checkCoreProg = undefined
+checkCoreProgR = undefined
+checkCoreExprR = undefined
+
 -- | Annotated typing context -- I have a feeling we're going to want this in the
 -- future.
 type Context b = [(b, Type)]
@@ -74,6 +80,8 @@ instance IsRlpcError TypeError where
 -- throw any number of fatal or nonfatal errors. Run with @runErrorful@.
 type HMError = Errorful TypeError

+{--
+
 -- | Assert that an expression unifies with a given type
 --
 -- >>> let e = [coreProg|3|]
@@ -276,3 +284,4 @@ demoContext =
    , ("False", TyCon "Bool")
    ]

+--}
--- a/src/Core/Lex.x
+++ b/src/Core/Lex.x
@@ -78,7 +78,7 @@ rlp :-
    "{"                     { constTok TokenLBrace }
    "}"                     { constTok TokenRBrace }
    ";"                     { constTok TokenSemicolon }
-    "::"                    { constTok TokenHasType }
+    ":"                     { constTok TokenHasType }
    "@"                     { constTok TokenTypeApp }
    "{-#"                   { constTok TokenLPragma `andBegin` pragma }

--- a/src/Core/Parse.y
+++ b/src/Core/Parse.y
@@ -5,14 +5,12 @@ Description : Parser for the Core language
 -}
 {-# LANGUAGE OverloadedStrings, ViewPatterns #-}
 module Core.Parse
-    ( parseCore
-    , parseCoreExpr
+    ( parseCoreExpr
    , parseCoreExprR
    , parseCoreProg
    , parseCoreProgR
    , module Core.Lex -- temp convenience
    , SrcError
-    , Module
    )
    where

@@ -32,19 +30,19 @@ import Data.Text.IO         qualified as TIO
 import Data.Text            (Text)
 import Data.Text            qualified as T
 import Data.HashMap.Strict  qualified as H
+
+import Core.Parse.Types
 }

-%name parseCore Module
 %name parseCoreExpr StandaloneExpr
 %name parseCoreProg StandaloneProgram
 %tokentype { Located CoreToken }
 %error { parseError }
-%monad { RLPC } { happyBind } { happyPure }
+%monad { P }

 %token
      let             { Located _ TokenLet }
      letrec          { Located _ TokenLetrec }
-      module          { Located _ TokenModule }
      where           { Located _ TokenWhere }
      case            { Located _ TokenCase }
      of              { Located _ TokenOf }
@@ -68,29 +66,27 @@ import Data.HashMap.Strict  qualified as H
      '{-#'           { Located _ TokenLPragma }
      '#-}'           { Located _ TokenRPragma }
      ';'             { Located _ TokenSemicolon }
-      '::'            { Located _ TokenHasType }
+      ':'             { Located _ TokenHasType }
      eof             { Located _ TokenEOF }

-%%
+%right '->'

-Module          :: { Module Name }
-Module          : module conname where Program Eof { Module (Just ($2, [])) $4 }
-                | Program Eof                      { Module Nothing $1 }
+%%

 Eof             :: { () }
 Eof             : eof           { () }
                | error         { () }

-StandaloneProgram :: { Program Name }
+StandaloneProgram :: { Program Var }
 StandaloneProgram : Program eof                 { $1 }

-Program         :: { Program Name }
-Program         : ScTypeSig ';' Program         { insTypeSig $1 $3 }
-                | ScTypeSig OptSemi             { singletonTypeSig $1 }
-                | ScDef     ';' Program         { insScDef $1 $3 }
-                | ScDef     OptSemi             { singletonScDef $1 }
-                | TLPragma  Program             {% doTLPragma $1 $2 }
-                | TLPragma                      {% doTLPragma $1 mempty }
+Program         :: { Program Var }
+                : TypedScDef ';' Program    { $3 & insTypeSig (fst $1)
+                                                 & insScDef (snd $1) }
+                | TypedScDef OptSemi        { mempty & insTypeSig (fst $1)
+                                                     & insScDef (snd $1) }
+                | TLPragma Program          {% doTLPragma $1 $2 }
+                | TLPragma                  {% doTLPragma $1 mempty }

 TLPragma        :: { Pragma }
                : '{-#' Words '#-}'             { Pragma $2 }
@@ -104,140 +100,152 @@ OptSemi         : ';'                           { () }
                | {- epsilon -}                 { () }

 ScTypeSig       :: { (Name, Type) }
-ScTypeSig       : Var '::' Type                 { ($1,$3) }
+ScTypeSig       : Id ':' Type                   { ($1, $3) }

-ScDefs          :: { [ScDef Name] }
-ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
-                | ScDef ';'                     { [$1] }
-                | ScDef                         { [$1] }
+TypedScDef      :: { (Var, ScDef Var) }
+                : Id ':' Type ';' Id ParList '=' Expr
+                            { (MkVar $1 $3, mkTypedScDef $1 $3 $5 $6 $8) }

-ScDef           :: { ScDef Name }
-ScDef           : Var ParList '=' Expr          { ScDef $1 $2 $4 }
-                -- hack to allow constructors to be compiled into scs
-                | Con ParList '=' Expr          { ScDef $1 $2 $4 }
+-- ScDefs          :: { [ScDef PsName] }
+-- ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
+--                 | ScDef ';'                     { [$1] }
+--                 | ScDef                         { [$1] }
+-- 
+-- ScDef           :: { ScDef PsName }
+-- ScDef           : Id ParList '=' Expr   { ScDef (Left $1) $2
+--                                                 ($4 & binders %~ Right) }

 Type            :: { Type }
-Type            : Type1                         { $1 }
+                : TypeApp '->' TypeApp              { $1 :-> $3 }
+                | TypeApp                         { $1 }
+
+TypeApp         :: { Type }
+                : TypeApp Type1                 { TyApp $1 $2 }
+                | Type1                         { $1 }
+
+-- do we want to allow symbolic names for tyvars and tycons?

 Type1           :: { Type }
 Type1           : '(' Type ')'                  { $2 }
-                | Type1 '->' Type               { $1 :-> $3 }
-                -- do we want to allow symbolic names for tyvars and tycons?
                | varname                       { TyVar $1 }
-                | conname                       { TyCon $1 }
+                | conname                       { if $1 == "Type"
+                                                    then TyKindType else TyCon $1 }

-ParList         :: { [Name] }
-ParList         : Var ParList                   { $1 : $2 }
-                | {- epsilon -}                 { [] }
+ParList      :: { [Name] }
+ParList      : varname ParList            { $1 : $2 }
+             | {- epsilon -}                 { [] }

-StandaloneExpr  :: { Expr Name }
+StandaloneExpr  :: { Expr Var }
 StandaloneExpr  : Expr eof                      { $1 }

-Expr            :: { Expr Name }
+Expr            :: { Expr Var }
 Expr            : LetExpr                       { $1 }
                | 'λ' Binders '->' Expr         { Lam $2 $4 }
                | Application                   { $1 }
                | CaseExpr                      { $1 }
                | Expr1                         { $1 }

-LetExpr         :: { Expr Name }
+LetExpr         :: { Expr Var }
 LetExpr         : let    '{'   Bindings '}'    in Expr { Let NonRec $3 $6 }
                | letrec '{'   Bindings '}'    in Expr { Let Rec $3 $6 }

-Binders         :: { [Name] }
+Binders         :: { [Var] }
 Binders         : Var Binders                  { $1 : $2 }
                | Var                          { [$1] }

-Application     :: { Expr Name }
-Application     : Expr1 AppArgs                { foldl' App $1 $2 }
+Application     :: { Expr Var }
+Application     : Application AppArg           { App $1 $2 }
+                | Expr1       AppArg           { App $1 $2 }

-AppArgs         :: { [Expr Name] }
-AppArgs         : Expr1 AppArgs                 { $1 : $2 }
-                | Expr1                         { [$1] }
+AppArg          :: { Expr Var }
+                : '@' Type1                     { Type $2 }
+                | Expr1                         { $1 }

-CaseExpr        :: { Expr Name }
+CaseExpr        :: { Expr Var }
 CaseExpr        : case Expr of '{' Alters '}'   { Case $2 $5 }

-Alters          :: { [Alter Name] }
+Alters          :: { [Alter Var] }
 Alters          : Alter ';' Alters              { $1 : $3 }
                | Alter ';'                     { [$1] }
                | Alter                         { [$1] }

-Alter           :: { Alter Name }
-Alter           : alttag ParList '->' Expr      { Alter (AltTag  $1) $2 $4 }
-                | Con    ParList '->' Expr      { Alter (AltData $1) $2 $4 }
+Alter           :: { Alter Var }
+Alter           : alttag  AltParList '->' Expr     { Alter (AltTag  $1) $2 $4 }
+                | conname AltParList '->' Expr     { Alter (AltData $1) $2 $4 }

-Expr1           :: { Expr Name }
+AltParList      :: { [Var] }
+                : Var AltParList                { $1 : $2 }
+                | {- epsilon -}                 { [] }
+
+Expr1           :: { Expr Var }
 Expr1           : litint                        { Lit $ IntL $1 }
                | Id                            { Var $1 }
                | PackCon                       { $1 }
                | '(' Expr ')'                  { $2 }

-PackCon         :: { Expr Name }
+PackCon         :: { Expr Var }
 PackCon         : pack '{' litint litint '}'    { Con $3 $4 }

-Bindings        :: { [Binding Name] }
+Bindings        :: { [Binding Var] }
 Bindings        : Binding ';' Bindings          { $1 : $3 }
                | Binding ';'                   { [$1] }
                | Binding                       { [$1] }

-Binding         :: { Binding Name }
+Binding         :: { Binding Var }
 Binding         : Var '=' Expr                  { $1 := $3 }

 Id              :: { Name }
-Id              : Var                                { $1 }
-                | Con                                { $1 }
+                : varname                           { $1 }
+                | conname                           { $1 }

-Var             :: { Name }
-Var             : varname                           { $1 }
-                | varsym                            { $1 }
-
-Con             :: { Name }
-Con             : conname                           { $1 }
-                | consym                            { $1 }
+Var             :: { Var }
+Var             : '(' varname ':' Type ')'          { MkVar $2 $4 }

 {

-parseError :: [Located CoreToken] -> RLPC a
+parseError :: [Located CoreToken] -> P a
 parseError (Located _ t : _) =
    error $ "<line>" <> ":" <> "<col>"
         <> ": parse error at token `" <> show t <> "'"

-{-# WARNING parseError "unimpl" #-}
-
-exprPragma :: [String] -> RLPC (Expr Name)
+exprPragma :: [String] -> RLPC (Expr Var)
 exprPragma ("AST" : e) = undefined
 exprPragma _           = undefined

-{-# WARNING exprPragma "unimpl" #-}
-
-astPragma :: [String] -> RLPC (Expr Name)
+astPragma :: [String] -> RLPC (Expr Var)
 astPragma _ = undefined

-{-# WARNING astPragma "unimpl" #-}
+-- insTypeSig :: (Hashable b) => (b, Type) -> Program b -> Program b
+-- insTypeSig ts = programTypeSigs %~ uncurry H.insert ts

-insTypeSig :: (Hashable b) => (b, Type) -> Program b -> Program b
-insTypeSig ts = programTypeSigs %~ uncurry H.insert ts
+insTypeSig :: Var -> Program Var -> Program Var
+insTypeSig w@(MkVar _ t) = programTypeSigs %~ H.insert w t

-singletonTypeSig :: (Hashable b) => (b, Type) -> Program b
-singletonTypeSig ts = insTypeSig ts mempty
+-- singletonTypeSig :: (Hashable b) => (b, Type) -> Program b
+-- singletonTypeSig ts = insTypeSig ts mempty

 insScDef :: (Hashable b) => ScDef b -> Program b -> Program b
 insScDef sc = programScDefs %~ (sc:)

-singletonScDef :: (Hashable b) => ScDef b -> Program b
-singletonScDef sc = insScDef sc mempty
+-- singletonScDef :: (Hashable b) => ScDef b -> Program b
+-- singletonScDef sc = insScDef sc mempty

-parseCoreExprR :: (Monad m) => [Located CoreToken] -> RLPCT m Expr'
-parseCoreExprR = hoistRlpcT generalise . parseCoreExpr
+parseCoreExprR :: (Monad m) => [Located CoreToken] -> RLPCT m (Expr Var)
+parseCoreExprR = liftMaybe . snd . flip runP def . parseCoreExpr

-parseCoreProgR :: forall m. (Monad m) => [Located CoreToken] -> RLPCT m Program'
-parseCoreProgR = ddumpast <=< (hoistRlpcT generalise . parseCoreProg)
-    where
-        ddumpast :: Program' -> RLPCT m Program'
-        ddumpast p = do
-            addDebugMsg "dump-parsed-core" . show $ p
-            pure p
+parseCoreProgR :: forall m. (Monad m)
+               => [Located CoreToken] -> RLPCT m (Program Var)
+parseCoreProgR s = do
+    let p = runP (parseCoreProg s) def
+    case p of
+        (st, Just a) -> do
+            ddumpast a
+            pure a
+  where
+    ddumpast :: Show a => Program a -> RLPCT m (Program a)
+    ddumpast p = do
+        addDebugMsg "dump-parsed-core" . show $ p
+        pure p

 happyBind :: RLPC a -> (a -> RLPC b) -> RLPC b
 happyBind m k = m >>= k
@@ -245,7 +253,7 @@ happyBind m k = m >>= k
 happyPure :: a -> RLPC a
 happyPure a = pure a

-doTLPragma :: Pragma -> Program' -> RLPC Program'
+doTLPragma :: Pragma -> Program Var -> P (Program Var)
 -- TODO: warn unrecognised pragma
 doTLPragma (Pragma []) p = pure p

--- a/src/Core/Parse/Types.hs
+++ b/src/Core/Parse/Types.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Core.Parse.Types
+    ( P(..)
+    , psTyVars
+    , def
+    , PsName
+    , mkTypedScDef
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Applicative
+import Control.Monad
+import Control.Monad.State
+import Data.Default
+import Data.Maybe
+import Data.Tuple               (swap)
+
+import Control.Lens
+
+import Core.Syntax
+--------------------------------------------------------------------------------
+
+newtype P a = P { runP :: PState -> (PState, Maybe a) }
+    deriving Functor
+
+data PState = PState
+    { _psTyVars :: [(Name, Kind)]
+    }
+
+instance Applicative P where
+    pure a = P (, Just a)
+
+    P pf <*> P pa = P \st ->
+        let (st',mf) = pf st
+            (st'',ma) = pa st'
+        in (st'', mf <*> ma)
+
+instance Monad P where
+    P pa >>= k = P \st ->
+        let (st',ma) = pa st
+        in case ma of
+            Just a -> runP (k a) st'
+            Nothing -> (st', Nothing)
+
+instance MonadState PState P where
+    state = P . fmap ((_2 %~ Just) . review swapped)
+
+instance Default PState where
+    def = undefined
+
+makeLenses ''PState
+
+type PsName = Either Name Var
+
+--------------------------------------------------------------------------------
+
+mkTypedScDef :: Name -> Type -> Name -> [Name] -> Expr Var -> ScDef Var
+mkTypedScDef nt tt n as e | nt == n = ScDef n' as' e
+    where
+        n' = MkVar n tt
+        as' = zipWith MkVar as (tt ^.. arrowStops)
+
--- a/src/Core/Syntax.hs
+++ b/src/Core/Syntax.hs
@@ -7,39 +7,38 @@ Description : Core ASTs and the like
 {-# LANGUAGE TemplateHaskell #-}
 -- for recursion-schemes
 {-# LANGUAGE DeriveTraversable, TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 module Core.Syntax
-    ( Expr(..)
-    , ExprF(..)
-    , ExprF'(..)
-    , Type(..)
-    , pattern TyInt
-    , Lit(..)
-    , pattern (:$)
-    , pattern (:@)
-    , pattern (:->)
-    , Binding(..)
-    , AltCon(..)
-    , pattern (:=)
-    , Rec(..)
-    , Alter(..)
-    , Name
-    , Tag
-    , ScDef(..)
-    , Module(..)
-    , Program(..)
-    , Program'
+    (
+    -- * Core AST
+      ExprF(..), ExprF'
+    , ScDef(..), ScDef'
+    , Program(..), Program'
+    , Type(..), Kind, pattern (:->), pattern TyInt
+    , AlterF(..), Alter(..), Alter', AltCon(..)
+    , pattern Binding, pattern Alter
+    , Rec(..), Lit(..)
    , Pragma(..)
-    , unliftScDef
-    , programScDefs
-    , programTypeSigs
-    , programDataTags
-    , Expr'
-    , ScDef'
-    , Alter'
-    , Binding'
-    , HasRHS(_rhs)
-    , HasLHS(_lhs)
-    , Pretty(pretty)
+    -- ** Variables and identifiers
+    , Name, Var(..), Tag, pattern (:^)
+    , Binding, BindingF(..), pattern (:=), pattern (:$)
+    , type Binding'
+    -- ** Working with the fixed point of ExprF
+    , Expr, Expr'
+    , pattern Con, pattern Var, pattern App, pattern Lam, pattern Let
+    , pattern Case, pattern Type, pattern Lit
+
+    -- * Pretty-printing
+    , Pretty(pretty), WithTerseBinds(..)
+
+    -- * Optics
+    , programScDefs, programTypeSigs, programDataTags
+    , formalising
+    , HasRHS(_rhs), HasLHS(_lhs)
+    , _BindingF, _MkVar
+    -- ** Classy optics
+    , HasBinders(..), HasArrowStops(..), HasApplicants1(..), HasApplicants(..)
    )
    where
 ----------------------------------------------------------------------------------
@@ -47,109 +46,183 @@ import Data.Coerce
 import Data.Pretty
 import Data.List                    (intersperse)
 import Data.Function                ((&))
-import Data.Functor.Foldable
-import Data.Functor.Foldable.TH     (makeBaseFunctor)
 import Data.String
 import Data.HashMap.Strict          (HashMap)
 import Data.HashMap.Strict          qualified as H
 import Data.Hashable
+import Data.Foldable                (traverse_)
+import Data.Functor
+import Data.Monoid
+import Data.Functor.Classes
 import Data.Text                    qualified as T
 import Data.Char
 import Data.These
-import Data.Bifoldable              (bifoldr)
 import GHC.Generics                 (Generic, Generically(..))
+import Text.Show.Deriving
+import Data.Eq.Deriving
+import Data.Kind                    qualified
+
+import Data.Fix                     hiding (cata, ana)
+import Data.Bifunctor               (Bifunctor(..))
+import Data.Bifoldable              (bifoldr, Bifoldable(..))
+import Data.Bifunctor.TH
+import Data.Bitraversable
+import Data.Functor.Foldable
+import Data.Functor.Foldable.TH     (makeBaseFunctor)
+
 -- Lift instances for the Core quasiquoters
-import Language.Haskell.TH.Syntax   (Lift)
+import Misc
+import Misc.Lift1
 import Control.Lens
 ----------------------------------------------------------------------------------

-data Expr b = Var Name
-            | Con Tag Int -- ^ Con Tag Arity
-            | Case (Expr b) [Alter b]
-            | Lam [b] (Expr b)
-            | Let Rec [Binding b] (Expr b)
-            | App (Expr b) (Expr b)
-            | Lit Lit
-            deriving (Show, Read, Lift)
+data ExprF b a = VarF Name
+               | ConF Tag Int -- ^ Con Tag Arity
+               | CaseF a [AlterF b a]
+               | LamF [b] a
+               | LetF Rec [BindingF b a] a
+               | AppF a a
+               | LitF Lit
+               | TypeF Type
+               deriving (Functor, Foldable, Traversable)

-deriving instance (Eq b) => Eq (Expr b)
+type Expr b = Fix (ExprF b)
+
+instance IsString (ExprF b a) where
+    fromString = VarF . fromString
+
+instance (IsString (f (Fix f))) => IsString (Fix f) where
+    fromString = Fix . fromString

 data Type = TyFun
          | TyVar Name
          | TyApp Type Type
          | TyCon Name
-          deriving (Show, Read, Lift, Eq)
+          | TyForall Var Type
+          | TyKindType
+          deriving (Show, Eq, Lift)
+
+type Kind = Type
+
+-- data TyCon = MkTyCon Name Kind
+--     deriving (Eq, Show, Lift)
+
+data Var = MkVar Name Type
+    deriving (Eq, Show, Lift)
+
+pattern (:^) :: Name -> Type -> Var
+pattern n :^ t = MkVar n t
+
+instance Hashable Var where
+    hashWithSalt s (MkVar n _) = hashWithSalt s n
+
+pattern Con :: Tag -> Int -> Expr b
+pattern Con t a = Fix (ConF t a)
+
+pattern Var :: Name -> Expr b
+pattern Var b = Fix (VarF b)
+
+pattern App :: Expr b -> Expr b -> Expr b
+pattern App f x = Fix (AppF f x)
+
+pattern Lam :: [b] -> Expr b -> Expr b
+pattern Lam bs e = Fix (LamF bs e)
+
+pattern Let :: Rec -> [Binding b] -> Expr b -> Expr b
+pattern Let r bs e = Fix (LetF r bs e)
+
+pattern Case :: Expr b -> [Alter b] -> Expr b
+pattern Case e as = Fix (CaseF e as)
+
+pattern Type :: Type -> Expr b
+pattern Type t = Fix (TypeF t)
+
+pattern Lit :: Lit -> Expr b
+pattern Lit t = Fix (LitF t)

 pattern TyInt :: Type
 pattern TyInt = TyCon "Int#"

-infixl 2 :$
-pattern (:$) :: Expr b -> Expr b -> Expr b 
-pattern f :$ x = App f x
-
-infixl 2 :@
-pattern (:@) :: Type -> Type -> Type
-pattern f :@ x = TyApp f x
-
 infixr 1 :->
 pattern (:->) :: Type -> Type -> Type
 pattern a :-> b = TyApp (TyApp TyFun a) b

-{-# COMPLETE Binding :: Binding #-}
-{-# COMPLETE (:=) :: Binding #-}
-data Binding b = Binding b (Expr b)
-    deriving (Show, Read, Lift)
+data BindingF b a = BindingF b (ExprF b a)
+    deriving (Functor, Foldable, Traversable)

-deriving instance (Eq b) => Eq (Binding b)
+type Binding b = BindingF b (Fix (ExprF b))
+
+type Binding' = Binding Name
+
+-- collapse = foldFix embed
+
+pattern Binding :: b -> Expr b -> Binding b
+pattern Binding k v <- BindingF k (wrapFix -> v)
+    where Binding k v = BindingF k (unwrapFix v)
+
+{-# COMPLETE (:=) #-}
+{-# COMPLETE Binding #-}

 infixl 1 :=
 pattern (:=) :: b -> Expr b -> Binding b
 pattern k := v = Binding k v

-data Alter b = Alter AltCon [b] (Expr b)
-    deriving (Show, Read, Lift)
+infixl 2 :$
+pattern (:$) :: Expr b -> Expr b -> Expr b
+pattern f :$ x = App f x

-deriving instance (Eq b) => Eq (Alter b)
+data AlterF b a = AlterF AltCon [b] (ExprF b a)
+    deriving (Functor, Foldable, Traversable)
+
+pattern Alter :: AltCon -> [b] -> Expr b -> Alter b
+pattern Alter con bs e <- AlterF con bs (wrapFix -> e)
+    where Alter con bs e = AlterF con bs (unwrapFix e)
+
+type Alter b = AlterF b (Fix (ExprF b))
+
+type Alter' = Alter Name
+
+-- pattern Alter :: AltCon -> [b] -> Expr b -> Alter b
+-- pattern Alter con bs e <- Fix (AlterF con bs (undefined -> e))
+--     where Alter con bs e = Fix (AlterF con bs undefined)

 newtype Pragma = Pragma [T.Text]

 data Rec = Rec
         | NonRec
-         deriving (Show, Read, Eq, Lift)
+         deriving (Show, Eq, Lift)

 data AltCon = AltData Name
            | AltTag Tag
            | AltLit Lit
            | AltDefault
-            deriving (Show, Read, Eq, Lift)
+            deriving (Show, Eq, Lift)

 newtype Lit = IntL Int
-    deriving (Show, Read, Eq, Lift)
+    deriving (Show, Eq, Lift)

 type Name = T.Text
 type Tag = Int

 data ScDef b = ScDef b [b] (Expr b)
-    deriving (Show, Lift)

-unliftScDef :: ScDef b -> Expr b
-unliftScDef (ScDef _ as e) = Lam as e
+-- unliftScDef :: ScDef b -> Expr b
+-- unliftScDef (ScDef _ as e) = Lam as e

 data Module b = Module (Maybe (Name, [Name])) (Program b)
-    deriving (Show, Lift)

 data Program b = Program
    { _programScDefs   :: [ScDef b]
    , _programTypeSigs :: HashMap b Type
-    , _programDataTags :: HashMap b (Tag, Int)
+    , _programDataTags :: HashMap Name (Tag, Int)
    -- ^ map constructors to their tag and arity
    }
-    deriving (Show, Lift, Generic)
+    deriving (Generic)
    deriving (Semigroup, Monoid)
        via Generically (Program b)

 makeLenses ''Program
-makeBaseFunctor ''Expr
+-- makeBaseFunctor ''Expr
 pure []

 -- this is a weird optic, stronger than Lens and Prism, but weaker than Iso.
@@ -163,65 +236,89 @@ type ExprF' = ExprF Name
 type Program' = Program Name
 type Expr' = Expr Name
 type ScDef' = ScDef Name
-type Alter' = Alter Name
-type Binding' = Binding Name
+-- type Alter' = Alter Name
+-- type Binding' = Binding Name

-instance IsString (Expr b) where
-    fromString = Var . fromString
-
-instance IsString Type where
-    fromString "" = error "IsString Type string may not be empty"
-    fromString s
-        | isUpper c     = TyCon . fromString $ s
-        | otherwise     = TyVar . fromString $ s
-        where (c:_) = s
+-- instance IsString (Expr b) where
+--     fromString = Var . fromString

 ----------------------------------------------------------------------------------

 class HasRHS s t a b | s -> a, t -> b, s b -> t, t a -> s where
    _rhs :: Lens s t a b

-instance HasRHS (Alter b) (Alter b) (Expr b) (Expr b) where
+instance HasRHS (AlterF b a) (AlterF b a') (ExprF b a) (ExprF b a') where
    _rhs = lens
-        (\ (Alter _ _ e) -> e)
-        (\ (Alter t as _) e' -> Alter t as e')
+        (\ (AlterF _ _ e) -> e)
+        (\ (AlterF t as _) e' -> AlterF t as e')

 instance HasRHS (ScDef b) (ScDef b) (Expr b) (Expr b) where
    _rhs = lens
        (\ (ScDef _ _ e) -> e)
        (\ (ScDef n as _) e' -> ScDef n as e')

-instance HasRHS (Binding b) (Binding b) (Expr b) (Expr b) where
-    _rhs = lens
-        (\ (_ := e) -> e)
-        (\ (k := _) e' -> k := e')
+instance HasRHS (BindingF b a) (BindingF b' a') (ExprF b a) (ExprF b' a')

 class HasLHS s t a b | s -> a, t -> b, s b -> t, t a -> s where
    _lhs :: Lens s t a b

-instance HasLHS (Alter b) (Alter b) (AltCon, [b]) (AltCon, [b]) where
-    _lhs = lens
-        (\ (Alter a bs _) -> (a,bs))
-        (\ (Alter _ _ e) (a',bs') -> Alter a' bs' e)
-
 instance HasLHS (ScDef b) (ScDef b) (b, [b]) (b, [b]) where
    _lhs = lens
        (\ (ScDef n as _) -> (n,as))
        (\ (ScDef _ _ e) (n',as') -> ScDef n' as' e)

-instance HasLHS (Binding b) (Binding b) b b where
-    _lhs = lens
-        (\ (k := _) -> k)
-        (\ (_ := e) k' -> k' := e)
+-- instance HasLHS (Binding b) (Binding b) b b where
+    -- _lhs = lens
+    --     (\ (k := _) -> k)
+    --     (\ (_ := e) k' -> k' := e)
+
+-- | This is not a valid isomorphism for expressions containing lambdas whose
+-- bodies are themselves lambdas with multiple arguments:
+--
+-- >>> [coreExpr|\x -> \y z -> x|] ^. from (from formalising)
+-- Lam ["x"] (Lam ["y"] (Lam ["z"] (Var "x")))
+-- >>> [coreExpr|\x -> \y z -> x|]
+-- Lam ["x"] (Lam ["y","z"] (Var "x"))
+--
+-- For this reason, it's best to consider 'formalising' as if it were two
+-- unrelated unidirectional getters.
+
+formalising :: Iso (Expr a) (Expr b) (Expr a) (Expr b)
+formalising = iso sa bt where
+    sa :: Expr a -> Expr a
+    sa = ana \case
+        Lam [b] e      -> LamF [b] e
+        Lam (b:bs) e   -> LamF [b] (Lam bs e)
+        Let r (b:bs) e -> LetF r [b] (Let r bs e)
+        x              -> project x
+
+    bt :: Expr b -> Expr b
+    bt = cata \case
+        LamF [b] (Lam bs e)                -> Lam (b:bs) e
+        LetF r [b] (Let r' bs e) | r == r' -> Let r (b:bs) e
+        x                                  -> embed x

 --------------------------------------------------------------------------------

-- TODO: print type sigs with corresponding scdefs
-- TODO: emit pragmas for datatags
-instance (Hashable b, Pretty b) => Pretty (Program b) where
-    pretty p = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p
-           $+$ vlinesOf (programJoinedDefs . to prettyGroup) p
+newtype WithTerseBinds a = WithTerseBinds a
+
+class MakeTerse a where
+    type AsTerse a :: Data.Kind.Type
+    asTerse :: a -> AsTerse a
+
+instance MakeTerse Var where
+    type AsTerse Var = Name
+    asTerse (MkVar n _) = n
+
+instance (Hashable b, Pretty b, Pretty (AsTerse b), MakeTerse b)
+      => Pretty (WithTerseBinds (Program b)) where
+    pretty (WithTerseBinds p)
+            = (datatags <> "\n")
+          $+$ defs
        where
+            datatags = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p
+            defs = vlinesOf (programJoinedDefs . to prettyGroup) p
+
            programJoinedDefs :: Fold (Program b) (These (b, Type) (ScDef b))
            programJoinedDefs = folding $ \p ->
                foldMapOf programTypeSigs thisTs p
@@ -234,67 +331,365 @@ instance (Hashable b, Pretty b) => Pretty (Program b) where
                H.singleton (sc ^. _lhs . _1) (That sc)

            prettyGroup :: These (b, Type) (ScDef b) -> Doc
-            prettyGroup = bifoldr ($$) ($$) mempty . bimap prettyTySig pretty
-
-            prettyTySig (n,t) = hsep [ttext n, "::", pretty t]
-
-            unionThese (This a) (That b) = These a b
-            unionThese (That b) (This a) = These a b
-            unionThese (These a b) _     = These a b
+            prettyGroup = bifoldr vs vs mempty
+                        . bimap (uncurry prettyTySig')
+                                (pretty . WithTerseBinds)
+                where vs = vsepTerm ";"

            cataDataTag n (t,a) acc = prettyDataTag n t a $+$ acc

-            prettyDataTag n t a =
-                hsep ["{-#", "PackData", ttext n, ttext t, ttext a, "#-}"]
+instance (Hashable b, Pretty b) => Pretty (Program b) where
+    pretty p = (datatags <> "\n")
+           $+$ defs
+        where
+            datatags = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p
+            defs = vlinesOf (programJoinedDefs . to prettyGroup) p
+
+            programJoinedDefs :: Fold (Program b) (These (b, Type) (ScDef b))
+            programJoinedDefs = folding $ \p ->
+                foldMapOf programTypeSigs thisTs p
+                `u` foldMapOf programScDefs thatSc p
+              where u = H.unionWith unionThese
+
+            thisTs = ifoldMap @b @(HashMap b)
+                (\n t -> H.singleton n (This (n,t)))
+            thatSc = foldMap $ \sc ->
+                H.singleton (sc ^. _lhs . _1) (That sc)
+
+            prettyGroup :: These (b, Type) (ScDef b) -> Doc
+            prettyGroup = bifoldr vs vs mempty
+                        . bimap (uncurry prettyTySig) pretty
+                where vs = vsepTerm ";"
+
+            cataDataTag n (t,a) acc = prettyDataTag n t a $+$ acc
+
+unionThese :: These a b -> These a b -> These a b
+unionThese (This a) (That b) = These a b
+unionThese (That b) (This a) = These a b
+unionThese (These a b) _     = These a b
+
+prettyDataTag :: (Pretty n, Pretty t, Pretty a)
+              => n -> t -> a -> Doc
+prettyDataTag n t a =
+    hsep ["{-#", "PackData", ttext n, ttext t, ttext a, "#-}"]
+
+prettyTySig :: (Pretty n, Pretty t) => n -> t -> Doc
+prettyTySig n t = hsep [ttext n, ":", pretty t]
+
+prettyTySig' :: (MakeTerse n, Pretty (AsTerse n), Pretty t) => n -> t -> Doc
+prettyTySig' n t = hsep [ttext (asTerse n), ":", pretty t]
+
+-- Pretty Type
+-- TyApp | appPrec   | left
+-- (:->) | appPrec-1 | right

 instance Pretty Type where
-    prettyPrec _ (TyVar n) = ttext n
-    prettyPrec _ TyFun = "(->)"
-    prettyPrec _ (TyCon n) = ttext n
-    prettyPrec p (a :-> b) = maybeParens (p>0) $
-        hsep [prettyPrec 1 a, "->", prettyPrec 0 b]
-    prettyPrec p (TyApp f x) = maybeParens (p>1) $
-        prettyPrec 1 f <+> prettyPrec 2 x
+    prettyPrec _ (TyVar n)   = ttext n
+    prettyPrec _ TyFun       = "(->)"
+    prettyPrec _ (TyCon n)   = ttext n
+    prettyPrec p (a :-> b)   = maybeParens (p>appPrec-1) $
+        hsep [prettyPrec appPrec a, "->", prettyPrec (appPrec-1) b]
+    prettyPrec p (TyApp f x) = maybeParens (p>appPrec) $
+        prettyPrec appPrec f <+> prettyPrec appPrec1 x
+    prettyPrec p (TyForall a m) = maybeParens (p>appPrec-2) $
+        "∀" <+> (prettyPrec appPrec1 a <> ".") <+> pretty m
+    prettyPrec _ TyKindType = "Type"
+
+instance (Pretty b, Pretty (AsTerse b), MakeTerse b)
+      => Pretty (WithTerseBinds (ScDef b)) where
+    pretty (WithTerseBinds sc) = hsep [name, as, "=", hang empty 1 e]
+        where
+            name = ttext $ sc ^. _lhs . _1 . to asTerse
+            as = sc & hsepOf (_lhs . _2 . each . to asTerse . to ttext)
+            e = pretty $ sc ^. _rhs

 instance (Pretty b) => Pretty (ScDef b) where
-    pretty sc = hsep [name, as, "=", hang empty 1 e, ";"]
+    pretty sc = hsep [name, as, "=", hang empty 1 e]
        where
            name = ttext $ sc ^. _lhs . _1
            as = sc & hsepOf (_lhs . _2 . each . to ttext)
            e = pretty $ sc ^. _rhs

-instance (Pretty b) => Pretty (Expr b) where
-    prettyPrec _ (Var n)      = ttext n
-    prettyPrec _ (Con t a)    = "Pack{" <> (ttext t <+> ttext a) <> "}"
-    prettyPrec _ (Lam bs e)   = hsep ["λ", hsep (prettyPrec 1 <$> bs), "->", pretty e]
-    prettyPrec _ (Let r bs e) = hsep [word, explicitLayout bs]
-                            $+$ hsep ["in", pretty e]
-        where word = if r == Rec then "letrec" else "let"
-    prettyPrec p (App f x)    = maybeParens (p>0) $
-        prettyPrec 0 f <+> prettyPrec 1 x
-    prettyPrec _ (Lit l)      = pretty l
-    prettyPrec p (Case e as)  = maybeParens (p>0) $
+instance (Pretty (f (Fix f))) => Pretty (Fix f) where
+    prettyPrec d (Fix f) = prettyPrec d f
+
+-- Pretty Expr
+-- LamF | appPrec1 | right
+-- AppF | appPrec  | left
+
+instance (Pretty b, Pretty a) => Pretty (ExprF b a) where
+    prettyPrec _ (VarF n) = ttext n
+    prettyPrec _ (ConF t a) = "Pack{" <> (ttext t <+> ttext a) <> "}"
+    prettyPrec p (LamF bs e) = maybeParens (p>0) $
+        hsep ["λ", hsep (prettyPrec appPrec1 <$> bs), "->", pretty e]
+    prettyPrec p (LetF r bs e) = maybeParens (p>0)
+                               $ hsep [pretty r, explicitLayout bs]
+                             $+$ hsep ["in", pretty e]
+    prettyPrec p (AppF f x) = maybeParens (p>appPrec) $
+        prettyPrec appPrec f <+> prettyPrec appPrec1 x
+    prettyPrec p (LitF l) = prettyPrec p l
+    prettyPrec p (CaseF e as) = maybeParens (p>0) $
        "case" <+> pretty e <+> "of"
        $+$ nest 2 (explicitLayout as)
+    prettyPrec p (TypeF t) = "@" <> prettyPrec appPrec1 t

-instance (Pretty b) => Pretty (Alter b) where
-    pretty (Alter c as e) =
+instance Pretty Rec where
+    pretty Rec = "letrec"
+    pretty NonRec = "let"
+
+instance (Pretty b, Pretty a) => Pretty (AlterF b a) where
+    pretty (AlterF c as e) =
        hsep [pretty c, hsep (pretty <$> as), "->", pretty e]

 instance Pretty AltCon where
    pretty (AltData n) = ttext n
    pretty (AltLit l) = pretty l
-    pretty (AltTag t) = ttext t
+    pretty (AltTag t) = "<" <> ttext t <> ">"
    pretty AltDefault = "_"

 instance Pretty Lit where
    pretty (IntL n) = ttext n

-instance (Pretty b) => Pretty (Binding b) where
-    pretty (k := v) = hsep [pretty k, "=", pretty v]
+instance (Pretty b, Pretty a) => Pretty (BindingF b a) where
+    pretty (BindingF k v) = hsep [pretty k, "=", pretty v]

 explicitLayout :: (Pretty a) => [a] -> Doc
 explicitLayout as = vcat inner <+> "}" where
    inner = zipWith (<+>) delims (pretty <$> as)
    delims = "{" : repeat ";"

+instance Pretty Var where
+    prettyPrec p (MkVar n t) = maybeParens (p>0) $
+        hsep [pretty n, ":", pretty t]
+
+--------------------------------------------------------------------------------
+
+-- instance Functor Alter where
+--     fmap f (Alter con bs e) = Alter con (f <$> bs) e'
+--         where
+--             e' = foldFix (embed . bimap' f id) e
+--             bimap' = $(makeBimap ''ExprF)
+
+-- instance Foldable Alter where
+-- instance Traversable Alter where
+-- instance Functor Binding where
+-- instance Foldable Binding where
+-- instance Traversable Binding where
+
+liftShowsPrecExpr :: (Show b)
+                  => (Int -> a -> ShowS)
+                  -> ([a] -> ShowS)
+                  -> Int -> ExprF b a -> ShowS
+liftShowsPrecExpr = $(makeLiftShowsPrec ''ExprF)
+
+showsPrec1Expr :: (Show b, Show a)
+               => Int -> ExprF b a -> ShowS
+showsPrec1Expr = $(makeShowsPrec1 ''ExprF)
+
+instance (Show b) => Show1 (AlterF b) where
+    liftShowsPrec sp spl d (AlterF con bs e) =
+        showsTernaryWith showsPrec showsPrec (liftShowsPrecExpr sp spl)
+                         "AlterF" d con bs e
+
+instance (Show b) => Show1 (BindingF b) where
+    liftShowsPrec sp spl d (BindingF k v) =
+        showsBinaryWith showsPrec (liftShowsPrecExpr sp spl)
+                        "BindingF" d k v
+
+instance (Show b, Show a) => Show (BindingF b a) where
+    showsPrec d (BindingF k v)
+        = showParen (d > 10)
+        $ showString "BindingF" . showChar ' '
+        . showsPrec 11 k . showChar ' '
+        . showsPrec1Expr 11 v
+
+instance (Show b, Show a) => Show (AlterF b a) where
+    showsPrec d (AlterF con bs e)
+        = showParen (d > 10)
+        $ showString "AlterF" . showChar ' '
+        . showsPrec 11 con . showChar ' '
+        . showsPrec 11 bs . showChar ' '
+        . showsPrec1Expr 11 e
+
+deriveShow1 ''ExprF
+
+deriving instance (Show b, Show a) => Show (ExprF b a)
+-- deriving instance (Show b, Show a) => Show (BindingF b a)
+-- deriving instance (Show b, Show a) => Show (AlterF b a)
+deriving instance Show b => Show (ScDef b)
+deriving instance Show b => Show (Program b)
+
+bimapExpr :: (b -> b') -> (a -> a')
+          -> ExprF b a -> ExprF b' a'
+bimapExpr = $(makeBimap ''ExprF)
+
+bifoldrExpr :: (b -> c -> c)
+            -> (a -> c -> c)
+            -> c -> ExprF b a -> c
+bifoldrExpr = $(makeBifoldr ''ExprF)
+
+bitraverseExpr :: Applicative f
+               => (b -> f b')
+               -> (a -> f a')
+               -> ExprF b a -> f (ExprF b' a')
+bitraverseExpr = $(makeBitraverse ''ExprF)
+
+instance Bifunctor AlterF where
+    bimap f g (AlterF con bs e) = AlterF con (f <$> bs) (bimapExpr f g e)
+
+instance Bifunctor BindingF where
+    bimap f g (BindingF k v) = BindingF (f k) (bimapExpr f g v)
+
+instance Bifoldable AlterF where
+    bifoldr f g z (AlterF con bs e) = bifoldrExpr f g z' e where
+        z' = foldr f z bs
+
+instance Bitraversable AlterF where
+    bitraverse f g (AlterF con bs e) =
+        AlterF con <$> traverse f bs <*> bitraverseExpr f g e
+
+instance Bifoldable BindingF where
+    bifoldr f g z (BindingF k v) = bifoldrExpr f g (f k z) v
+
+instance Bitraversable BindingF where
+    bitraverse f g (BindingF k v) =
+        BindingF <$> f k <*> bitraverseExpr f g v
+
+deriveBifunctor ''ExprF
+deriveBifoldable ''ExprF
+deriveBitraversable ''ExprF
+
+instance Lift b => Lift1 (ExprF b) where
+    lift1 (VarF k)      = liftCon 'VarF (lift k)
+    lift1 (AppF f x)    = liftCon2 'AppF (lift f) (lift x)
+    lift1 (LamF b e)    = liftCon2 'LamF (lift b) (lift e)
+    lift1 (LetF r bs e) = liftCon3 'LetF (lift r) (lift bs) (lift e)
+    lift1 (CaseF e as)  = liftCon2 'CaseF (lift e) (lift as)
+    lift1 (TypeF t)     = liftCon 'TypeF (lift t)
+    lift1 (LitF l)      = liftCon 'LitF (lift l)
+    lift1 (ConF t a)    = liftCon2 'ConF (lift t) (lift a)
+
+deriving instance (Lift b, Lift a) => Lift (ExprF b a)
+deriving instance (Lift b, Lift a) => Lift (BindingF b a)
+deriving instance (Lift b, Lift a) => Lift (AlterF b a)
+deriving instance Lift b => Lift (ScDef b)
+deriving instance Lift b => Lift (Program b)
+
+--------------------------------------------------------------------------------
+
+class HasApplicants1 s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    applicants1 :: Traversal s t a b
+
+class HasApplicants s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    applicants :: Traversal s t a b
+
+instance HasApplicants1 Type Type Type Type where
+    applicants1 k (TyApp f x) = TyApp <$> applicants1 k f <*> k x
+    applicants1 k x           = k x
+
+instance HasApplicants Type Type Type Type where
+    applicants k (TyApp f x) = TyApp <$> applicants k f <*> k x
+    applicants k x           = pure x
+
+-- instance HasArguments (ExprF b (Fix (ExprF b))) (ExprF b (Fix (ExprF b)))
+--                        (Fix (ExprF b)) (Fix (ExprF b)) where
+--     arguments k (AppF f x) = AppF <$> arguments k f <*> k x
+--     arguments k x          = unwrapFix <$> k (wrapFix x)
+
+-- instance HasArguments (f (Fix f)) (f (Fix f)) (Fix f) (Fix f)
+--       => HasArguments (Fix f) (Fix f) (Fix f) (Fix f) where
+--     arguments :: forall g. Applicative g
+--                => LensLike' g (Fix f) (Fix f)
+--     arguments k (Fix f) = Fix <$> arguments k f
+
+-- arguments :: Traversal' (Expr b) (Expr b)
+-- arguments k (App f x) = App <$> arguments k f <*> k x
+-- arguments k x         = k x
+
+class HasBinders s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    binders :: Traversal s t a b
+
+instance HasBinders (ScDef b) (ScDef b') b b' where
+    binders k (ScDef b as e) = ScDef <$> k b <*> traverse k as <*> binders k e
+
+instance (Hashable b, Hashable b')
+      => HasBinders (Program b) (Program b') b b' where
+    binders :: forall f. (Applicative f)
+            => LensLike f (Program b) (Program b') b b'
+    binders k p
+        = Program
+        <$> traverse (binders k) (_programScDefs p)
+        <*> (getAp . ifoldMap toSingleton $ _programTypeSigs p)
+        <*> pure (_programDataTags p)
+      where
+        toSingleton :: b -> Type -> Ap f (HashMap b' Type)
+        toSingleton b t = Ap $ (`H.singleton` t) <$> k b
+
+instance HasBinders a a' b b'
+    => HasBinders (ExprF b a) (ExprF b' a') b b' where
+    binders :: forall f. (Applicative f)
+                    => LensLike f (ExprF b a) (ExprF b' a') b b'
+    binders k = go where
+        go :: ExprF b a -> f (ExprF b' a')
+        go (LamF bs e)   = LamF <$> traverse k bs <*> binders k e
+        go (CaseF e as)  = CaseF <$> binders k e <*> eachbind as
+        go (LetF r bs e) = LetF r <$> eachbind bs <*> binders k e
+        go f             = bitraverse k (binders k) f
+
+        eachbind :: forall p. Bitraversable p => [p b a] -> f [p b' a']
+        eachbind bs = bitraverse k (binders k) `traverse` bs
+
+instance HasBinders a a b b'
+      => HasBinders (AlterF b a) (AlterF b' a) b b' where
+    binders k (AlterF con bs e) =
+        AlterF con <$> traverse k bs <*> traverseOf binders k e
+
+instance HasBinders a a b b'
+      => HasBinders (BindingF b a) (BindingF b' a) b b' where
+    binders k (BindingF b v) = BindingF <$> k b <*> binders k v
+
+instance (HasBinders (f b (Fix (f b))) (f b' (Fix (f b'))) b b')
+      => HasBinders (Fix (f b)) (Fix (f b')) b b' where
+    binders k (Fix f) = Fix <$> binders k f
+
+class HasArrowStops s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    arrowStops :: Traversal s t a b
+
+instance HasArrowStops Type Type Type Type where
+    arrowStops k (s :-> t) = (:->) <$> k s <*> arrowStops k t
+    arrowStops k t = k t
+
+--------------------------------------------------------------------------------
+
+liftEqExpr :: (Eq b)
+           => (a -> a' -> Bool)
+           -> ExprF b a -> ExprF b a' -> Bool
+liftEqExpr = $(makeLiftEq ''ExprF)
+
+instance (Eq b, Eq a) => Eq (BindingF b a) where
+    BindingF ka va == BindingF kb vb =
+        ka == kb && va `eq` vb
+      where eq = liftEqExpr (==)
+
+instance (Eq b, Eq a) => Eq (AlterF b a) where
+    AlterF cona bsa ea == AlterF conb bsb eb =
+        cona == conb && bsa == bsb && ea `eq` eb
+      where eq = liftEqExpr (==)
+
+instance (Eq b) => Eq1 (AlterF b) where
+    liftEq f (AlterF cona bsa ea) (AlterF conb bsb eb) =
+        cona == conb && bsa == bsb && ea `eq` eb
+      where eq = liftEqExpr f
+
+instance (Eq b) => Eq1 (BindingF b) where
+    liftEq f (BindingF ka va) (BindingF kb vb) =
+        ka == kb && va `eq` vb
+      where eq = liftEqExpr f
+
+deriveEq1 ''ExprF
+
+deriving instance (Eq b, Eq a) => Eq (ExprF b a)
+
+makePrisms ''BindingF
+makePrisms ''Var
+
--- a/src/Core/SystemF.hs
+++ b/src/Core/SystemF.hs
@@ -0,0 +1,235 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE OverloadedLists #-}
+module Core.SystemF
+    ( lintCoreProgR
+    )
+    where
+--------------------------------------------------------------------------------
+import GHC.Generics                 (Generic, Generically(..))
+import Data.HashMap.Strict          (HashMap)
+import Data.HashMap.Strict          qualified as H
+import Data.Function                (on)
+import Data.Traversable
+import Data.Foldable
+import Data.List.Extra
+import Control.Monad.Utils
+import Control.Monad
+import Data.Text                    qualified as T
+import Data.Pretty
+import Text.Printf
+
+import Control.Comonad
+import Control.Comonad.Cofree
+import Data.Fix
+import Data.Functor
+
+import Control.Lens                 hiding ((:<))
+import Control.Lens.Unsound
+
+import Compiler.RLPC
+import Compiler.RlpcError
+import Core
+--------------------------------------------------------------------------------
+
+data Gamma = Gamma
+    { _gammaVars   :: HashMap Name Type
+    , _gammaTyVars :: HashMap Name Kind
+    , _gammaTyCons :: HashMap Name Kind
+    }
+    deriving (Generic)
+    deriving (Semigroup, Monoid)
+        via (Generically Gamma)
+
+makeLenses ''Gamma
+
+lintCoreProgR :: (Monad m) => Program Var -> RLPCT m (Program Name)
+lintCoreProgR = undefined
+
+lint :: Program Var -> Program Name
+lint = undefined
+
+type ET = Cofree (ExprF Var) Type
+
+type SysF = Either SystemFError
+
+data SystemFError = SystemFErrorUndefinedVariable Name
+                  | SystemFErrorKindMismatch Kind Kind
+                  | SystemFErrorCouldNotMatch Type Type
+                  deriving Show
+
+instance IsRlpcError SystemFError where
+    liftRlpcError = \case
+        SystemFErrorUndefinedVariable n ->
+            undefinedVariableErr n
+        SystemFErrorKindMismatch k k' ->
+            Text [ T.pack $ printf "Could not match kind `%s' with `%s'"
+                                   (pretty k) (pretty k')
+                 ]
+        SystemFErrorCouldNotMatch t t' ->
+            Text [ T.pack $ printf "Could not match type `%s' with `%s'"
+                                   (pretty t) (pretty t')
+                 ]
+
+justLintCoreExpr = fmap (fmap (prettyPrec appPrec1)) . lintE demoContext
+
+lintE :: Gamma -> Expr Var -> SysF ET
+lintE g = \case
+    Var n -> lookupVar g n <&> (:< VarF n)
+    Lit (IntL n) -> pure $ TyInt :< LitF (IntL n)
+
+    Type t -> kindOf g t <&> (:< TypeF t)
+
+    App f x
+        -- type application
+        | Right (TyForall (a :^ k) m :< f') <- lintE g f
+        , Right (k' :< TypeF t) <- lintE g x
+        , k == k'
+        -> pure $ subst a t m :< f'
+
+        -- value application
+        | Right fw@((s :-> t) :< _) <- lintE g f
+        , Right xw@(s' :< _) <- lintE g x
+        , s == s'
+        -> pure $ t :< AppF fw xw
+
+    Lam bs e -> do
+        e'@(t :< _) <- lintE g' e
+        pure $ foldr arrowify t bs :< LamF bs e'
+      where
+        g' = foldMap suppl bs <> g
+
+        suppl (MkVar n t)
+            | isKind t  = mempty & gammaTyVars %~ H.insert n t
+            | otherwise = mempty & gammaVars %~ H.insert n t
+
+        arrowify (MkVar n s) s'
+            | isKind s  = TyForall (n :^ s) s'
+            | otherwise = s :-> s'
+
+    Let Rec bs e -> do
+        e'@(t :< _) <- lintE g' e
+        bs' <- (uncurry checkBind . (_2 %~ wrapFix)) `traverse` binds
+        pure $ t :< LetF Rec bs' e'
+      where
+        binds = bs ^.. each . _BindingF
+        vs = binds ^.. each . _1 . _MkVar
+        g' = supplementVars vs g
+        checkBind v@(MkVar n t) e = case lintE g' e of
+            Right (t' :< e') | t == t'   -> Right (BindingF v e')
+                             | otherwise -> Left (SystemFErrorCouldNotMatch t t')
+            Left e -> Left e
+    Let NonRec bs e -> do
+        (g',bs') <- mapAccumLM checkBind g bs
+        e'@(t :< _) <- lintE g' e
+        pure $ t :< LetF NonRec bs' e'
+      where
+        checkBind :: Gamma -> BindingF Var (Expr Var)
+                  -> SysF (Gamma, BindingF Var ET)
+        checkBind g (BindingF v@(n :^ t) e) = case lintE g (wrapFix e) of
+            Right (t' :< e')
+                | t == t'   -> Right (supplementVar n t g, BindingF v e')
+                | otherwise -> Left (SystemFErrorCouldNotMatch t t')
+            Left e -> Left e
+
+    Case e as -> do
+        e'@(et :< _) <- lintE g e
+        (ts,as') <- unzip <$> checkAlt et `traverse` as
+        case allUnify ts of
+            Just err -> Left err
+            Nothing  -> pure $ head ts  :< CaseF e' as'
+      where
+        checkAlt :: Type -> Alter Var -> SysF (Type, AlterF Var ET)
+        checkAlt scrutineeType (AlterF (AltData con) bs e) = do
+            ct <- lookupVar g con
+            ct' <- foldrMOf applicants (elimForall g) ct scrutineeType
+            zipWithM_ fzip bs (ct' ^.. arrowStops)
+            (t :< e') <- lintE (supplementVars (varsToPairs bs) g) (wrapFix e)
+            pure (t, AlterF (AltData con) bs e')
+          where
+            fzip (MkVar _ t) t'
+                | t == t'   = Right ()
+                | otherwise = Left (SystemFErrorCouldNotMatch t t')
+
+allUnify :: [Type] -> Maybe SystemFError
+allUnify [] = Nothing
+allUnify [t] = Nothing
+allUnify (t:t':ts)
+    | t == t'   = allUnify ts
+    | otherwise = Just (SystemFErrorCouldNotMatch t t')
+
+elimForall :: Gamma -> Type -> Type -> SysF Type
+elimForall g t (TyForall (n :^ k) m) = do
+    k' <- kindOf g t
+    case k == k' of
+        True -> pure $ subst n t m
+        False -> Left $ SystemFErrorKindMismatch k k'
+elimForall _ m _ = pure m
+ 
+varsToPairs :: [Var] -> [(Name, Type)]
+varsToPairs = toListOf (each . _MkVar)
+
+checkAgainst :: Gamma -> Var -> Expr Var -> SysF ET
+checkAgainst g v@(MkVar n t) e = case lintE g e of
+    Right e'@(t' :< _) | t == t'      -> Right e'
+                       | otherwise    -> Left (SystemFErrorCouldNotMatch t t')
+    Left a -> Left a
+
+supplementVars :: [(Name, Type)] -> Gamma -> Gamma
+supplementVars vs = gammaVars <>~ H.fromList vs
+
+supplementVar :: Name -> Type -> Gamma -> Gamma
+supplementVar n t = gammaVars %~ H.insert n t
+
+supplementTyVar :: Name -> Kind -> Gamma -> Gamma
+supplementTyVar n t = gammaTyVars %~ H.insert n t
+
+subst :: Name -> Type -> Type -> Type
+subst k v (TyVar n) | k == n = v
+subst k v (TyForall (MkVar n k') t)
+    | k /= n                 = TyForall (MkVar n k') (subst k v t)
+    | otherwise              = TyForall (MkVar n k') t
+subst k v (TyApp f x)        = (TyApp `on` subst k v) f x
+subst _ _ x                  = x
+
+isKind :: Type -> Bool
+isKind (s :-> t)  = isKind s && isKind t
+isKind TyKindType = True
+isKind _          = False
+
+kindOf :: Gamma -> Type -> SysF Kind
+kindOf g (TyVar n)  = lookupTyVar g n
+kindOf _ TyKindType = pure TyKindType
+kindOf g (TyCon n)  = lookupCon g n
+kindOf _ e          = error (show e)
+
+lookupCon :: Gamma -> Name -> SysF Kind
+lookupCon g n = case g ^. gammaTyCons . at n of
+    Just k  -> Right k
+    Nothing -> Left (SystemFErrorUndefinedVariable n)
+
+lookupVar :: Gamma -> Name -> SysF Type
+lookupVar g n = case g ^. gammaVars . at n of
+    Just t -> Right t
+    Nothing -> Left (SystemFErrorUndefinedVariable n)
+
+lookupTyVar :: Gamma -> Name -> SysF Kind
+lookupTyVar g n = case g ^. gammaTyVars . at n of
+    Just k -> Right k
+    Nothing -> Left (SystemFErrorUndefinedVariable n)
+
+demoContext :: Gamma
+demoContext = Gamma
+    { _gammaVars =
+        [ ("id", TyForall ("a" :^ TyKindType) $ TyVar "a" :-> TyVar "a")
+        , ("Just", TyForall ("a" :^ TyKindType) $
+            TyVar "a" :-> (TyCon "Maybe" `TyApp` TyVar "a"))
+        , ("Nothing", TyForall ("a" :^ TyKindType) $
+            TyCon "Maybe" `TyApp` TyVar "a")
+        ]
+    , _gammaTyVars = []
+    , _gammaTyCons =
+        [ ("Int#", TyKindType)
+        , ("Maybe", TyKindType :-> TyKindType)
+        ]
+    }
+
--- a/src/Core/TH.hs
+++ b/src/Core/TH.hs
@@ -5,8 +5,8 @@ Description : Core quasiquoters
 module Core.TH
    ( coreExpr
    , coreProg
-    , coreExprT
-    , coreProgT
+    -- , coreExprT
+    -- , coreProgT
    )
    where
 ----------------------------------------------------------------------------------
@@ -33,16 +33,18 @@ coreExpr :: QuasiQuoter
 coreExpr = mkqq $ lexCoreR >=> parseCoreExprR

 -- | Type-checked @coreProg@
-coreProgT :: QuasiQuoter
-coreProgT = mkqq $ lexCoreR >=> parseCoreProgR >=> checkCoreProgR
+-- coreProgT :: QuasiQuoter
+-- coreProgT = mkqq $ lexCoreR >=> parseCoreProgR >=> checkCoreProgR

-coreExprT :: QuasiQuoter
-coreExprT = mkqq $ lexCoreR >=> parseCoreExprR >=> checkCoreExprR g
-    where
-        g = [ ("+#", TyCon "Int#" :-> TyCon "Int#" :-> TyCon "Int#")
-            , ("id", TyCon "a" :-> TyCon "a")
-            , ("fix", (TyCon "a" :-> TyCon "a") :-> TyCon "a")
-            ]
+-- coreExprT :: QuasiQuoter
+-- coreExprT = mkqq $ lexCoreR >=> parseCoreExprR >=> checkCoreExprR g
+--     where
+--         g = [ ("+#", TyInt :-> TyInt :-> TyInt)
+--             , ("id", TyForall (MkVar "a" TyKindType) $
+--                     TyVar "a" :-> TyVar "a")
+--             , ("fix", TyForall (MkVar "a" TyKindType) $
+--                     (TyVar "a" :-> TyVar "a") :-> TyVar "a")
+--             ]

 mkqq :: (Lift a) => (Text -> RLPCIO a) -> QuasiQuoter
 mkqq p = QuasiQuoter
--- a/src/Core/Utils.hs
+++ b/src/Core/Utils.hs
@@ -2,8 +2,6 @@ module Core.Utils
    ( programRhss
    , programGlobals
    , isAtomic
-    -- , insertModule
-    , extractProgram
    , freeVariables
    )
    where
@@ -30,34 +28,29 @@ isAtomic _        = False

 ----------------------------------------------------------------------------------

-- TODO: export list awareness
-- insertModule :: Module b -> Program b -> Program b
-- insertModule (Module _ p) = programScDefs %~ (<>m)
+freeVariables :: Expr b -> Set b
+freeVariables = undefined

-extractProgram :: Module b -> Program b
-extractProgram (Module _ p) = p
+-- freeVariables :: Expr' -> Set Name
+-- freeVariables = cata go
+--     where
+--         go :: ExprF Name (Set Name) -> Set Name
+--         go (VarF k)         = S.singleton k
+--         -- TODO: collect free vars in rhss of bs
+--         go (LetF _ bs e)    = (e `S.union` esFree) `S.difference` ns
+--             where
+--                 es = bs ^.. each . _rhs :: [Expr']
+--                 ns = S.fromList $ bs ^.. each . _lhs
+--                 -- TODO: this feels a little wrong. maybe a different scheme is
+--                 -- appropriate
+--                 esFree = foldMap id $ freeVariables <$> es

----------------------------------------------------------------------------------
-
-freeVariables :: Expr' -> Set Name
-freeVariables = cata go
-    where
-        go :: ExprF Name (Set Name) -> Set Name
-        go (VarF k)         = S.singleton k
-        -- TODO: collect free vars in rhss of bs
-        go (LetF _ bs e)    = (e `S.union` esFree) `S.difference` ns
-            where
-                es = bs ^.. each . _rhs :: [Expr']
-                ns = S.fromList $ bs ^.. each . _lhs
-                -- TODO: this feels a little wrong. maybe a different scheme is
-                -- appropriate
-                esFree = foldMap id $ freeVariables <$> es
-
-        go (CaseF e as)     = e `S.union` asFree
-            where
-                asFree = foldMap id $ freeVariables <$> (fmap altToLam as)
-                -- we map alts to lambdas to avoid writing a 'freeVariablesAlt'
-                altToLam (Alter _ ns e) = Lam ns e
-        go (LamF bs e)      = e `S.difference` (S.fromList bs)
-        go e                = foldMap id e
+--         go (CaseF e as)     = e `S.union` asFree
+--             where
+--                 -- asFree = foldMap id $ freeVariables <$> (fmap altToLam as)
+--                 asFree = foldMap (freeVariables . altToLam) as
+--                 -- we map alts to lambdas to avoid writing a 'freeVariablesAlt'
+--                 altToLam (Alter _ ns e) = Lam ns e
+--         go (LamF bs e)      = e `S.difference` (S.fromList bs)
+--         go e                = foldMap id e

--- a/src/Core2Core.hs
+++ b/src/Core2Core.hs
@@ -116,7 +116,7 @@ floatNonStrictCases g = goE
            goE e
            traverse_ goE altBodies
            pure e'
-        goC (f :$ x)            = (:$) <$> goC f <*> goC x
+        goC (App f x)           = App <$> goC f <*> goC x
        goC (Let r bs e)        = Let r <$> bs' <*> goE e
            where bs' = travBs goC bs
        goC (Lit l)             = pure (Lit l)
@@ -128,10 +128,9 @@ floatNonStrictCases g = goE
        -- extract the right-hand sides of a list of bindings, traverse each
        -- one, and return the original list of bindings
        travBs :: (Expr' -> Floater Expr') -> [Binding'] -> Floater [Binding']
-        travBs c bs = bs ^.. each . _rhs
-                    & traverse goC
-                    & const (pure bs)
+        travBs c bs = undefined
        -- ^ ??? what the fuck?
+        -- ^ 24/02/22: what is this shit lol?

 -- when provided with a case expr, floatCase will float the case into a
 -- supercombinator of its free variables. the sc is returned along with an
--- a/src/Data/Pretty.hs
+++ b/src/Data/Pretty.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 module Data.Pretty
    ( Pretty(..)
    , rpretty
@@ -6,8 +7,11 @@ module Data.Pretty
    , hsepOf, vsepOf
    , vcatOf
    , vlinesOf
+    , vsepTerm
    , module Text.PrettyPrint
    , maybeParens
+    , appPrec
+    , appPrec1
    )
    where
 ----------------------------------------------------------------------------------
@@ -15,10 +19,13 @@ import Text.PrettyPrint             hiding ((<>))
 import Text.PrettyPrint.HughesPJ    hiding ((<>))
 import Text.Printf
 import Data.String                  (IsString(..))
-import Data.Text.Lens
+import Data.Text.Lens               hiding ((:<))
 import Data.Monoid
-import Data.Text                    qualified as T
 import Control.Lens
+
+-- instances
+import Control.Comonad.Cofree
+import Data.Text                    qualified as T
 ----------------------------------------------------------------------------------

 class Pretty a where
@@ -27,7 +34,7 @@ class Pretty a where

    {-# MINIMAL pretty | prettyPrec #-}
    pretty = prettyPrec 0
-    prettyPrec a _ = pretty a
+    prettyPrec = const pretty

 rpretty :: (IsString s, Pretty a) => a -> s
 rpretty = fromString . render . pretty
@@ -45,6 +52,9 @@ instance (Show a) => Pretty (Showing a) where

 deriving via Showing Int instance Pretty Int

+class (forall a. Pretty a => Pretty (f a)) => Pretty1 f where
+    liftPrettyPrec :: (Int -> a -> Doc) -> f a -> Doc
+
 --------------------------------------------------------------------------------

 ttext :: Pretty t => t -> Doc
@@ -63,3 +73,19 @@ vlinesOf :: Getting (Endo Doc) s Doc -> s -> Doc
 vlinesOf l = foldrOf l (\a b -> a $+$ "" $+$ b) mempty
 -- hack(?) to separate chunks with a blankline

+vsepTerm :: Doc -> Doc -> Doc -> Doc
+vsepTerm term a b = (a <> term) $+$ b
+
+--------------------------------------------------------------------------------
+
+appPrec, appPrec1 :: Int
+appPrec  = 10
+appPrec1 = 11
+
+instance PrintfArg Doc where
+    formatArg d fmt
+        | fmtChar (vFmt 'D' fmt) == 'D' = formatString (render d) fmt'
+        | otherwise                     = errorBadFormat $ fmtChar fmt
+      where
+        fmt' = fmt { fmtChar = 's', fmtPrecision = Nothing }
+
--- a/src/Misc.hs
+++ b/src/Misc.hs
@@ -0,0 +1,17 @@
+module Misc where
+--------------------------------------------------------------------------------
+import Data.Functor.Classes
+--------------------------------------------------------------------------------
+
+
+showsTernaryWith :: (Int -> a -> ShowS)
+                 -> (Int -> b -> ShowS)
+                 -> (Int -> c -> ShowS)
+                 -> String -> Int -> a -> b -> c -> ShowS
+showsTernaryWith sp1 sp2 sp3 name d x y z
+    = showParen (d > 10)
+    $ showString name . showChar ' '
+    . sp1 11 x . showChar ' '
+    . sp2 11 y . showChar ' '
+    . sp3 11 z
+
--- a/src/Misc/Lift1.hs
+++ b/src/Misc/Lift1.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Misc.Lift1
+    ( Lift1(..)
+    , liftCon, liftCon2, liftCon3
+    , Lift(..)
+    )
+    where
+--------------------------------------------------------------------------------
+import Language.Haskell.TH              hiding (Type, Name)
+import Language.Haskell.TH.Syntax       hiding (Type, Name)
+import Language.Haskell.TH.Syntax       qualified as TH
+import Language.Haskell.TH.Quote
+import Data.Kind                        qualified
+import GHC.Generics
+
+import Data.Fix
+--------------------------------------------------------------------------------
+
+class Lift1 (f :: Data.Kind.Type -> Data.Kind.Type) where
+    lift1 :: (Quote m, Lift t) => f t -> m Exp
+
+liftCon :: Quote m => TH.Name -> m Exp -> m Exp
+liftCon n = fmap (AppE (ConE n))
+
+liftCon2 :: Quote m => TH.Name -> m Exp -> m Exp -> m Exp
+liftCon2 n a b = do
+    a' <- a
+    b' <- b
+    pure $ ConE n `AppE` a' `AppE` b'
+
+liftCon3 :: Quote m => TH.Name -> m Exp -> m Exp -> m Exp -> m Exp
+liftCon3 n a b c = do
+    a' <- a
+    b' <- b
+    c' <- c
+    pure $ ConE n `AppE` a' `AppE` b' `AppE` c'
+
+instance Lift1 f => Lift (Fix f) where
+    lift (Fix f) = AppE (ConE 'Fix) <$> lift1 f
+
+
--- a/src/Rlp/Lex.x
+++ b/src/Rlp/Lex.x
@@ -8,6 +8,7 @@ module Rlp.Lex
    , Located(..)
    , lexToken
    , lexStream
+    , lexStream'
    , lexDebug
    , lexCont
    , popLexState
@@ -29,6 +30,7 @@ import Data.Word
 import Data.Default
 import Control.Lens

+import Compiler.Types
 import Debug.Trace
 import Rlp.Parse.Types
 }
@@ -274,11 +276,12 @@ lexCont :: (Located RlpToken -> P a) -> P a
 lexCont = (lexToken >>=)

 lexStream :: P [RlpToken]
-lexStream = do
-    t <- lexToken
-    case t of
-        Located _ TokenEOF -> pure [TokenEOF]
-        Located _ t        -> (t:) <$> lexStream
+lexStream = fmap extract <$> lexStream'
+
+lexStream' :: P [Located RlpToken]
+lexStream' = lexToken >>= \case
+    t@(Located _ TokenEOF) -> pure [t]
+    t        -> (t:) <$> lexStream'

 lexDebug :: (Located RlpToken -> P a) -> P a
 lexDebug k = do
--- a/src/Rlp/Parse.y
+++ b/src/Rlp/Parse.y
@@ -5,15 +5,17 @@ module Rlp.Parse
    , parseRlpProgR
    , parseRlpExpr
    , parseRlpExprR
+    , runP'
    )
    where
 import Compiler.RlpcError
 import Compiler.RLPC
+import Control.Comonad.Cofree
 import Rlp.Lex
 import Rlp.Syntax
 import Rlp.Parse.Types
 import Rlp.Parse.Associate
-import Control.Lens                 hiding (snoc, (.>), (<.), (<<~))
+import Control.Lens                 hiding (snoc, (.>), (<.), (<<~), (:<))
 import Data.List.Extra
 import Data.Fix
 import Data.Functor.Const
@@ -71,12 +73,11 @@ import Compiler.Types

 %%

-StandaloneProgram   :: { RlpProgram RlpcPs }
-StandaloneProgram   : '{' Decls  '}'        {% mkProgram $2 }
-                    | VL  DeclsV VR         {% mkProgram $2 }
+StandaloneProgram   :: { Program RlpcPs SrcSpan }
+StandaloneProgram   : layout0(Decl)         {% mkProgram $1 }

-StandaloneExpr      :: { RlpExpr RlpcPs }
-                    : VL Expr VR            { extract $2 }
+StandaloneExpr      :: { Expr' RlpcPs SrcSpan }
+                    : VL Expr VR            { $2 }

 VL  :: { () }
 VL  : vlbrace       { () }
@@ -85,125 +86,105 @@ VR  :: { () }
 VR  : vrbrace       { () }
    | error         { () }

-Decls               :: { [Decl' RlpcPs] }
-Decls               : Decl ';' Decls        { $1 : $3 }
-                    | Decl ';'              { [$1] }
-                    | Decl                  { [$1] }
+VS                  :: { () }
+VS                  : ';'                   { () }
+                    | vsemi                 { () }

-DeclsV              :: { [Decl' RlpcPs] }
-DeclsV              : Decl VS DeclsV        { $1 : $3 }
-                    | Decl VS               { [$1] }
-                    | Decl                  { [$1] }
-
-VS                  :: { Located RlpToken }
-VS                  : ';'                   { $1 }
-                    | vsemi                 { $1 }
-
-Decl        :: { Decl' RlpcPs }
+Decl        :: { Decl RlpcPs SrcSpan }
            : FunDecl                   { $1 }
            | TySigDecl                 { $1 }
            | DataDecl                  { $1 }
            | InfixDecl                 { $1 }

-TySigDecl   :: { Decl' RlpcPs }
-            : Var '::' Type             { (\e -> TySigD [extract e]) <<~ $1 <~> $3 }
+TySigDecl   :: { Decl RlpcPs SrcSpan }
+            : Var '::' Type             { TySigD [$1] $3 }

-InfixDecl   :: { Decl' RlpcPs }
-            : InfixWord litint InfixOp  { $1 =>> \w ->
-                                          InfixD (extract $1) (extractInt $ extract $2)
-                                          (extract $3) }
+InfixDecl   :: { Decl RlpcPs SrcSpan }
+            : InfixWord litint InfixOp  {% mkInfixD $1 ($2 ^. _litint) $3 }

-InfixWord   :: { Located Assoc }
-            : infixl                    { $1 \$> InfixL }
-            | infixr                    { $1 \$> InfixR }
-            | infix                     { $1 \$> Infix  }
+InfixWord   :: { Assoc }
+            : infixl                    { InfixL }
+            | infixr                    { InfixR }
+            | infix                     { Infix }

-DataDecl    :: { Decl' RlpcPs }
-            : data Con TyParams '=' DataCons    { $1 \$> DataD (extract $2) $3 $5 }
+DataDecl    :: { Decl RlpcPs SrcSpan }
+            : data Con TyParams '=' DataCons    { DataD $2 $3 $5 }

 TyParams    :: { [PsName] }
            : {- epsilon -}             { [] }
-            | TyParams varname          { $1 `snoc` (extractName . extract $ $2) }
+            | TyParams varname          { $1 `snoc` extractName $2 }

 DataCons    :: { [ConAlt RlpcPs] }
            : DataCons '|' DataCon      { $1 `snoc` $3 }
            | DataCon                   { [$1] }

 DataCon     :: { ConAlt RlpcPs }
-            : Con Type1s                { ConAlt (extract $1) $2 }
+            : Con Type1s                { ConAlt $1 $2 }

-Type1s      :: { [RlpType' RlpcPs] }
+Type1s      :: { [Ty RlpcPs] }
            : {- epsilon -}             { [] }
            | Type1s Type1              { $1 `snoc` $2 }

-Type1       :: { RlpType' RlpcPs }
+Type1       :: { Ty RlpcPs }
            : '(' Type ')'              { $2 }
-            | conname                   { fmap ConT (mkPsName $1) }
-            | varname                   { fmap VarT (mkPsName $1) }
+            | conname                   { ConT (extractName $1) }
+            | varname                   { VarT (extractName $1) }

-Type        :: { RlpType' RlpcPs }
-            : Type '->' Type            { FunT <<~ $1 <~> $3 }
+Type        :: { Ty RlpcPs }
+            : Type '->' Type            { FunT $1 $3 }
            | TypeApp                   { $1 }

-TypeApp     :: { RlpType' RlpcPs }
+TypeApp     :: { Ty RlpcPs }
            : Type1                     { $1 }
-            | TypeApp Type1             { AppT <<~ $1 <~> $2 }
+            | TypeApp Type1             { AppT $1 $2 }

-FunDecl     :: { Decl' RlpcPs }
-FunDecl     : Var Params '=' Expr       { $4 =>> \e ->
-                                          FunD (extract $1) $2 e Nothing }
+FunDecl     :: { Decl RlpcPs SrcSpan }
+FunDecl     : Var Params '=' Expr       { FunD $1 $2 $4 Nothing }

-Params      :: { [Pat' RlpcPs] }
+Params      :: { [Pat RlpcPs] }
 Params      : {- epsilon -}             { [] }
            | Params Pat1               { $1 `snoc` $2 }

-Pat         :: { Pat' RlpcPs }
-            : Con Pat1s                 { $1 =>> \cn ->
-                                          ConP (extract $1) $2 }
+Pat         :: { Pat RlpcPs }
+            : Con Pat1s                 { ConP $1 $2 }
            | Pat1                      { $1 }

-Pat1s       :: { [Pat' RlpcPs] }
+Pat1s       :: { [Pat RlpcPs] }
            : Pat1s Pat1                { $1 `snoc` $2 }
            | Pat1                      { [$1] }

-Pat1        :: { Pat' RlpcPs }
-            : Con                       { fmap (`ConP` []) $1 }
-            | Var                       { fmap VarP $1 }
-            | Lit                       { LitP <<= $1 }
-            | '(' Pat ')'               { $1 .> $2 <. $3 }
+Pat1        :: { Pat RlpcPs }
+            : Con                       { ConP $1 [] }
+            | Var                       { VarP $1 }
+            | Lit                       { LitP $1 }
+            | '(' Pat ')'               { $2 }

-Expr        :: { RlpExpr' RlpcPs }
+Expr        :: { Expr' RlpcPs SrcSpan }
            -- infixities delayed till next release :(
-            -- : Expr1 InfixOp Expr        { $2 =>> \o ->
-            --                              OAppE (extract o) $1 $3 }
-            : TempInfixExpr             { $1 }
+            -- : Expr1 InfixOp Expr        { undefined }
+            : AppExpr                   { $1 }
+            | TempInfixExpr             { $1 }
            | LetExpr                   { $1 }
            | CaseExpr                  { $1 }
-            | AppExpr                   { $1 }

-TempInfixExpr :: { RlpExpr' RlpcPs }
+TempInfixExpr :: { Expr' RlpcPs SrcSpan }
 TempInfixExpr : Expr1 InfixOp TempInfixExpr {% tempInfixExprErr $1 $3 }
-              | Expr1 InfixOp Expr1 { $2 =>> \o ->
-                                      OAppE (extract o) $1 $3 }
+              | Expr1 InfixOp Expr1         { nolo' $ InfixEF $2 $1 $3 }

-AppExpr     :: { RlpExpr' RlpcPs }
+AppExpr     :: { Expr' RlpcPs SrcSpan }
            : Expr1                     { $1 }
-            | AppExpr Expr1             { AppE <<~ $1 <~> $2 }
+            | AppExpr Expr1             { comb2 AppEF $1 $2 }

-LetExpr     :: { RlpExpr' RlpcPs }
-            : let layout1(Binding) in Expr      { $1 \$> LetE $2 $4 }
-            | letrec layout1(Binding) in Expr   { $1 \$> LetrecE $2 $4 }
+LetExpr     :: { Expr' RlpcPs SrcSpan }
+            : let layout1(Binding) in Expr      { nolo' $ LetEF NonRec $2 $4 }
+            | letrec layout1(Binding) in Expr   { nolo' $ LetEF Rec $2 $4 }

-CaseExpr    :: { RlpExpr' RlpcPs }
-            : case Expr of layout0(CaseAlt)
-                { CaseE <<~ $2 <#> $4 }
+CaseExpr    :: { Expr' RlpcPs SrcSpan }
+            : case Expr of layout0(Alt)     { nolo' $ CaseEF $2 $4 }

 -- TODO: where-binds
-CaseAlt     :: { (Alt RlpcPs, Where RlpcPs) }
-            : Alt                           { ($1, []) }
-
-Alt         :: { Alt RlpcPs }
-            : Pat '->' Expr                 { AltA $1 $3 }
+Alt         :: { Alt' RlpcPs SrcSpan }
+            : Pat '->' Expr                 { AltA $1 (view _unwrap $3) Nothing }

 -- layout0(p : β) :: [β]
 layout0(p)  : '{' layout_list0(';',p) '}'   { $2 }
@@ -222,38 +203,68 @@ layout1(p)  : '{' layout_list1(';',p) '}'   { $2 }
 layout_list1(sep,p) : p                          { [$1] }
                    | layout_list1(sep,p) sep p  { $1 `snoc` $3 }

-Binding     :: { Binding' RlpcPs }
-            : Pat '=' Expr              { PatB <<~ $1 <~> $3 }
+Binding     :: { Binding' RlpcPs SrcSpan }
+            : Pat '=' Expr              { PatB $1 (view _unwrap $3) }

-Expr1       :: { RlpExpr' RlpcPs }
-            : '(' Expr ')'              { $1 .> $2 <. $3 }
-            | Lit                       { fmap LitE $1 }
-            | Var                       { fmap VarE $1 }
-            | Con                       { fmap VarE $1 }
+Expr1       :: { Expr' RlpcPs SrcSpan }
+            : '(' Expr ')'              { $2 }
+            | Lit                       { nolo' $ LitEF $1 }
+            | Var                       { case $1 of Located ss _ -> ss :< VarEF $1 }
+            | Con                       { case $1 of Located ss _ -> ss :< VarEF $1 }

-InfixOp     :: { Located PsName }
-            : consym                    { mkPsName $1 }
-            | varsym                    { mkPsName $1 }
+InfixOp     :: { PsName }
+            : consym                    { extractName $1 }
+            | varsym                    { extractName $1 }

 -- TODO: microlens-pro save me microlens-pro (rewrite this with prisms)
-Lit         :: { Lit' RlpcPs }
-            : litint                    { $1 <&> (IntL . (\ (TokenLitInt n) -> n)) }
+Lit         :: { Lit RlpcPs }
+            : litint                    { $1 ^. to extract
+                                              . singular _TokenLitInt
+                                              . to IntL }

-Var         :: { Located PsName }
-Var         : varname                   { mkPsName $1 }
-            | varsym                    { mkPsName $1 }
+Var         :: { PsName }
+Var         : varname                   { $1 <&> view (singular _TokenVarName) }
+            | varsym                    { $1 <&> view (singular _TokenVarSym) }

-Con         :: { Located PsName }
-            : conname                   { mkPsName $1 }
+Con         :: { PsName }
+            : conname                   { $1 <&> view (singular _TokenConName) }

 {

-parseRlpExprR :: (Monad m) => Text -> RLPCT m (RlpExpr RlpcPs)
+parseRlpProgR :: (Monad m) => Text -> RLPCT m (Program RlpcPs SrcSpan)
+parseRlpProgR s = do
+    a <- liftErrorful $ pToErrorful parseRlpProg st
+    addDebugMsg @_ @String "dump-parsed" $ show a
+    pure a
+  where
+    st = programInitState s
+
+parseRlpExprR :: (Monad m) => Text -> RLPCT m (Expr' RlpcPs SrcSpan)
 parseRlpExprR s = liftErrorful $ pToErrorful parseRlpExpr st
    where
        st = programInitState s

-parseRlpProgR :: (Monad m) => Text -> RLPCT m (RlpProgram RlpcPs)
+mkInfixD :: Assoc -> Int -> PsName -> P (Decl RlpcPs SrcSpan)
+mkInfixD a p ln@(Located ss n) = do
+    let opl :: Lens' ParseState (Maybe OpInfo)
+        opl = psOpTable . at n
+    opl <~ (use opl >>= \case
+        Just o  -> addWoundHere l e >> pure (Just o) where
+            e = RlpParErrDuplicateInfixD n
+            l = T.length n
+        Nothing -> pure (Just (a,p))
+        )
+    pos <- use (psInput . aiPos)
+    pure $ InfixD a p ln
+
+{--
+
+parseRlpExprR :: (Monad m) => Text -> RLPCT m (Expr RlpcPs)
+parseRlpExprR s = liftErrorful $ pToErrorful parseRlpExpr st
+    where
+        st = programInitState s
+
+parseRlpProgR :: (Monad m) => Text -> RLPCT m (Program RlpcPs)
 parseRlpProgR s = do
    a <- liftErrorful $ pToErrorful parseRlpProg st
    addDebugMsg @_ @String "dump-parsed" $ show a
@@ -276,37 +287,48 @@ extractInt :: RlpToken -> Int
 extractInt (TokenLitInt n) = n
 extractInt _ = error "extractInt: ugh"

-mkProgram :: [Decl' RlpcPs] -> P (RlpProgram RlpcPs)
+mkProgram :: [Decl RlpcPs SrcSpan] -> P (Program RlpcPs SrcSpan)
 mkProgram ds = do
    pt <- use psOpTable
-    pure $ RlpProgram (associate pt <$> ds)
-
-parseError :: (Located RlpToken, [String]) -> P a
-parseError ((Located ss t), exp) = addFatal $
-    errorMsg ss (RlpParErrUnexpectedToken t exp)
-
-mkInfixD :: Assoc -> Int -> PsName -> P (Decl' RlpcPs)
-mkInfixD a p n = do
-    let opl :: Lens' ParseState (Maybe OpInfo)
-        opl = psOpTable . at n
-    opl <~ (use opl >>= \case
-        Just o  -> addWoundHere l e >> pure (Just o) where
-            e = RlpParErrDuplicateInfixD n
-            l = T.length n
-        Nothing -> pure (Just (a,p))
-        )
-    pos <- use (psInput . aiPos)
-    pure $ Located (spanFromPos pos 0) (InfixD a p n)
+    pure $ Program (associate pt <$> ds)

 intOfToken :: Located RlpToken -> Int
 intOfToken (Located _ (TokenLitInt n)) = n

-tempInfixExprErr :: RlpExpr' RlpcPs -> RlpExpr' RlpcPs -> P a
+tempInfixExprErr :: Expr RlpcPs -> Expr RlpcPs -> P a
 tempInfixExprErr (Located a _) (Located b _) =
    addFatal $ errorMsg (a <> b) $ RlpParErrOther
        [ "The rl' frontend is currently in beta. Support for infix expressions is minimal, sorry! :("
        , "In the mean time, don't mix any infix operators."
        ]

+--}
+
+_litint :: Getter (Located RlpToken) Int
+_litint = to extract
+        . singular _TokenLitInt
+
+tempInfixExprErr :: Expr' RlpcPs SrcSpan -> Expr' RlpcPs SrcSpan -> P a
+tempInfixExprErr (a :< _) (b :< _) =
+    addFatal $ errorMsg (a <> b) $ RlpParErrOther
+        [ "The rl' frontend is currently in beta. Support for infix expressions is minimal, sorry! :("
+        , "In the mean time, don't mix any infix operators."
+        ]
+
+mkProgram :: [Decl RlpcPs SrcSpan] -> P (Program RlpcPs SrcSpan)
+mkProgram ds = do
+    pt <- use psOpTable
+    pure $ Program (associate pt <$> ds)
+
+extractName :: Located RlpToken -> PsName
+extractName (Located ss (TokenVarSym n)) = Located ss n
+extractName (Located ss (TokenVarName n)) = Located ss n
+extractName (Located ss (TokenConName n)) = Located ss n
+extractName (Located ss (TokenConSym n)) = Located ss n
+
+parseError :: (Located RlpToken, [String]) -> P a
+parseError ((Located ss t), exp) = addFatal $
+    errorMsg ss (RlpParErrUnexpectedToken t exp)
+
 }

--- a/src/Rlp/Parse/Associate.hs
+++ b/src/Rlp/Parse/Associate.hs
@@ -16,7 +16,7 @@ import Rlp.Parse.Types
 import Rlp.Syntax
 --------------------------------------------------------------------------------

-associate :: OpTable -> Decl' RlpcPs -> Decl' RlpcPs
+associate :: OpTable -> Decl RlpcPs a -> Decl RlpcPs a
 associate _ p = p

 {-# WARNING associate "unimplemented" #-}
--- a/src/Rlp/Parse/Types.hs
+++ b/src/Rlp/Parse/Types.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE ImplicitParams, ViewPatterns, PatternSynonyms #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE UndecidableInstances #-}
 module Rlp.Parse.Types
    (
    -- * Trees That Grow
@@ -17,10 +18,9 @@ module Rlp.Parse.Types
    , RlpToken(..), AlexInput(..), Position(..), spanFromPos, LexerAction
    , Located(..), PsName
    -- ** Lenses
+    , _TokenLitInt, _TokenVarName, _TokenConName, _TokenVarSym
    , aiPrevChar, aiSource, aiBytes, aiPos, posLine, posColumn

-    , (<<~), (<~>)
-
    -- * Error handling
    , MsgEnvelope(..), RlpcError(..), RlpParseError(..)
    , addFatal, addWound, addFatalHere, addWoundHere
@@ -28,6 +28,7 @@ module Rlp.Parse.Types
    where
 --------------------------------------------------------------------------------
 import Core.Syntax                  (Name)
+import Text.Show.Deriving
 import Control.Monad
 import Control.Monad.State.Strict
 import Control.Monad.Errorful
@@ -53,34 +54,9 @@ import Compiler.Types

 data RlpcPs

-type instance XRec RlpcPs a = Located a
-type instance IdP RlpcPs = PsName
+type instance NameP RlpcPs = PsName

-type instance XFunD RlpcPs = ()
-type instance XDataD RlpcPs = ()
-type instance XInfixD RlpcPs = ()
-type instance XTySigD RlpcPs = ()
-type instance XXDeclD RlpcPs = ()
-
-type instance XLetE RlpcPs = ()
-type instance XLetrecE RlpcPs = ()
-type instance XVarE RlpcPs = ()
-type instance XLamE RlpcPs = ()
-type instance XCaseE RlpcPs = ()
-type instance XIfE RlpcPs = ()
-type instance XAppE RlpcPs = ()
-type instance XLitE RlpcPs = ()
-type instance XParE RlpcPs = ()
-type instance XOAppE RlpcPs = ()
-type instance XXRlpExprE RlpcPs = ()
-
-type PsName = Text
-
-instance MapXRec RlpcPs where
-    mapXRec = fmap
-
-instance UnXRec RlpcPs where
-    unXRec = extract
+type PsName = Located Text

 --------------------------------------------------------------------------------

@@ -118,10 +94,10 @@ data RlpToken
    -- literals
    = TokenLitInt Int
    -- identifiers
-    | TokenVarName Name
-    | TokenConName Name
-    | TokenVarSym Name
-    | TokenConSym Name
+    | TokenVarName Text
+    | TokenConName Text
+    | TokenVarSym Text
+    | TokenConSym Text
    -- reserved words
    | TokenData
    | TokenCase
@@ -152,6 +128,31 @@ data RlpToken
    | TokenEOF
    deriving (Show)

+_TokenLitInt :: Prism' RlpToken Int
+_TokenLitInt = prism TokenLitInt $ \case
+    TokenLitInt n -> Right n
+    x             -> Left x
+
+_TokenVarName :: Prism' RlpToken Text
+_TokenVarName = prism TokenVarName $ \case
+    TokenVarName n -> Right n
+    x              -> Left x
+
+_TokenVarSym :: Prism' RlpToken Text
+_TokenVarSym = prism TokenVarSym $ \case
+    TokenVarSym n -> Right n
+    x              -> Left x
+
+_TokenConName :: Prism' RlpToken Text
+_TokenConName = prism TokenConName $ \case
+    TokenConName n -> Right n
+    x              -> Left x
+
+_TokenConSym :: Prism' RlpToken Text
+_TokenConSym = prism TokenConSym $ \case
+    TokenConSym n -> Right n
+    x              -> Left x
+
 newtype P a = P {
        runP :: ParseState
             -> (ParseState, [MsgEnvelope RlpParseError], Maybe a)
@@ -281,13 +282,14 @@ initAlexInput s = AlexInput

 --------------------------------------------------------------------------------

-deriving instance Lift (RlpProgram RlpcPs)
-deriving instance Lift (Decl RlpcPs)
-deriving instance Lift (Pat RlpcPs)
-deriving instance Lift (Lit RlpcPs)
-deriving instance Lift (RlpExpr RlpcPs)
-deriving instance Lift (Binding RlpcPs)
-deriving instance Lift (RlpType RlpcPs)
-deriving instance Lift (Alt RlpcPs)
-deriving instance Lift (ConAlt RlpcPs)
+
+-- deriving instance Lift (Program RlpcPs)
+-- deriving instance Lift (Decl RlpcPs)
+-- deriving instance Lift (Pat RlpcPs)
+-- deriving instance Lift (Lit RlpcPs)
+-- deriving instance Lift (Expr RlpcPs)
+-- deriving instance Lift (Binding RlpcPs)
+-- deriving instance Lift (Ty RlpcPs)
+-- deriving instance Lift (Alt RlpcPs)
+-- deriving instance Lift (ConAlt RlpcPs)

--- a/src/Rlp/Syntax.hs
+++ b/src/Rlp/Syntax.hs
@@ -1,362 +1,10 @@
-- recursion-schemes
-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable
-  , TemplateHaskell, TypeFamilies #-}
-{-# LANGUAGE OverloadedStrings, PatternSynonyms, ViewPatterns #-}
-{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
-{-# LANGUAGE UndecidableInstances, ImpredicativeTypes #-}
 module Rlp.Syntax
-    (
-    -- * AST
-      RlpProgram(..)
-    , progDecls
-    , Decl(..), Decl', RlpExpr(..), RlpExpr', RlpExprF(..)
-    , Pat(..), Pat'
-    , Alt(..), Where
-    , Assoc(..)
-    , Lit(..), Lit'
-    , RlpType(..), RlpType'
-    , ConAlt(..)
-    , Binding(..), Binding'
-
-    , _PatB, _FunB
-    , _VarP, _LitP, _ConP
-
-    -- * Trees That Grow boilerplate
-    -- ** Extension points
-    , IdP, IdP', XRec, UnXRec(..), MapXRec(..)
-    -- *** Decl
-    , XFunD, XTySigD, XInfixD, XDataD, XXDeclD
-    -- *** RlpExpr
-    , XLetE, XLetrecE, XVarE, XLamE, XCaseE, XIfE, XAppE, XLitE
-    , XParE, XOAppE, XXRlpExprE
-    -- ** Pattern synonyms
-    -- *** Decl
-    , pattern FunD, pattern TySigD, pattern InfixD, pattern DataD
-    , pattern FunD'', pattern TySigD'', pattern InfixD'', pattern DataD''
-    -- *** RlpExpr
-    , pattern LetE, pattern LetrecE, pattern VarE, pattern LamE, pattern CaseE
-    , pattern IfE , pattern AppE, pattern LitE, pattern ParE, pattern OAppE
-    , pattern XRlpExprE
-    -- *** RlpType
-    , pattern FunConT'', pattern FunT'', pattern AppT'', pattern VarT''
-    , pattern ConT''
-    -- *** Pat
-    , pattern VarP'', pattern LitP'', pattern ConP''
-    -- *** Binding
-    , pattern PatB''
+    ( module Rlp.Syntax.Backstage
+    , module Rlp.Syntax.Types
    )
    where
----------------------------------------------------------------------------------
-import Data.Text                    (Text)
-import Data.Text                    qualified as T
-import Data.String                  (IsString(..))
-import Data.Functor.Foldable
-import Data.Functor.Foldable.TH     (makeBaseFunctor)
-import Data.Functor.Classes
-import Data.Functor.Identity
-import Data.Kind                    (Type)
-import GHC.Generics
-import Language.Haskell.TH.Syntax   (Lift)
-import Control.Lens
-import Core.Syntax                  hiding (Lit, Type, Binding, Binding')
-import Core                         (HasRHS(..), HasLHS(..))
----------------------------------------------------------------------------------
-
-data RlpModule p = RlpModule
-    { _rlpmodName       :: Text
-    , _rlpmodProgram    :: RlpProgram p
-    }
-
-- | dear god.
-type PhaseShow p =
-    ( Show (XRec p (Pat p)), Show (XRec p (RlpExpr p))
-    , Show (XRec p (Lit p)), Show (IdP p)
-    , Show (XRec p (RlpType p))
-    , Show (XRec p (Binding p))
-    )
-
-newtype RlpProgram p = RlpProgram [Decl' p]
-
-progDecls :: Lens' (RlpProgram p) [Decl' p]
-progDecls = lens
-    (\ (RlpProgram ds) -> ds)
-    (const RlpProgram)
-
-deriving instance (PhaseShow p, Show (XRec p (Decl p))) => Show (RlpProgram p)
-
-data RlpType p = FunConT
-               | FunT (RlpType' p) (RlpType' p)
-               | AppT (RlpType' p) (RlpType' p)
-               | VarT (IdP p)
-               | ConT (IdP p)
-
-type RlpType' p = XRec p (RlpType p)
-
-pattern FunConT'' :: (UnXRec p) => RlpType' p
-pattern FunT''    :: (UnXRec p) => RlpType' p -> RlpType' p -> RlpType' p
-pattern AppT''    :: (UnXRec p) => RlpType' p -> RlpType' p -> RlpType' p
-pattern VarT''    :: (UnXRec p) => IdP p -> RlpType' p
-pattern ConT''    :: (UnXRec p) => IdP p -> RlpType' p
-
-pattern FunConT''     <- (unXRec -> FunConT)
-pattern FunT''    s t <- (unXRec -> FunT s t)
-pattern AppT''    s t <- (unXRec -> AppT s t)
-pattern VarT''    n   <- (unXRec -> VarT n)
-pattern ConT''    n   <- (unXRec -> ConT n)
-
-deriving instance (PhaseShow p)
-                  => Show (RlpType p)
-
-data Decl p = FunD'   (XFunD p)    (IdP p) [Pat' p] (RlpExpr' p) (Maybe (Where p))
-            | TySigD' (XTySigD p)  [IdP p] (RlpType' p)
-            | DataD'  (XDataD p)   (IdP p) [IdP p] [ConAlt p]
-            | InfixD' (XInfixD p)  Assoc Int (IdP p)
-            | XDeclD' !(XXDeclD p)
-
-deriving instance
-    ( Show (XFunD p), Show (XTySigD p)
-    , Show (XDataD p), Show (XInfixD p)
-    , Show (XXDeclD p)
-    , PhaseShow p
-    ) 
-    => Show (Decl p)
-
-type family XFunD p
-type family XTySigD p
-type family XDataD p
-type family XInfixD p
-type family XXDeclD p
-
-pattern FunD   :: (XFunD p ~ ())
-               => IdP p -> [Pat' p] -> RlpExpr' p -> Maybe (Where p)
-               -> Decl p
-pattern TySigD :: (XTySigD p ~ ()) => [IdP p] -> RlpType' p -> Decl p
-pattern DataD  :: (XDataD p ~ ()) => IdP p -> [IdP p] -> [ConAlt p] -> Decl p
-pattern InfixD :: (XInfixD p ~ ()) => Assoc -> Int -> IdP p -> Decl p
-pattern XDeclD :: (XXDeclD p ~ ()) => Decl p
-
-pattern FunD n as e wh = FunD' () n as e wh
-pattern TySigD ns t    = TySigD' () ns t
-pattern DataD n as cs  = DataD' () n as cs
-pattern InfixD a p n   = InfixD' () a p n
-pattern XDeclD         = XDeclD' ()
-
-pattern FunD''   :: (UnXRec p)
-                 => IdP p -> [Pat' p] -> RlpExpr' p -> Maybe (Where p)
-                 -> Decl' p
-pattern TySigD'' :: (UnXRec p)
-                 => [IdP p] -> RlpType' p -> Decl' p
-pattern DataD''  :: (UnXRec p)
-                 => IdP p -> [IdP p] -> [ConAlt p] -> Decl' p
-pattern InfixD'' :: (UnXRec p)
-                 => Assoc -> Int -> IdP p -> Decl' p
-
-pattern FunD''   n as e wh <- (unXRec -> FunD' _ n as e wh)
-pattern TySigD'' ns t      <- (unXRec -> TySigD' _ ns t)
-pattern DataD''  n as ds   <- (unXRec -> DataD' _ n as ds)
-pattern InfixD'' a p n     <- (unXRec -> InfixD' _ a p n)
-
-type Decl' p = XRec p (Decl p)
-
-data Assoc = InfixL
-           | InfixR
-           | Infix
-           deriving (Show, Lift)
-
-data ConAlt p = ConAlt (IdP p) [RlpType' p]
-
-deriving instance (Show (IdP p), Show (XRec p (RlpType p))) => Show (ConAlt p)
-
-data RlpExpr p = LetE'      (XLetE p) [Binding' p] (RlpExpr' p)
-               | LetrecE'   (XLetrecE p) [Binding' p] (RlpExpr' p)
-               | VarE'      (XVarE p) (IdP p)
-               | LamE'      (XLamE p) [Pat p] (RlpExpr' p)
-               | CaseE'     (XCaseE p) (RlpExpr' p) [(Alt p, Where p)]
-               | IfE'       (XIfE p) (RlpExpr' p) (RlpExpr' p) (RlpExpr' p)
-               | AppE'      (XAppE p) (RlpExpr' p) (RlpExpr' p)
-               | LitE'      (XLitE p) (Lit p)
-               | ParE'      (XParE p) (RlpExpr' p)
-               | OAppE'     (XOAppE p) (IdP p) (RlpExpr' p) (RlpExpr' p)
-               | XRlpExprE' !(XXRlpExprE p)
-               deriving (Generic)
-
-type family XLetE p
-type family XLetrecE p
-type family XVarE p
-type family XLamE p
-type family XCaseE p
-type family XIfE p
-type family XAppE p
-type family XLitE p
-type family XParE p
-type family XOAppE p
-type family XXRlpExprE p
-
-pattern LetE :: (XLetE p ~ ()) => [Binding' p] -> RlpExpr' p -> RlpExpr p
-pattern LetrecE :: (XLetrecE p ~ ()) => [Binding' p] -> RlpExpr' p -> RlpExpr p
-pattern VarE :: (XVarE p ~ ()) => IdP p -> RlpExpr p
-pattern LamE :: (XLamE p ~ ()) => [Pat p] -> RlpExpr' p -> RlpExpr p
-pattern CaseE :: (XCaseE p ~ ()) => RlpExpr' p -> [(Alt p, Where p)] -> RlpExpr p
-pattern IfE :: (XIfE p ~ ()) => RlpExpr' p -> RlpExpr' p -> RlpExpr' p -> RlpExpr p
-pattern AppE :: (XAppE p ~ ()) => RlpExpr' p -> RlpExpr' p -> RlpExpr p
-pattern LitE :: (XLitE p ~ ()) => Lit p -> RlpExpr p
-pattern ParE :: (XParE p ~ ()) => RlpExpr' p -> RlpExpr p
-pattern OAppE :: (XOAppE p ~ ()) => IdP p -> RlpExpr' p -> RlpExpr' p -> RlpExpr p
-pattern XRlpExprE :: (XXRlpExprE p ~ ()) => RlpExpr p
-
-pattern LetE bs e = LetE' () bs e
-pattern LetrecE bs e = LetrecE' () bs e
-pattern VarE n = VarE' () n
-pattern LamE as e = LamE' () as e
-pattern CaseE e as = CaseE' () e as
-pattern IfE c a b = IfE' () c a b
-pattern AppE f x = AppE' () f x
-pattern LitE l = LitE' () l
-pattern ParE e = ParE' () e
-pattern OAppE n a b = OAppE' () n a b
-pattern XRlpExprE = XRlpExprE' ()
-
-deriving instance
-    ( Show (XLetE p), Show (XLetrecE p), Show (XVarE p)
-    , Show (XLamE p), Show (XCaseE p), Show (XIfE p)
-    , Show (XAppE p), Show (XLitE p), Show (XParE p)
-    , Show (XOAppE p), Show (XXRlpExprE p)
-    , PhaseShow p
-    ) => Show (RlpExpr p)
-
-type RlpExpr' p = XRec p (RlpExpr p)
-
-class UnXRec p where
-    unXRec :: XRec p a -> a
-
-class WrapXRec p where
-    wrapXRec :: a -> XRec p a
-
-class MapXRec p where
-    mapXRec :: (a -> b) -> XRec p a -> XRec p b
-
-- old definition:
-- type family XRec p (f :: Type -> Type) = (r :: Type) | r -> p f
-type family XRec p a = (r :: Type) | r -> p a
-
-type family IdP p
-
-type IdP' p = XRec p (IdP p)
-
-type Where p = [Binding p]
-
-- do we want guards?
-data Alt p = AltA (Pat' p) (RlpExpr' p)
-
-deriving instance (PhaseShow p) => Show (Alt p)
-
-data Binding p = PatB (Pat' p) (RlpExpr' p)
-               | FunB (IdP p) [Pat' p] (RlpExpr' p)
-
-type Binding' p = XRec p (Binding p)
-
-pattern PatB'' :: (UnXRec p) => Pat' p -> RlpExpr' p -> Binding' p
-pattern PatB'' p e <- (unXRec -> PatB p e)
-
-deriving instance (Show (XRec p (Pat p)), Show (XRec p (RlpExpr p)), Show (IdP p)
-                  ) => Show (Binding p)
-
-data Pat p = VarP (IdP p)
-           | LitP (Lit' p)
-           | ConP (IdP p) [Pat' p]
-
-pattern VarP'' :: (UnXRec p) => IdP p -> Pat' p
-pattern LitP'' :: (UnXRec p) => Lit' p -> Pat' p
-pattern ConP'' :: (UnXRec p) => IdP p -> [Pat' p] -> Pat' p
-
-pattern VarP'' n    <- (unXRec -> VarP n)
-pattern LitP'' l    <- (unXRec -> LitP l)
-pattern ConP'' c as <- (unXRec -> ConP c as)
-
-deriving instance (PhaseShow p) => Show (Pat p)
-
-type Pat' p = XRec p (Pat p)
-
-data Lit p = IntL Int
-           | CharL Char
-           | ListL [RlpExpr' p]
-
-deriving instance (PhaseShow p) => Show (Lit p)
-
-type Lit' p = XRec p (Lit p)
-
-- instance HasLHS Alt Alt Pat Pat where
--     _lhs = lens
--         (\ (AltA p _) -> p)
--         (\ (AltA _ e) p' -> AltA p' e)
-
-- instance HasRHS Alt Alt RlpExpr RlpExpr where
--     _rhs = lens
--         (\ (AltA _ e) -> e)
--         (\ (AltA p _) e' -> AltA p e')
-
-- makeBaseFunctor ''RlpExpr
-
-- showsTernaryWith :: (Int -> x -> ShowS)
--                  -> (Int -> y -> ShowS)
--                  -> (Int -> z -> ShowS)
--                  -> String -> Int
--                  -> x -> y -> z
--                  -> ShowS
-- showsTernaryWith sa sb sc name p a b c = showParen (p > 10)
--     $ showString name
--     . showChar ' ' . sa 11 a 
--     . showChar ' ' . sb 11 b
--     . showChar ' ' . sc 11 c
-
+--------------------------------------------------------------------------------
+import Rlp.Syntax.Backstage
+import Rlp.Syntax.Types
 --------------------------------------------------------------------------------

-makeLenses ''RlpModule
-makePrisms ''Pat
-makePrisms ''Binding
-
--------------------------------------------------------------------------------
-
-data RlpExprF p a = LetE'F  (XLetE p) [Binding' p] a
-                  | LetrecE'F  (XLetrecE p) [Binding' p] a
-                  | VarE'F  (XVarE p) (IdP p)
-                  | LamE'F  (XLamE p) [Pat p] a
-                  | CaseE'F (XCaseE p) a [(Alt p, Where p)]
-                  | IfE'F   (XIfE p) a a a
-                  | AppE'F  (XAppE p) a a
-                  | LitE'F  (XLitE p) (Lit p)
-                  | ParE'F  (XParE p) a
-                  | OAppE'F (XOAppE p) (IdP p) a a
-                  | XRlpExprE'F !(XXRlpExprE p)
-                  deriving (Functor, Foldable, Traversable, Generic)
-
-type instance Base (RlpExpr p) = RlpExprF p
-
-instance (UnXRec p) => Recursive (RlpExpr p) where
-    project = \case
-        LetE' xx bs e   -> LetE'F xx bs (unXRec e)
-        LetrecE' xx bs e   -> LetrecE'F xx bs (unXRec e)
-        VarE' xx n      -> VarE'F xx n
-        LamE' xx ps e   -> LamE'F xx ps (unXRec e)
-        CaseE' xx e as  -> CaseE'F xx (unXRec e) as
-        IfE' xx a b c   -> IfE'F xx (unXRec a) (unXRec b) (unXRec c)
-        AppE' xx f x    -> AppE'F xx (unXRec f) (unXRec x)
-        LitE' xx l      -> LitE'F xx l
-        ParE' xx e      -> ParE'F xx (unXRec e)
-        OAppE' xx f a b -> OAppE'F xx f (unXRec a) (unXRec b)
-        XRlpExprE' xx   -> XRlpExprE'F xx
-
-instance (WrapXRec p) => Corecursive (RlpExpr p) where
-    embed = \case
-        LetE'F xx bs e   -> LetE' xx bs (wrapXRec e)
-        LetrecE'F xx bs e   -> LetrecE' xx bs (wrapXRec e)
-        VarE'F xx n      -> VarE' xx n
-        LamE'F xx ps e   -> LamE' xx ps (wrapXRec e)
-        CaseE'F xx e as  -> CaseE' xx (wrapXRec e) as
-        IfE'F xx a b c   -> IfE' xx (wrapXRec a) (wrapXRec b) (wrapXRec c)
-        AppE'F xx f x    -> AppE' xx (wrapXRec f) (wrapXRec x)
-        LitE'F xx l      -> LitE' xx l
-        ParE'F xx e      -> ParE' xx (wrapXRec e)
-        OAppE'F xx f a b -> OAppE' xx f (wrapXRec a) (wrapXRec b)
-        XRlpExprE'F xx   -> XRlpExprE' xx
-
--- a/src/Rlp/Syntax/Backstage.hs
+++ b/src/Rlp/Syntax/Backstage.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Rlp.Syntax.Backstage
+    ( strip
+    )
+    where
+--------------------------------------------------------------------------------
+import Data.Fix                     hiding (cata)
+import Data.Functor.Classes
+import Data.Functor.Foldable
+import Rlp.Syntax.Types
+import Text.Show.Deriving
+import Language.Haskell.TH.Syntax   (Lift)
+--------------------------------------------------------------------------------
+
+-- oprhan instances because TH
+
+instance (Show (NameP p)) => Show1 (Alt p) where
+    liftShowsPrec = $(makeLiftShowsPrec ''Alt)
+
+instance (Show (NameP p)) => Show1 (Binding p) where
+    liftShowsPrec = $(makeLiftShowsPrec ''Binding)
+
+instance (Show (NameP p)) => Show1 (ExprF p) where
+    liftShowsPrec = $(makeLiftShowsPrec ''ExprF)
+
+deriving instance (Lift (NameP p), Lift a) => Lift (Expr' p a)
+deriving instance (Lift (NameP p), Lift a) => Lift (Decl p a)
+deriving instance (Show (NameP p), Show a) => Show (Decl p a)
+
+deriving instance (Show (NameP p), Show a) => Show (Program p a)
+
+strip :: Functor f => Cofree f a -> Fix f
+strip (_ :< as) = Fix $ strip <$> as
+
--- a/src/Rlp/Syntax/Types.hs
+++ b/src/Rlp/Syntax/Types.hs
@@ -0,0 +1,143 @@
+-- recursion-schemes
+{-# LANGUAGE DeriveTraversable, TemplateHaskell, TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings, PatternSynonyms, ViewPatterns #-}
+{-# LANGUAGE UndecidableInstances, ImpredicativeTypes #-}
+module Rlp.Syntax.Types
+    (
+      NameP
+    , SimpleP
+    , Assoc(..)
+    , ConAlt(..)
+    , Alt(..), Alt'
+    , Ty(..)
+    , Binding(..), Binding'
+    , Expr', ExprF(..)
+    , Rec(..)
+    , Lit(..)
+    , Pat(..)
+    , Decl(..)
+    , Program(..)
+    , Where
+
+    -- * Re-exports
+    , Cofree(..)
+    , Trans.Cofree.CofreeF
+    , SrcSpan(..)
+    )
+    where
+----------------------------------------------------------------------------------
+import Data.Text                    (Text)
+import Data.Text                    qualified as T
+import Data.String                  (IsString(..))
+import Data.Functor.Classes
+import Data.Functor.Identity
+import Data.Functor.Compose
+import Data.Fix
+import Data.Kind                    (Type)
+import GHC.Generics
+import Language.Haskell.TH.Syntax   (Lift)
+import Control.Lens                 hiding ((:<))
+
+import Control.Comonad.Trans.Cofree qualified as Trans.Cofree
+import Control.Comonad.Cofree
+import Data.Functor.Foldable
+import Data.Functor.Foldable.TH     (makeBaseFunctor)
+
+import Compiler.Types               (SrcSpan(..), Located(..))
+import Core.Syntax                  qualified as Core
+import Core                         (Rec(..), HasRHS(..), HasLHS(..))
+----------------------------------------------------------------------------------
+
+data SimpleP
+
+type instance NameP SimpleP = String
+
+type family NameP p
+
+data ExprF p a = LetEF   Rec [Binding p a] a
+               | VarEF   (NameP p)
+               | LamEF   [Pat p] a
+               | CaseEF  a [Alt p a]
+               | IfEF    a a a
+               | AppEF   a a
+               | LitEF   (Lit p)
+               | ParEF   a
+               | InfixEF (NameP p) a a
+               deriving (Functor, Foldable, Traversable)
+
+data ConAlt p = ConAlt (NameP p) [Ty p]
+
+deriving instance (Lift (NameP p)) => Lift (ConAlt p)
+deriving instance (Show (NameP p)) => Show (ConAlt p)
+
+data Ty p = ConT (NameP p)
+          | VarT (NameP p)
+          | FunT (Ty p) (Ty p)
+          | AppT (Ty p) (Ty p)
+
+deriving instance (Show (NameP p)) => Show (Ty p)
+deriving instance (Lift (NameP p)) => Lift (Ty p)
+
+data Pat p = VarP (NameP p)
+           | LitP (Lit p)
+           | ConP (NameP p) [Pat p]
+
+deriving instance (Lift (NameP p)) => Lift (Pat p)
+deriving instance (Show (NameP p)) => Show (Pat p)
+
+data Lit p = IntL Int
+    deriving Show
+
+deriving instance (Lift (NameP p)) => Lift (Lit p)
+
+data Assoc = InfixL | InfixR | Infix
+    deriving (Lift, Show)
+
+deriving instance (Show (NameP p), Show a) => Show (ExprF p a)
+deriving instance (Lift (NameP p), Lift a) => Lift (ExprF p a)
+
+data Binding p a = PatB (Pat p) (ExprF p a)
+    deriving (Functor, Foldable, Traversable)
+
+deriving instance (Lift (NameP p), Lift a) => Lift (Binding p a)
+deriving instance (Show (NameP p), Show a) => Show (Binding p a)
+
+type Binding' p a = Binding p (Cofree (ExprF p) a)
+
+type Where p a = [Binding p a]
+
+data Alt p a = AltA (Pat p) (ExprF p a) (Maybe (Where p a))
+    deriving (Functor, Foldable, Traversable)
+
+deriving instance (Show (NameP p), Show a) => Show (Alt p a)
+deriving instance (Lift (NameP p), Lift a) => Lift (Alt p a)
+
+type Expr p = Fix (ExprF p)
+
+type Alt' p a = Alt p (Cofree (ExprF p) a)
+
+--------------------------------------------------------------------------------
+
+data Program p a = Program
+    { _programDecls :: [Decl p a]
+    }
+
+data Decl p a = FunD   (NameP p) [Pat p] (Expr' p a) (Maybe (Where p a))
+              | TySigD [NameP p] (Ty p)
+              | DataD  (NameP p) [NameP p] [ConAlt p]
+              | InfixD Assoc Int (NameP p)
+
+type Decl' p a = Decl p (Cofree (ExprF p) a)
+
+type Expr' p = Cofree (ExprF p)
+
+makeLenses ''Program
+
+loccof :: Iso' (Cofree f SrcSpan) (Located (f (Cofree f SrcSpan)))
+loccof = iso sa bt where
+    sa :: Cofree f SrcSpan -> Located (f (Cofree f SrcSpan))
+    sa (ss :< as) = Located ss as
+
+    bt :: Located (f (Cofree f SrcSpan)) -> Cofree f SrcSpan
+    bt (Located ss as) = ss :< as
+
--- a/src/Rlp/TH.hs
+++ b/src/Rlp/TH.hs
@@ -17,10 +17,12 @@ import Rlp.Parse
 --------------------------------------------------------------------------------

 rlpProg :: QuasiQuoter
-rlpProg = mkqq parseRlpProgR
+rlpProg = undefined
+-- rlpProg = mkqq parseRlpProgR

 rlpExpr :: QuasiQuoter
-rlpExpr = mkqq parseRlpExprR
+rlpExpr = undefined
+-- rlpExpr = mkqq parseRlpExprR

 mkq :: (Lift a) => (Text -> RLPCIO a) -> String -> Q Exp
 mkq parse = evalAndParse >=> lift where
--- a/src/Rlp2Core.hs
+++ b/src/Rlp2Core.hs
@@ -41,6 +41,12 @@ import Rlp.Syntax                       as Rlp
 import Rlp.Parse.Types                  (RlpcPs, PsName)
 --------------------------------------------------------------------------------

+desugarRlpProgR = undefined
+desugarRlpProg = undefined
+desugarRlpExpr = undefined
+
+{--
+
 type Tree a = Either Name (Name, Branch a)

 -- | Rose tree branch representing "nested" "patterns" in the Core language. That
@@ -234,3 +240,5 @@ typeToCore (VarT'' x)   = TyVar (dsNameToName x)
 dsNameToName :: IdP RlpcPs -> Name
 dsNameToName = id

+-}
+
--- a/tst/Compiler/TypesSpec.hs
+++ b/tst/Compiler/TypesSpec.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE ParallelListComp #-}
+module Compiler.TypesSpec
+    ( spec
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Lens.Combinators
+import Data.Function            ((&))
+
+import Test.QuickCheck
+import Test.Hspec
+
+import Compiler.Types           (SrcSpan(..), srcSpanAbs, srcSpanLen)
+--------------------------------------------------------------------------------
+
+spec :: Spec
+spec = do
+    describe "SrcSpan" $ do
+        -- it "associates under closure"
+        --     prop_SrcSpan_mul_associative
+        it "commutes under closure"
+            prop_SrcSpan_mul_commutative
+        it "equals itself when squared"
+            prop_SrcSpan_mul_square_eq
+
+prop_SrcSpan_mul_associative :: Property
+prop_SrcSpan_mul_associative = property $ \a b c ->
+    -- very crudely approximate when overflow will occur; bail we think it
+    -- will
+    (([a,b,c] :: [SrcSpan]) & allOf (each . (srcSpanAbs <> srcSpanLen))
+                                    (< (maxBound @Int `div` 3)))
+    ==> (a <> b) <> c === a <> (b <> c :: SrcSpan)
+
+prop_SrcSpan_mul_commutative :: Property
+prop_SrcSpan_mul_commutative = property $ \a b ->
+    a <> b === (b <> a :: SrcSpan)
+
+prop_SrcSpan_mul_square_eq :: Property
+prop_SrcSpan_mul_square_eq = property $ \a ->
+    a <> a === (a :: SrcSpan)
+
+instance Arbitrary SrcSpan where
+    arbitrary = do
+        l <- chooseInt (1, maxBound)
+        c <- chooseInt (1, maxBound)
+        a <- chooseInt (0, maxBound)
+            `suchThat` (\n -> n >= pred l + pred c)
+        s <- chooseInt (0, maxBound)
+        pure $ SrcSpan l c a s
+
+    shrink (SrcSpan l c a s) =
+        [ SrcSpan l' c' a' s'
+        | (l',c',a',s') <- shrinkParts
+        , l' >= 1
+        , c' >= 1
+        , a' >= pred l' + pred c'
+        ]
+      where
+        -- shfl as = unsafePerformIO (generate $ shuffle as)
+        shrinkParts = 
+            [ (l',c',a',s')
+            | l' <- shrinkIntegral l
+            | c' <- shrinkIntegral c
+            | a' <- shrinkIntegral a
+            | s' <- shrinkIntegral s
+            ]
+
Author	SHA1	Message	Date
crumbtoo	c026f6f8f9	system F	2024-02-29 09:52:08 -07:00
crumbtoo	16f7f51fb8	almost done	2024-02-27 14:48:02 -07:00
crumbtoo	f8201b7d61	pretty-printing	2024-02-27 07:56:25 -07:00
crumbtoo	b67fe4eb2d	terse pretty-printing	2024-02-27 06:14:02 -07:00
crumbtoo	1315ea7ea8	parse	2024-02-27 05:12:19 -07:00
crumbtoo	d60bd86842	it may not be perfection but it is progress	2024-02-26 18:18:02 -07:00
crumbtoo	c226b2da88	HasBinders Binding	2024-02-26 17:03:20 -07:00
crumbtoo	893a01a8bb	HasBinders Program	2024-02-26 16:41:54 -07:00
crumbtoo	4bbf3a3afe	fromString for Fix	2024-02-26 14:59:37 -07:00
crumbtoo	c8967572a6	Eq1	2024-02-26 14:58:17 -07:00
crumbtoo	30fe41ce97	Eq1	2024-02-26 14:57:22 -07:00
crumbtoo	8c2ea566dc	instances for Fix	2024-02-26 14:29:57 -07:00
crumbtoo	d9682561b8	instances (finally)	2024-02-26 12:23:21 -07:00
crumbtoo	4225bf8066	Bi{foldable,functor,traversable}	2024-02-26 10:41:41 -07:00
crumbtoo	15f65a79f6	instance hell	2024-02-26 10:12:33 -07:00
crumbtoo	240db0df3d	clisp->sbcl	2024-02-23 20:34:38 -07:00
crumbtoo	a582cd9fcf	stopping for a bit	2024-02-22 15:56:00 -07:00
crumbtoo	a50a4590c5	parser compiles	2024-02-22 15:08:55 -07:00
crumbtoo	d3bcbf9624	things	2024-02-22 14:05:29 -07:00
crumbtoo	fd47599b06	things	2024-02-22 14:05:24 -07:00
crumbtoo	a7dd852464	fix hardcoded builddir	2024-02-22 10:51:43 -07:00
crumbtoo	a2ad7856a6	fix default `prettyPrec` definition	2024-02-22 08:57:35 -07:00
crumbtoo	c0baf46f29	Merge branch 'no-ttg' into dev	2024-02-22 08:15:03 -07:00
crumbtoo	09f393af89	good enough	2024-02-20 14:34:42 -07:00
crumbtoo	e63e34a3d8	ohhhhhhhh	2024-02-20 11:52:44 -07:00
crumbtoo	13e8701b8a	why did i do this to myself	2024-02-20 11:26:35 -07:00
crumbtoo	66c3d878c2	i want to fucking die	2024-02-20 11:10:33 -07:00
crumbtoo	820bd7cdbc	backstage	2024-02-17 01:56:29 -07:00
crumbtoo	9297d815d6	something	2024-02-16 18:23:02 -07:00
crumbtoo	910cf66468	HasLocation HasLocation	2024-02-16 18:03:49 -07:00
crumbtoo	da81a5a98e	SrcSpan	2024-02-16 16:14:38 -07:00
crumbtoo	caeec216b5	no-ttg	2024-02-16 15:11:08 -07:00
crumbtoo	e9cab1ddaf	no-ttg	2024-02-15 18:27:04 -07:00