seems to work

i'm honestly rather disappointed in myself for not implementing a comonadic algo J.
cross my heart i'll come back to this and return stronger!
in the mean time, i really need to get this thing into a presentable state...

Makefile_happysrcs

@@ -9,12 +9,16 @@ CABAL_BUILD = $(shell ./find-build.cl)
 
 all: parsers lexers
 
-parsers: $(CABAL_BUILD)/Rlp/Parse.hs $(CABAL_BUILD)/Core/Parse.hs
+parsers: $(CABAL_BUILD)/Rlp/Parse.hs $(CABAL_BUILD)/Core/Parse.hs \
+		$(CABAL_BUILD)/Rlp/AltParse.hs
 lexers: $(CABAL_BUILD)/Rlp/Lex.hs $(CABAL_BUILD)/Core/Lex.hs
 
 $(CABAL_BUILD)/Rlp/Parse.hs: $(SRC)/Rlp/Parse.y
 	$(HAPPY) $(HAPPY_OPTS) $< -o $@
 
+$(CABAL_BUILD)/Rlp/AltParse.hs: $(SRC)/Rlp/AltParse.y
+	$(HAPPY) $(HAPPY_OPTS) $< -o $@
+
 $(CABAL_BUILD)/Rlp/Lex.hs: $(SRC)/Rlp/Lex.x
 	$(ALEX) $(ALEX_OPTS) $< -o $@
 

rlp.cabal

@@ -32,8 +32,13 @@ library
                     , Core.HindleyMilner
                     , Control.Monad.Errorful
                     , Rlp.Syntax
+                    , Rlp.AltSyntax
+                    , Rlp.AltParse
+                    , Rlp.HindleyMilner
+                    , Rlp.HindleyMilner.Types
                     , Rlp.Syntax.Backstage
                     , Rlp.Syntax.Types
+                    , Rlp.Syntax.Good
                     -- , Rlp.Parse.Decls
                     , Rlp.Parse
                     , Rlp.Parse.Associate
@@ -66,6 +71,7 @@ library
                     , data-default-class >= 0.1.2 && < 0.2
                     , hashable >= 1.4.3 && < 1.5
                     , mtl >= 2.3.1 && < 2.4
+                    , transformers
                     , text >= 2.0.2 && < 2.2
                     , unordered-containers >= 0.2.20 && < 0.3
                     , recursion-schemes >= 5.2.2 && < 5.3

src/Compiler/JustRun.hs

@@ -10,6 +10,7 @@ types such as @RLPC@ or @Text@.
 module Compiler.JustRun
     ( justLexCore
     , justParseCore
+    , justParseRlp
     , justTypeCheckCore
     , justHdbg
     , makeItPretty, makeItPretty'
@@ -29,15 +30,18 @@ import Data.Text                        qualified as T
 import Data.Function                    ((&))
 import System.IO
 import GM
-import Rlp.Parse
 import Rlp2Core
 import Data.Pretty
+
+import Rlp.AltParse
+import Rlp.AltSyntax                    qualified as Rlp
 ----------------------------------------------------------------------------------
 
 justHdbg :: String -> IO GmState
-justHdbg s = do
+justHdbg = undefined
-    p <- evalRLPCIO def (parseRlpProgR >=> desugarRlpProgR $ T.pack s)
+-- justHdbg s = do
-    withFile "/tmp/t.log" WriteMode $ hdbgProg p
+--     p <- evalRLPCIO def (parseRlpProgR >=> desugarRlpProgR $ T.pack s)
+--     withFile "/tmp/t.log" WriteMode $ hdbgProg p
 
 justLexCore :: String -> Either [MsgEnvelope RlpcError] [CoreToken]
 justLexCore s = lexCoreR (T.pack s)
@@ -49,6 +53,13 @@ justParseCore s = parse (T.pack s)
                 & rlpcToEither
     where parse = lexCoreR @Identity >=> parseCoreProgR
 
+justParseRlp :: String
+             -> Either [MsgEnvelope RlpcError]
+                       (Rlp.Program Name (Rlp.RlpExpr Name))
+justParseRlp s = parse (T.pack s)
+               & rlpcToEither
+    where parse = parseRlpProgR @Identity
+
 justTypeCheckCore :: String -> Either [MsgEnvelope RlpcError] Program'
 justTypeCheckCore s = typechk (T.pack s)
                     & rlpcToEither

src/Compiler/Types.hs

@@ -46,8 +46,6 @@ import Data.Function                (on)
 data Located a = Located SrcSpan a
     deriving (Show, Lift, Functor)
 
-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
 
@@ -56,10 +54,10 @@ pattern a :<$ b = a Trans.Cofree.:< b
 
 infixl 5 <~>
 
--- (~>) :: (CanGet k, CanSet k', HasLocation k a, HasLocation k' b)
+(~>) :: (CanGet k, CanSet k', HasLocation k a, HasLocation k' b)
---      => a -> b -> b
+     => a -> b -> b
--- a ~> b = 
+a ~> b = b & fromSet getSetLocation .~ (a ^. fromGet getSetLocation)
-(~>) = undefined
+-- (~>) = undefined
 
 infixl 4 ~>
 
@@ -97,15 +95,15 @@ data SrcSpan = SrcSpan
     !Int -- ^ Length
     deriving (Show, Eq, Lift)
 
-tupling :: Iso' SrcSpan (Int, Int, Int, Int)
+_SrcSpan :: Iso' SrcSpan (Int, Int, Int, Int)
-tupling = iso (\ (SrcSpan a b c d) -> (a,b,c,d))
+_SrcSpan = 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
+srcSpanLine = _SrcSpan . _1
-srcSpanColumn = tupling . _2
+srcSpanColumn = _SrcSpan . _2
-srcSpanAbs = tupling . _3
+srcSpanAbs = _SrcSpan . _3
-srcSpanLen = tupling . _4
+srcSpanLen = _SrcSpan . _4
 
 -- | debug tool
 nolo :: a -> Located a
@@ -228,3 +226,4 @@ lochead afs (Located ss fss) = ss :< unwrap (lochead afs $ Located ss fss)
 --------------------------------------------------------------------------------
 
 makePrisms ''Located
+

src/Control/Monad/Errorful.hs

@@ -14,7 +14,9 @@ module Control.Monad.Errorful
     where
 ----------------------------------------------------------------------------------
 import Control.Monad.State.Strict
+import Control.Monad.Writer
 import Control.Monad.Reader
+import Control.Monad.Accum
 import Control.Monad.Trans
 import Data.Functor.Identity
 import Data.Coerce
@@ -85,3 +87,16 @@ instance (Monad m, MonadErrorful e m) => MonadErrorful e (ReaderT r m) where
     addWound = lift . addWound
     addFatal = lift . addFatal
 
+instance (Monad m, MonadState s m) => MonadState s (ErrorfulT e m) where
+    state = lift . state
+
+instance (Monoid w, Monad m, MonadWriter w m) => MonadWriter w (ErrorfulT e m) where
+    tell = lift . tell
+    listen (ErrorfulT m) = ErrorfulT $ listen m <&> \ ((ma,es),w) ->
+        ((,w) <$> ma, es)
+    pass (ErrorfulT m) = undefined
+
+instance (Monoid w, Monad m, MonadAccum w m)
+      => MonadAccum w (ErrorfulT e m) where
+    accum = lift . accum
+

src/Core/Syntax.hs

@@ -33,10 +33,11 @@ module Core.Syntax
     , Pretty(pretty), WithTerseBinds(..)
 
     -- * Optics
-    , programScDefs, programTypeSigs, programDataTags
+    , HasArrowSyntax(..)
-    , formalising
+    , programScDefs, programTypeSigs, programDataTags, programTyCons
+    , formalising, lambdaLifting
     , HasRHS(_rhs), HasLHS(_lhs)
-    , _BindingF, _MkVar
+    , _BindingF, _MkVar, _ScDef
     -- ** Classy optics
     , HasBinders(..), HasArrowStops(..), HasApplicants1(..), HasApplicants(..)
     )
@@ -50,6 +51,7 @@ import Data.String
 import Data.HashMap.Strict          (HashMap)
 import Data.HashMap.Strict          qualified as H
 import Data.Hashable
+import Data.Hashable.Lifted
 import Data.Foldable                (traverse_)
 import Data.Functor
 import Data.Monoid
@@ -57,7 +59,7 @@ import Data.Functor.Classes
 import Data.Text                    qualified as T
 import Data.Char
 import Data.These
-import GHC.Generics                 (Generic, Generically(..))
+import GHC.Generics                 (Generic, Generic1, Generically(..))
 import Text.Show.Deriving
 import Data.Eq.Deriving
 import Data.Kind                    qualified
@@ -143,9 +145,22 @@ pattern Lit t = Fix (LitF t)
 pattern TyInt :: Type
 pattern TyInt = TyCon "Int#"
 
+class HasArrowSyntax s a b | s -> a b where
+    _arrowSyntax :: Prism' s (a, b)
+
+instance HasArrowSyntax Type Type Type where
+    _arrowSyntax = prism make unmake where
+        make (s,t) = TyFun `TyApp` s `TyApp` t
+
+        unmake (TyFun `TyApp` s `TyApp` t) = Right (s,t)
+        unmake s                           = Left s
+
 infixr 1 :->
-pattern (:->) :: Type -> Type -> Type
+pattern (:->) :: HasArrowSyntax s a b
-pattern a :-> b = TyApp (TyApp TyFun a) b
+              => a -> b -> s
+-- pattern (:->) :: Type -> Type -> Type
+pattern a :-> b <- (preview _arrowSyntax -> Just (a, b))
+    where a :-> b = _arrowSyntax # (a, b)
 
 data BindingF b a = BindingF b (ExprF b a)
     deriving (Functor, Foldable, Traversable)
@@ -216,6 +231,8 @@ data Program b = Program
     , _programTypeSigs :: HashMap b Type
     , _programDataTags :: HashMap Name (Tag, Int)
     -- ^ map constructors to their tag and arity
+    , _programTyCons   :: HashMap Name Kind
+    -- ^ map type constructors to their kind
     }
     deriving (Generic)
     deriving (Semigroup, Monoid)
@@ -242,6 +259,14 @@ type ScDef' = ScDef Name
 -- instance IsString (Expr b) where
 --     fromString = Var . fromString
 
+lambdaLifting :: Iso (ScDef b) (ScDef b') (b, Expr b) (b', Expr b')
+lambdaLifting = iso sa bt where
+    sa (ScDef n as e) = (n, e') where
+        e' = Lam as e
+
+    bt (n, Lam as e) = ScDef n as e
+    bt (n, e)        = ScDef n [] e
+
 ----------------------------------------------------------------------------------
 
 class HasRHS s t a b | s -> a, t -> b, s b -> t, t a -> s where
@@ -410,36 +435,56 @@ instance (Pretty b) => Pretty (ScDef b) where
             as = sc & hsepOf (_lhs . _2 . each . to ttext)
             e = pretty $ sc ^. _rhs
 
-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 = prettyPrec1
-    prettyPrec _ (ConF t a) = "Pack{" <> (ttext t <+> ttext a) <> "}"
+
-    prettyPrec p (LamF bs e) = maybeParens (p>0) $
+    -- prettyPrec _ (VarF n) = ttext n
-        hsep ["λ", hsep (prettyPrec appPrec1 <$> bs), "->", pretty e]
+    -- prettyPrec _ (ConF t a) = "Pack{" <> (ttext t <+> ttext a) <> "}"
-    prettyPrec p (LetF r bs e) = maybeParens (p>0)
+    -- prettyPrec p (LamF bs e) = maybeParens (p>0) $
-                               $ hsep [pretty r, explicitLayout bs]
+    --     hsep ["λ", hsep (prettyPrec appPrec1 <$> bs), "->", pretty e]
-                             $+$ hsep ["in", pretty e]
+    -- prettyPrec p (LetF r bs e) = maybeParens (p>0)
-    prettyPrec p (AppF f x) = maybeParens (p>appPrec) $
+    --                            $ hsep [pretty r, explicitLayout bs]
-        prettyPrec appPrec f <+> prettyPrec appPrec1 x
+    --                          $+$ hsep ["in", pretty e]
-    prettyPrec p (LitF l) = prettyPrec p l
+    -- prettyPrec p (AppF f x) = maybeParens (p>appPrec) $
-    prettyPrec p (CaseF e as) = maybeParens (p>0) $
+    --     prettyPrec appPrec f <+> prettyPrec appPrec1 x
-        "case" <+> pretty e <+> "of"
+    -- prettyPrec p (LitF l) = prettyPrec p l
-        $+$ nest 2 (explicitLayout as)
+    -- prettyPrec p (CaseF e as) = maybeParens (p>0) $
-    prettyPrec p (TypeF t) = "@" <> prettyPrec appPrec1 t
+    --     "case" <+> pretty e <+> "of"
+    --     $+$ nest 2 (explicitLayout as)
+    -- prettyPrec p (TypeF t) = "@" <> prettyPrec appPrec1 t
+
+instance (Pretty b) => Pretty1 (ExprF b) where
+    liftPrettyPrec pr _ (VarF n) = ttext n
+    liftPrettyPrec pr _ (ConF t a) = "Pack{" <> (ttext t <+> ttext a) <> "}"
+    liftPrettyPrec pr p (LamF bs e) = maybeParens (p>0) $
+        hsep ["λ", hsep (prettyPrec appPrec1 <$> bs), "->", pr 0 e]
+    liftPrettyPrec pr p (LetF r bs e) = maybeParens (p>0)
+                               $ hsep [pretty r, bs']
+                             $+$ hsep ["in", pr 0 e]
+        where bs' = liftExplicitLayout (liftPrettyPrec pr 0) bs
+    liftPrettyPrec pr p (AppF f x) = maybeParens (p>appPrec) $
+        pr appPrec f <+> pr appPrec1 x
+    liftPrettyPrec pr p (LitF l) = prettyPrec p l
+    liftPrettyPrec pr p (CaseF e as) = maybeParens (p>0) $
+            "case" <+> pr 0 e <+> "of"
+            $+$ nest 2 as'
+        where as' = liftExplicitLayout (liftPrettyPrec pr 0) as
+    liftPrettyPrec pr p (TypeF t) = "@" <> prettyPrec appPrec1 t
 
 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) =
+    prettyPrec = prettyPrec1
-        hsep [pretty c, hsep (pretty <$> as), "->", pretty e]
+
+instance (Pretty b) => Pretty1 (AlterF b) where
+    liftPrettyPrec pr _ (AlterF c as e) =
+        hsep [pretty c, hsep (pretty <$> as), "->", liftPrettyPrec pr 0 e]
 
 instance Pretty AltCon where
     pretty (AltData n) = ttext n
@@ -451,7 +496,15 @@ instance Pretty Lit where
     pretty (IntL n) = ttext n
 
 instance (Pretty b, Pretty a) => Pretty (BindingF b a) where
-    pretty (BindingF k v) = hsep [pretty k, "=", pretty v]
+    prettyPrec = prettyPrec1
+
+instance Pretty b => Pretty1 (BindingF b) where
+    liftPrettyPrec pr _ (BindingF k v) = hsep [pretty k, "=", liftPrettyPrec pr 0 v]
+
+liftExplicitLayout :: (a -> Doc) -> [a] -> Doc
+liftExplicitLayout pr as = vcat inner <+> "}" where
+    inner = zipWith (<+>) delims (pr <$> as)
+    delims = "{" : repeat ";"
 
 explicitLayout :: (Pretty a) => [a] -> Doc
 explicitLayout as = vcat inner <+> "}" where
@@ -559,15 +612,24 @@ deriveBifunctor ''ExprF
 deriveBifoldable ''ExprF
 deriveBitraversable ''ExprF
 
+instance Lift b => Lift1 (BindingF b) where
+    liftLift lf (BindingF k v) = liftCon2 'BindingF (lift k) (liftLift lf v)
+
+instance Lift b => Lift1 (AlterF b) where
+    liftLift lf (AlterF con bs e) =
+        liftCon3 'AlterF (lift con) (lift1 bs) (liftLift lf e)
+
 instance Lift b => Lift1 (ExprF b) where
-    lift1 (VarF k)      = liftCon 'VarF (lift k)
+    liftLift lf (VarF k)      = liftCon 'VarF (lift k)
-    lift1 (AppF f x)    = liftCon2 'AppF (lift f) (lift x)
+    liftLift lf (AppF f x)    = liftCon2 'AppF (lf f) (lf x)
-    lift1 (LamF b e)    = liftCon2 'LamF (lift b) (lift e)
+    liftLift lf (LamF b e)    = liftCon2 'LamF (lift b) (lf e)
-    lift1 (LetF r bs e) = liftCon3 'LetF (lift r) (lift bs) (lift e)
+    liftLift lf (LetF r bs e) = liftCon3 'LetF (lift r) bs' (lf e)
-    lift1 (CaseF e as)  = liftCon2 'CaseF (lift e) (lift as)
+        where bs' = liftLift (liftLift lf) bs
-    lift1 (TypeF t)     = liftCon 'TypeF (lift t)
+    liftLift lf (CaseF e as)  = liftCon2 'CaseF (lf e) as'
-    lift1 (LitF l)      = liftCon 'LitF (lift l)
+        where as' = liftLift (liftLift lf) as
-    lift1 (ConF t a)    = liftCon2 'ConF (lift t) (lift a)
+    liftLift lf (TypeF t)     = liftCon 'TypeF (lift t)
+    liftLift lf (LitF l)      = liftCon 'LitF (lift l)
+    liftLift lf (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)
@@ -621,6 +683,7 @@ instance (Hashable b, Hashable b')
         <$> traverse (binders k) (_programScDefs p)
         <*> (getAp . ifoldMap toSingleton $ _programTypeSigs p)
         <*> pure (_programDataTags p)
+        <*> pure (_programTyCons p)
       where
         toSingleton :: b -> Type -> Ap f (HashMap b' Type)
         toSingleton b t = Ap $ (`H.singleton` t) <$> k b
@@ -692,4 +755,28 @@ deriving instance (Eq b, Eq a) => Eq (ExprF b a)
 
 makePrisms ''BindingF
 makePrisms ''Var
+makePrisms ''ScDef
+
+deriving instance Generic (ExprF b a)
+deriving instance Generic1 (ExprF b)
+deriving instance Generic1 (AlterF b)
+deriving instance Generic1 (BindingF b)
+deriving instance Generic (AlterF b a)
+deriving instance Generic (BindingF b a)
+deriving instance Generic AltCon
+deriving instance Generic Lit
+deriving instance Generic Rec
+deriving instance Generic Type
+
+instance Hashable Lit
+instance Hashable AltCon
+instance Hashable Rec
+instance Hashable Type
+instance (Hashable b, Hashable a) => Hashable (BindingF b a)
+instance (Hashable b, Hashable a) => Hashable (AlterF b a)
+instance (Hashable b, Hashable a) => Hashable (ExprF b a)
+
+instance Hashable b => Hashable1 (AlterF b)
+instance Hashable b => Hashable1 (BindingF b)
+instance Hashable b => Hashable1 (ExprF b)
 

src/Core/SystemF.hs

@@ -45,8 +45,36 @@ makeLenses ''Gamma
 lintCoreProgR :: (Monad m) => Program Var -> RLPCT m (Program Name)
 lintCoreProgR = undefined
 
-lint :: Program Var -> Program Name
+lintDontCheck :: Program Var -> Program Name
-lint = undefined
+lintDontCheck = binders %~ view (_MkVar . _1)
+
+lint :: Program Var -> SysF (Program Name)
+lint p = do
+    scs <- traverse (lintScDef g0) $ p ^. programScDefs
+    pure $ lintDontCheck p & programScDefs .~ scs
+  where
+    g0 = mempty & gammaVars .~ typeSigs
+                & gammaTyCons .~ p ^. programTyCons
+    -- 'p' stores the type signatures as 'HashMap Var Type',
+    -- while our typechecking context demands a 'HashMap Name Type'.
+    -- This conversion is perfectly safe, as the 'Hashable' instance for
+    -- 'Var' hashes exactly the internal 'Name'. i.e.
+    -- `hash (MkVar n t) = hash n`.
+    typeSigs = p ^. programTypeSigs
+             & H.mapKeys (view $ _MkVar . _1)
+
+lintScDef :: Gamma -> ScDef Var -> SysF (ScDef Name)
+lintScDef g = traverseOf lambdaLifting $ \ (MkVar n t, e) -> do
+    e'@(t' :< _) <- lintE g e
+    assertUnify t t'
+    let e'' = stripVars . stripTypes $ e'
+    pure (n, e'')
+
+stripTypes :: ET -> Expr Var
+stripTypes (_ :< as) = Fix (stripTypes <$> as)
+
+stripVars :: Expr Var -> Expr Name
+stripVars = binders %~ view (_MkVar . _1)
 
 type ET = Cofree (ExprF Var) Type
 
@@ -150,6 +178,11 @@ lintE g = \case
                 | t == t'   = Right ()
                 | otherwise = Left (SystemFErrorCouldNotMatch t t')
 
+assertUnify :: Type -> Type -> SysF ()
+assertUnify t t'
+    | t == t'   = pure ()
+    | otherwise = Left (SystemFErrorCouldNotMatch t t')
+
 allUnify :: [Type] -> Maybe SystemFError
 allUnify [] = Nothing
 allUnify [t] = Nothing

src/Data/Pretty.hs

@@ -1,13 +1,13 @@
-{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
 module Data.Pretty
-    ( Pretty(..)
+    ( Pretty(..), Pretty1(..)
+    , prettyPrec1
     , rpretty
     , ttext
+    , Showing(..)
     -- * Pretty-printing lens combinators
-    , hsepOf, vsepOf
+    , hsepOf, vsepOf, vcatOf, vlinesOf, vsepTerm
-    , vcatOf
+    , vsep
-    , vlinesOf
-    , vsepTerm
     , module Text.PrettyPrint
     , maybeParens
     , appPrec
@@ -20,12 +20,14 @@ import Text.PrettyPrint.HughesPJ    hiding ((<>))
 import Text.Printf
 import Data.String                  (IsString(..))
 import Data.Text.Lens               hiding ((:<))
-import Data.Monoid
+import Data.Monoid                  hiding (Sum)
 import Control.Lens
 
 -- instances
 import Control.Comonad.Cofree
 import Data.Text                    qualified as T
+import Data.Functor.Sum
+import Data.Fix                     (Fix(..))
 ----------------------------------------------------------------------------------
 
 class Pretty a where
@@ -53,7 +55,24 @@ 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
+    liftPrettyPrec :: (Int -> a -> Doc) -> Int -> f a -> Doc
+
+prettyPrec1 :: (Pretty1 f, Pretty a) => Int -> f a -> Doc
+prettyPrec1 = liftPrettyPrec prettyPrec
+
+instance (Pretty1 f, Pretty1 g, Pretty a) => Pretty (Sum f g a) where
+    prettyPrec p (InL fa) = prettyPrec1 p fa
+    prettyPrec p (InR ga) = prettyPrec1 p ga
+
+instance (Pretty1 f, Pretty1 g) => Pretty1 (Sum f g) where
+    liftPrettyPrec pr p (InL fa) = liftPrettyPrec pr p fa
+    liftPrettyPrec pr p (InR ga) = liftPrettyPrec pr p ga
+
+instance (Pretty (f (Fix f))) => Pretty (Fix f) where
+    prettyPrec d (Fix f) = prettyPrec d f
+
+-- instance (Pretty1 f) => Pretty (Fix f) where
+--     prettyPrec d (Fix f) = prettyPrec1 d f
 
 --------------------------------------------------------------------------------
 
@@ -76,6 +95,9 @@ vlinesOf l = foldrOf l (\a b -> a $+$ "" $+$ b) mempty
 vsepTerm :: Doc -> Doc -> Doc -> Doc
 vsepTerm term a b = (a <> term) $+$ b
 
+vsep :: [Doc] -> Doc
+vsep = foldr ($+$) mempty
+
 --------------------------------------------------------------------------------
 
 appPrec, appPrec1 :: Int

src/Misc/Lift1.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE TemplateHaskell #-}
 module Misc.Lift1
-    ( Lift1(..)
+    ( Lift1(..), lift1
     , liftCon, liftCon2, liftCon3
     , Lift(..)
     )
@@ -13,11 +13,17 @@ import Language.Haskell.TH.Quote
 import Data.Kind                        qualified
 import GHC.Generics
 
+-- instances
 import Data.Fix
+import Data.Functor.Sum
 --------------------------------------------------------------------------------
 
 class Lift1 (f :: Data.Kind.Type -> Data.Kind.Type) where
-    lift1 :: (Quote m, Lift t) => f t -> m Exp
+    -- lift1 :: (Quote m, Lift t) => f t -> m Exp
+    liftLift :: (Quote m) => (a -> m Exp) -> f a -> m Exp
+
+lift1 :: (Lift1 f, Lift a, Quote m) => f a -> m Exp
+lift1 = liftLift lift
 
 liftCon :: Quote m => TH.Name -> m Exp -> m Exp
 liftCon n = fmap (AppE (ConE n))
@@ -38,4 +44,11 @@ liftCon3 n a b c = do
 instance Lift1 f => Lift (Fix f) where
     lift (Fix f) = AppE (ConE 'Fix) <$> lift1 f
 
+instance Lift1 [] where
+    liftLift lf []     = pure $ ConE '[]
+    liftLift lf (a:as) = liftCon2 '(:) (lf a) (liftLift lf as)
+
+instance (Lift1 f, Lift1 g) => Lift1 (Sum f g) where
+    liftLift lf (InL fa) = liftCon 'InL $ liftLift lf fa
+    liftLift lf (InR ga) = liftCon 'InR $ liftLift lf ga
 

src/Rlp/AltParse.y

@@ -0,0 +1,232 @@
+{
+module Rlp.AltParse
+    ( parseRlpProg
+    , parseRlpProgR
+    , parseRlpExprR
+    , runP'
+    )
+    where
+import Data.List.Extra
+import Data.Text                (Text)
+
+import Control.Comonad
+import Control.Comonad.Cofree
+import Control.Lens             hiding (snoc)
+
+import Compiler.RlpcError
+import Compiler.RLPC
+import Control.Monad.Errorful
+
+import Rlp.Lex
+import Rlp.AltSyntax
+import Rlp.Parse.Types          hiding (PsName)
+import Core.Syntax              qualified as Core
+}
+
+%name parseRlpProg StandaloneProgram
+%name parseRlpExpr StandaloneExpr
+
+%monad { P }
+%lexer { lexCont } { Located _ TokenEOF }
+%error { parseError }
+%errorhandlertype explist
+%tokentype { Located RlpToken }
+
+%token
+    varname         { Located _ (TokenVarName _) }
+    conname         { Located _ (TokenConName _) }
+    consym          { Located _ (TokenConSym _) }
+    varsym          { Located _ (TokenVarSym _) }
+    data            { Located _ TokenData }
+    case            { Located _ TokenCase }
+    of              { Located _ TokenOf }
+    litint          { Located _ (TokenLitInt _) }
+    '='             { Located _ TokenEquals }
+    '|'             { Located _ TokenPipe }
+    '::'            { Located _ TokenHasType }
+    ';'             { Located _ TokenSemicolon }
+    'λ'             { Located _ TokenLambda }
+    '('             { Located _ TokenLParen }
+    ')'             { Located _ TokenRParen }
+    '->'            { Located _ TokenArrow }
+    vsemi           { Located _ TokenSemicolonV }
+    '{'             { Located _ TokenLBrace }
+    '}'             { Located _ TokenRBrace }
+    vlbrace         { Located _ TokenLBraceV }
+    vrbrace         { Located _ TokenRBraceV }
+    infixl          { Located _ TokenInfixL }
+    infixr          { Located _ TokenInfixR }
+    infix           { Located _ TokenInfix }
+    let             { Located _ TokenLet }
+    letrec          { Located _ TokenLetrec }
+    in              { Located _ TokenIn }
+
+%nonassoc '='
+%right '->'
+%right in
+
+%%
+
+StandaloneProgram :: { Program Name (RlpExpr PsName) }
+                  : layout0(Decl)       { Program $1 }
+
+
+StandaloneExpr :: { RlpExpr PsName }
+               : VL Expr VR             { $2 }
+
+VL  :: { () }
+VL  : vlbrace       { () }
+
+VR  :: { () }
+VR  : vrbrace       { () }
+    | error         { () }
+
+VS                  :: { () }
+VS                  : ';'                   { () }
+                    | vsemi                 { () }
+
+Decl                :: { Decl PsName (RlpExpr PsName) }
+                    : FunD                  { $1 }
+                    | DataD                 { $1 }
+                    | TySigD                { $1 }
+
+TySigD              :: { Decl PsName (RlpExpr PsName) }
+                    : Var '::' Type         { TySigD $1 $3 }
+
+DataD               :: { Decl PsName (RlpExpr PsName) }
+                    : data Con TyVars               { DataD $2 $3 [] }
+                    | data Con TyVars '=' DataCons  { DataD $2 $3 $5 }
+
+DataCons            :: { [DataCon PsName] }
+                    : DataCon '|' DataCons  { $1 : $3 }
+                    | DataCon               { [$1] }
+
+DataCon             :: { DataCon PsName }
+                    : Con list0(Type1)      { DataCon $1 $2 }
+
+Type1               :: { Type PsName }
+                    : varname               { VarT $ extractVarName $1 }
+                    | Con                   { ConT $1 }
+                    | '(' Type ')'          { $2 }
+
+Type                :: { Type PsName }
+                    : Type '->' Type        { $1 :-> $3 }
+                    | AppT                  { $1 }
+
+AppT                :: { Type PsName }
+                    : Type1                 { $1 }
+                    | AppT Type1            { AppT $1 $2 }
+
+TyVars              :: { [PsName] }
+                    : list0(varname)     { $1 <&> view ( to extract
+                                                       . singular _TokenVarName ) }
+
+FunD                :: { Decl PsName (RlpExpr PsName) }
+                    : Var Pat1s '=' Expr    { FunD $1 $2 $4 }
+
+Expr                :: { RlpExpr PsName }
+                    : AppE                  { $1 }
+                    | LetE                  { $1 }
+                    | CaseE                 { $1 }
+                    | LamE                  { $1 }
+
+LamE                :: { RlpExpr PsName }
+                    : 'λ' list0(varname) '->' Expr { Finl $ Core.LamF (fmap extractName $2) $4 }
+
+CaseE               :: { RlpExpr PsName }
+                    : case Expr of CaseAlts { Finr $ CaseEF $2 $4 }
+
+CaseAlts            :: { [Alter PsName (RlpExpr PsName)] }
+                    : layout1(CaseAlt)      { $1 }
+
+CaseAlt             :: { Alter PsName (RlpExpr PsName) }
+                    : Pat '->' Expr    { Alter $1 $3 }
+
+LetE                :: { RlpExpr PsName }
+                    : let layout1(Binding) in Expr
+                        { Finr $ LetEF Core.NonRec $2 $4 }
+
+Binding             :: { Binding PsName (RlpExpr PsName) }
+                    : Pat '=' Expr          { VarB $1 $3 }
+
+Expr1               :: { RlpExpr PsName }
+                    : VarE                  { $1 }
+                    | litint                { $1 ^. to extract
+                                                  . singular _TokenLitInt
+                                                  . to (Finl . Core.LitF . Core.IntL) }
+                    | '(' Expr ')'          { $2 }
+
+AppE                :: { RlpExpr PsName }
+                    : AppE Expr1            { Finl $ Core.AppF $1 $2 }
+                    | Expr1                 { $1 }
+
+VarE                :: { RlpExpr PsName }
+                    : Var                   { Finl $ Core.VarF $1 }
+
+Pat1s               :: { [Pat PsName] }
+                    : list0(Pat1)           { $1 }
+
+Pat1                :: { Pat PsName }
+                    : Var                   { VarP $1 }
+                    | Con                   { ConP $1 }
+                    | '(' Pat ')'           { $2 }
+
+Pat                 :: { Pat PsName }
+                    : AppP                  { $1 }
+
+AppP                :: { Pat PsName }
+                    : Pat1                  { $1 }
+                    | AppP Pat1             { $1 `AppP` $2 }
+
+Con                 :: { PsName }
+                    : conname               { $1 ^. to extract
+                                                  . singular _TokenConName }
+                    | '(' consym ')'        { $1 ^. to extract
+                                                  . singular _TokenConSym }
+
+Var                 :: { PsName }
+                    : varname               { $1 ^. to extract
+                                                  . singular _TokenVarName }
+                    | '(' varsym ')'        { $2 ^. to extract
+                                                  . singular _TokenVarSym }
+
+-- list0(p : α) : [α]
+list0(p) : {- epsilon -}            { [] }
+         | list0(p) p             { $1 `snoc` $2 }
+
+-- layout0(p : β) :: [β]
+layout0(p)  : '{' layout_list0(';',p) '}'   { $2 }
+            | VL  layout_list0(VS,p)  VR    { $2 }
+
+-- layout_list0(sep : α, p : β) :: [β]
+layout_list0(sep,p) : p                          { [$1] }
+                    | layout_list1(sep,p) sep p  { $1 `snoc` $3 }
+                    | {- epsilon -}              { [] }
+
+-- layout1(p : β) :: [β]
+layout1(p)  : '{' layout_list1(';',p) '}'   { $2 }
+            | VL  layout_list1(VS,p) VR     { $2 }
+
+-- layout_list1(sep : α, p : β) :: [β]
+layout_list1(sep,p) : p                          { [$1] }
+                    | layout_list1(sep,p) sep p  { $1 `snoc` $3 }
+
+{
+
+extractVarName = view $ to extract . singular _TokenVarName
+
+parseRlpProgR :: (Monad m) => Text -> RLPCT m (Program Name (RlpExpr PsName))
+parseRlpProgR s = liftErrorful $ errorful (ma,es)
+    where
+        (_,es,ma) = runP' parseRlpProg s
+
+parseRlpExprR :: (Monad m) => Text -> RLPCT m (RlpExpr PsName)
+parseRlpExprR s = liftErrorful $ errorful (ma,es)
+    where
+        (_,es,ma) = runP' parseRlpExpr s
+
+parseError = error "explode"
+
+extractName = view $ to extract . singular _TokenVarName
+
+}

src/Rlp/AltSyntax.hs

@@ -0,0 +1,219 @@
+{-# LANGUAGE TemplateHaskell, PatternSynonyms #-}
+module Rlp.AltSyntax
+    (
+    -- * AST
+      Program(..), Decl(..), ExprF(..), Pat(..)
+    , RlpExprF, RlpExpr, Binding(..), Alter(..)
+    , DataCon(..), Type(..)
+    , pattern IntT
+
+    , TypeF(..)
+
+    , Core.Name, PsName
+    , pattern (Core.:->)
+
+    -- * Optics
+    , programDecls
+    , _VarP, _FunB, _VarB
+
+    -- * Functor-related tools
+    , Fix(..), Cofree(..), Sum(..), pattern Finl, pattern Finr
+    )
+    where
+--------------------------------------------------------------------------------
+import Data.Functor.Sum
+import Control.Comonad.Cofree
+import Data.Fix
+import Data.Function            (fix)
+import GHC.Generics             (Generic, Generic1)
+import Data.Hashable
+import Data.Hashable.Lifted
+import GHC.Exts                 (IsString)
+import Control.Lens
+
+import Data.Functor.Foldable.TH
+import Text.Show.Deriving
+import Data.Eq.Deriving
+import Data.Text                qualified as T
+import Data.Pretty
+import Misc.Lift1
+
+import Compiler.Types
+import Core.Syntax              qualified as Core
+--------------------------------------------------------------------------------
+
+type PsName = T.Text
+
+newtype Program b a = Program [Decl b a]
+    deriving Show
+
+programDecls :: Lens' (Program b a) [Decl b a]
+programDecls = lens (\ (Program ds) -> ds) (const Program)
+
+data Decl b a = FunD b [Pat b] a
+              | DataD b [b] [DataCon b]
+              | TySigD b (Type b)
+              deriving Show
+
+data DataCon b = DataCon b [Type b]
+    deriving (Show, Generic)
+
+data Type b = VarT b
+            | ConT b
+            | AppT (Type b) (Type b)
+            | FunT
+            | ForallT b (Type b)
+            deriving (Show, Eq, Generic, Functor, Foldable, Traversable)
+
+instance (Hashable b) => Hashable (Type b)
+
+pattern IntT :: (IsString b, Eq b) => Type b
+pattern IntT = ConT "Int#"
+
+instance Core.HasArrowSyntax (Type b) (Type b) (Type b) where
+    _arrowSyntax = prism make unmake where
+        make (s,t) = FunT `AppT` s `AppT` t
+
+        unmake (FunT `AppT` s `AppT` t) = Right (s,t)
+        unmake s                        = Left s
+
+data ExprF b a = InfixEF b a a
+               | LetEF Core.Rec [Binding b a] a
+               | CaseEF a [Alter b a]
+               deriving (Functor, Foldable, Traversable)
+               deriving (Eq, Generic, Generic1)
+
+data Alter b a = Alter (Pat b) a
+               deriving (Show, Functor, Foldable, Traversable)
+               deriving (Eq, Generic, Generic1)
+
+data Binding b a = FunB b [Pat b] a
+                 | VarB (Pat b) a
+                 deriving (Show, Functor, Foldable, Traversable)
+                 deriving (Eq, Generic, Generic1)
+
+-- type Expr b = Cofree (ExprF b)
+
+type RlpExprF b = Sum (Core.ExprF b) (ExprF b)
+
+type RlpExpr b = Fix (RlpExprF b)
+
+data Pat b = VarP b
+           | ConP b
+           | AppP (Pat b) (Pat b)
+           deriving (Eq, Show, Generic)
+
+deriveShow1 ''Alter
+deriveShow1 ''Binding
+deriveShow1 ''ExprF
+deriving instance (Show b, Show a) => Show (ExprF b a)
+
+pattern Finl :: f (Fix (Sum f g)) -> Fix (Sum f g)
+pattern Finl fa = Fix (InL fa)
+
+pattern Finr :: g (Fix (Sum f g)) -> Fix (Sum f g)
+pattern Finr ga = Fix (InR ga)
+
+--------------------------------------------------------------------------------
+
+instance (Pretty b, Pretty a) => Pretty (ExprF b a) where
+    prettyPrec = prettyPrec1
+
+instance (Pretty b, Pretty a) => Pretty (Alter b a) where
+    prettyPrec = prettyPrec1
+
+instance (Pretty b) => Pretty1 (Alter b) where
+    liftPrettyPrec pr _ (Alter p e) =
+        hsep [ pretty p, "->", pr 0 e]
+
+instance Pretty b => Pretty1 (ExprF b) where
+    liftPrettyPrec pr p (InfixEF o a b) = maybeParens (p>0) $
+        pr 1 a <+> pretty o <+> pr 1 b
+    liftPrettyPrec pr p (CaseEF e as) = maybeParens (p>0) $
+        hsep [ "case", pr 0 e, "of" ]
+        $+$ nest 2 (vcat $ liftPrettyPrec pr 0 <$> as)
+
+instance (Pretty b, Pretty a) => Pretty (Decl b a) where
+    prettyPrec = prettyPrec1
+
+instance (Pretty b) => Pretty1 (Decl b) where
+    liftPrettyPrec pr _ (FunD f as e) =
+        hsep [ ttext f, hsep (prettyPrec appPrec1 <$> as)
+             , "=", pr 0 e ]
+
+    liftPrettyPrec _ _ (DataD f as []) =
+        hsep [ "data", ttext f, hsep (pretty <$> as) ]
+
+    liftPrettyPrec _ _ (DataD f as ds) =
+        hsep [ "data", ttext f, hsep (pretty <$> as), cons ]
+      where
+        cons = vcat $ zipWith (<+>) delims (pretty <$> ds)
+        delims = "=" : repeat "|"
+
+    liftPrettyPrec _ _ (TySigD n t) =
+        hsep [ ttext n, ":", pretty t ]
+
+instance (Pretty b) => Pretty (DataCon b) where
+    pretty (DataCon n as) = ttext n <+> hsep (prettyPrec appPrec1 <$> as)
+
+-- (->) is given prec `appPrec-1`
+instance (Pretty b) => Pretty (Type b) where
+    prettyPrec _ (VarT n) = ttext n
+    prettyPrec _ (ConT n) = ttext n
+    prettyPrec p (s Core.:-> t) = maybeParens (p>appPrec-1) $
+        hsep [ prettyPrec appPrec s, "->", prettyPrec (appPrec-1) t ]
+    prettyPrec p (AppT f x) = maybeParens (p>appPrec) $
+        prettyPrec appPrec f <+> prettyPrec appPrec1 x
+    prettyPrec p FunT = maybeParens (p>0) "->"
+
+instance (Pretty b) => Pretty (Pat b) where
+    prettyPrec p (VarP b) = prettyPrec p b
+    prettyPrec p (ConP b) = prettyPrec p b
+    prettyPrec p (AppP c x) = maybeParens (p>appPrec) $
+        prettyPrec appPrec c <+> prettyPrec appPrec1 x
+
+instance (Pretty a, Pretty b) => Pretty (Program b a) where
+    prettyPrec = prettyPrec1
+
+instance (Pretty b) => Pretty1 (Program b) where
+    liftPrettyPrec pr p (Program ds) = vsep $ liftPrettyPrec pr p <$> ds
+
+makePrisms ''Pat
+makePrisms ''Binding
+
+deriving instance (Lift b, Lift a) => Lift (Program b a)
+deriving instance (Lift b, Lift a) => Lift (Decl b a)
+deriving instance (Lift b) => Lift (Pat b)
+deriving instance (Lift b) => Lift (DataCon b)
+deriving instance (Lift b) => Lift (Type b)
+
+instance Lift b => Lift1 (Binding b) where
+    liftLift lf (VarB b a) = liftCon2 'VarB (lift b) (lf a)
+
+instance Lift b => Lift1 (Alter b) where
+    liftLift lf (Alter b a) = liftCon2 'Alter (lift b) (lf a)
+
+instance Lift b => Lift1 (ExprF b) where
+    liftLift lf (InfixEF o a b) =
+        liftCon3 'InfixEF (lift o) (lf a) (lf b)
+    liftLift lf (LetEF r bs e) =
+        liftCon3 'LetEF (lift r) bs' (lf e)
+      where bs' = liftLift (liftLift lf) bs
+    liftLift lf (CaseEF e as) =
+        liftCon2 'CaseEF (lf e) as'
+      where as' = liftLift (liftLift lf) as
+
+deriveEq1 ''Binding
+deriveEq1 ''Alter
+deriveEq1 ''ExprF
+
+instance (Hashable b) => Hashable (Pat b)
+instance (Hashable b, Hashable a) => Hashable (Binding b a)
+instance (Hashable b, Hashable a) => Hashable (Alter b a)
+instance (Hashable b, Hashable a) => Hashable (ExprF b a)
+instance (Hashable b) => Hashable1 (Alter b)
+instance (Hashable b) => Hashable1 (Binding b)
+instance (Hashable b) => Hashable1 (ExprF b)
+
+makeBaseFunctor ''Type
+

src/Rlp/HindleyMilner.hs

@@ -0,0 +1,161 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE OverloadedLists #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Rlp.HindleyMilner
+    ( typeCheckRlpProgR
+    , solve
+    , TypeError(..)
+    , runHM'
+    , HM
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Lens             hiding (Context', Context, (:<), para)
+import Control.Monad.Errorful
+import Control.Monad.State
+import Control.Monad.Accum
+import Control.Monad
+import Control.Arrow            ((>>>))
+import Control.Monad.Writer.Strict
+import Data.Text                qualified as T
+import Data.Pretty
+import Data.Hashable
+import Data.HashMap.Strict      (HashMap)
+import Data.HashMap.Strict      qualified as H
+import Data.HashSet             (HashSet)
+import Data.HashSet             qualified as S
+import Data.Maybe               (fromMaybe)
+import Data.Traversable
+import GHC.Generics             (Generic(..), Generically(..))
+
+import Data.Functor
+import Data.Functor.Foldable
+import Data.Fix                 hiding (cata, para)
+import Control.Comonad.Cofree
+import Control.Comonad
+
+import Compiler.RLPC
+import Compiler.RlpcError
+import Rlp.AltSyntax            as Rlp
+import Core.Syntax              qualified as Core
+import Core.Syntax              (ExprF(..), Lit(..))
+import Rlp.HindleyMilner.Types
+--------------------------------------------------------------------------------
+
+fixCofree :: (Functor f, Functor g)
+          => Iso (Fix f) (Fix g) (Cofree f ()) (Cofree g b)
+fixCofree = iso sa bt where
+    sa = foldFix (() :<)
+    bt (_ :< as) = Fix $ bt <$> as
+
+lookupVar :: PsName -> Context -> HM (Type PsName)
+lookupVar n g = case g ^. contextVars . at n of
+    Just t -> pure t
+    Nothing -> addFatal $ TyErrUntypedVariable n
+
+gather :: RlpExpr PsName -> HM (Type PsName, PartialJudgement)
+gather e = look >>= (H.lookup e >>> maybe memoise pure)
+    where
+        memoise = do
+            r <- gather' e
+            add (H.singleton e r)
+            pure r
+
+gather' :: RlpExpr PsName -> HM (Type PsName, PartialJudgement)
+gather' = \case
+    Finl (LitF (IntL _)) -> pure (IntT, mempty)
+
+    Finl (VarF n) -> do
+        t <- freshTv
+        let j = mempty & assumptions .~ H.singleton n [t]
+        pure (t,j)
+
+    Finl (AppF f x) -> do
+        tfx <- freshTv
+        (tf,jf) <- gather f
+        (tx,jx) <- gather x
+        let jtfx = mempty & constraints .~ [Equality tf (tx :-> tfx)]
+        pure (tfx, jf <> jx <> jtfx)
+
+    Finl (LamF [b] e) -> do
+        tb <- freshTv
+        (te,je) <- gather e
+        let cs = maybe [] (fmap $ Equality tb) (je ^. assumptions . at b)
+            as = je ^. assumptions & at b .~ Nothing
+            j = mempty & constraints .~ cs & assumptions .~ as
+            t = tb :-> te
+        pure (t,j)
+
+unify :: [Constraint] -> HM Context
+
+unify [] = pure mempty
+
+unify (Equality (sx :-> sy) (tx :-> ty) : cs) =
+    unify $ Equality sx tx : Equality sy ty : cs
+
+-- elim
+unify (Equality (ConT s) (ConT t) : cs) | s == t = unify cs
+unify (Equality (VarT s) (VarT t) : cs) | s == t = unify cs
+
+unify (Equality (VarT s) t : cs)
+    | occurs s t = addFatal $ TyErrRecursiveType s t
+    | otherwise  = unify cs' <&> contextVars . at s ?~ t
+  where
+    cs' = cs & each . constraintTypes %~ subst s t
+
+-- swap
+unify (Equality s (VarT t) : cs) = unify (Equality (VarT t) s : cs)
+
+unify (Equality s t : _) = addFatal $ TyErrCouldNotUnify s t
+
+annotate :: RlpExpr PsName
+         -> HM (Cofree (RlpExprF PsName) (Type PsName, PartialJudgement))
+annotate = sequenceA . fixtend (gather . wrapFix)
+
+solveTree :: Cofree (RlpExprF PsName) (Type PsName, PartialJudgement)
+          -> HM (Type PsName)
+solveTree e = undefined
+
+infer1 :: RlpExpr PsName -> HM (Type PsName)
+infer1 e = do
+    ((t,j) :< _) <- annotate e
+    g <- unify (j ^. constraints)
+    pure $ ifoldrOf (contextVars . itraversed) subst t g
+
+solve = undefined
+-- solve g e = do
+--     (t,j) <- gather e
+--     g' <- unify cs
+--     pure $ ifoldrOf (contextVars . itraversed) subst t g'
+
+occurs :: PsName -> Type PsName -> Bool
+occurs n = cata \case
+    VarTF m | n == m -> True
+    t                -> or t
+
+subst :: PsName -> Type PsName -> Type PsName -> Type PsName
+subst n t' = para \case
+    VarTF m | n == m -> t'
+    -- shadowing
+    ForallTF x (pre,post) | x == n    -> ForallT x pre
+                          | otherwise -> ForallT x post
+    t -> embed $ t <&> view _2
+
+prettyHM :: (Pretty a)
+         => Either [TypeError] (a, [Constraint])
+         -> Either [TypeError] (String, [String])
+prettyHM = over (mapped . _1) rpretty
+         . over (mapped . _2 . each) rpretty
+
+fixtend :: Functor f => (f (Fix f) -> b) -> Fix f -> Cofree f b
+fixtend c (Fix f) = c f :< fmap (fixtend c) f
+
+infer :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName))
+infer = undefined
+
+typeCheckRlpProgR :: (Monad m)
+                  => Program PsName (RlpExpr PsName)
+                  -> RLPCT m (Program PsName
+                      (Cofree (RlpExprF PsName) (Type PsName)))
+typeCheckRlpProgR = undefined
+

src/Rlp/HindleyMilner/Types.hs

@@ -0,0 +1,162 @@
+{-# LANGUAGE OverloadedLists #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Rlp.HindleyMilner.Types
+    where
+--------------------------------------------------------------------------------
+import Data.Hashable
+import Data.HashMap.Strict      (HashMap)
+import Data.HashMap.Strict      qualified as H
+import Data.HashSet             (HashSet)
+import Data.HashSet             qualified as S
+import GHC.Generics             (Generic(..), Generically(..))
+import Data.Kind                qualified
+import Data.Text                qualified as T
+import Control.Monad.Writer
+import Control.Monad.Accum
+import Control.Monad.Trans.Accum
+import Control.Monad.Errorful
+import Control.Monad.State
+import Text.Printf
+import Data.Pretty
+import Data.Function
+
+import Control.Lens             hiding (Context', Context)
+
+import Compiler.RlpcError
+import Rlp.AltSyntax
+--------------------------------------------------------------------------------
+
+newtype Context = Context
+    { _contextVars      :: HashMap PsName (Type PsName)
+    }
+    deriving (Show, Generic)
+    deriving (Semigroup, Monoid)
+        via Generically Context
+
+data Constraint = Equality (Type PsName) (Type PsName)
+    deriving (Eq, Generic, Show)
+
+data PartialJudgement = PartialJudgement
+    { _constraints :: [Constraint]
+    , _assumptions :: HashMap PsName [Type PsName]
+    }
+    deriving (Generic, Show)
+    deriving (Monoid)
+        via Generically PartialJudgement
+
+instance Semigroup PartialJudgement where
+    a <> b = PartialJudgement
+        { _constraints = ((<>) `on` _constraints) a b
+        , _assumptions = (H.unionWith (<>) `on` _assumptions) a b
+        }
+
+instance Hashable Constraint
+
+type Memo = HashMap (RlpExpr PsName) (Type PsName, PartialJudgement)
+
+type HM = ErrorfulT TypeError (StateT Int (Accum Memo))
+
+-- | Type error enum.
+data TypeError
+    -- | Two types could not be unified
+    = TyErrCouldNotUnify (Type Name) (Type Name)
+    -- | @x@ could not be unified with @t@ because @x@ occurs in @t@
+    | TyErrRecursiveType Name (Type Name)
+    -- | Untyped, potentially undefined variable
+    | TyErrUntypedVariable Name
+    | TyErrMissingTypeSig Name
+    | TyErrNonHomogenousCaseAlternatives (RlpExpr PsName)
+    deriving (Show)
+
+instance IsRlpcError TypeError where
+    liftRlpcError = \case
+        -- todo: use anti-parser instead of show
+        TyErrCouldNotUnify t u -> Text
+            [ T.pack $ printf "Could not match type `%s` with `%s`."
+                              (rpretty @String t) (rpretty @String u)
+            , "Expected: " <> rpretty t
+            , "Got: " <> rpretty u
+            ]
+        TyErrUntypedVariable n -> Text
+            [ "Untyped (likely undefined) variable `" <> n <> "`"
+            ]
+        TyErrRecursiveType t x -> Text
+            [ T.pack $ printf "Recursive type: `%s' occurs in `%s'"
+                              (rpretty @String t) (rpretty @String x)
+            ]
+
+-- type Memo t = HashMap t (Type PsName, PartialJudgement)
+
+-- newtype HM t a = HM { unHM :: Int -> Memo t -> (a, Int, Memo t) }
+
+-- runHM :: (Hashable t) => HM t a -> (a, Memo t)
+-- runHM hm = let (a,_,m) = unHM hm 0 mempty in (a,m)
+
+-- instance Functor (HM t) where
+--     fmap f (HM h) = HM \n m -> h n m & _1 %~ f
+
+-- instance Applicative (HM t) where
+--     pure a = HM \n m -> (a,n,m)
+--     HM hf <*> HM ha = HM \n m ->
+--         let (f',n',m') = hf n m
+--             (a,n'',m'') = ha n' m'
+--         in (f' a, n'', m'')
+
+-- instance Monad (HM t) where
+--     HM ha >>= k = HM \n m ->
+--         let (a,n',m') = ha n m
+--             (a',n'',m'') = unHM (k a) n' m'
+--         in (a',n'', m'')
+
+-- instance Hashable t => MonadWriter (Memo t) (HM t) where
+--     -- IMPORTAN! (<>) is left-biased for HashMap! append `w` to the RIGHt!
+--     writer (a,w) = HM \n m -> (a,n,m <> w)
+--     listen ma = HM \n m ->
+--         let (a,n',m') = unHM ma n m
+--         in ((a,m'),n',m')
+--     pass maww = HM \n m ->
+--         let ((a,ww),n',m') = unHM maww n m
+--         in (a,n',ww m')
+
+-- instance MonadState Int (HM t) where
+--     state f = HM \n m ->
+--         let (a,n') = f n
+--         in (a,n',m)
+
+freshTv :: HM (Type PsName)
+freshTv = do
+    n <- get
+    modify succ
+    pure . VarT $ "$a" <> T.pack (show n)
+
+runHM' :: HM a -> Either [TypeError] a
+runHM' e = maybe (Left es) Right ma
+    where
+        ((ma,es),m) = (`runAccum` mempty) . (`evalStateT` 0) . runErrorfulT $ e
+
+-- addConstraint :: Constraint -> HM ()
+-- addConstraint = tell . pure
+
+makePrisms ''PartialJudgement
+makeLenses ''PartialJudgement
+makeLenses ''Context
+makePrisms ''Constraint
+makePrisms ''TypeError
+
+supplement :: [(PsName, Type PsName)] -> Context -> Context
+supplement bs = contextVars %~ (H.fromList bs <>)
+
+demoContext :: Context
+demoContext = Context
+    { _contextVars =
+        [ ("+#", IntT :-> IntT :-> IntT)
+        ]
+    }
+
+constraintTypes :: Traversal' Constraint (Type PsName)
+constraintTypes k (Equality s t) = Equality <$> k s <*> k t
+
+instance Pretty Constraint where
+    pretty (Equality s t) =
+        hsep [prettyPrec appPrec1 s, "~", prettyPrec appPrec1 t]
+

src/Rlp/Lex.x

@@ -14,6 +14,7 @@ module Rlp.Lex
     , popLexState
     , programInitState
     , runP'
+    , popLayout
     )
     where
 import Codec.Binary.UTF8.String (encodeChar)
@@ -61,7 +62,7 @@ $asciisym       = [\!\#\$\%\&\*\+\.\/\<\=\>\?\@\\\^\|\-\~\:]
     |infixr|infixl|infix
 
 @reservedop =
-    "=" | \\ | "->" | "|" | "::"
+    "=" | \\ | "->" | "|" | ":"
 
 rlp :-
     
@@ -167,9 +168,10 @@ lexReservedName = \case
 lexReservedOp :: Text -> RlpToken
 lexReservedOp = \case
     "="     -> TokenEquals
-    "::"    -> TokenHasType
+    ":"     -> TokenHasType
     "|"     -> TokenPipe
     "->"    -> TokenArrow
+    "\\"    -> TokenLambda
     s       -> error (show s)
 
 -- | @andBegin@, with the subtle difference that the start code is set

src/Rlp/Parse.y

@@ -84,7 +84,7 @@ VL  : vlbrace       { () }
 
 VR  :: { () }
 VR  : vrbrace       { () }
-    | error         { () }
+    | error         {% void popLayout }
 
 VS                  :: { () }
 VS                  : ';'                   { () }

src/Rlp/Parse/Types.hs

@@ -18,7 +18,7 @@ module Rlp.Parse.Types
     , RlpToken(..), AlexInput(..), Position(..), spanFromPos, LexerAction
     , Located(..), PsName
     -- ** Lenses
-    , _TokenLitInt, _TokenVarName, _TokenConName, _TokenVarSym
+    , _TokenLitInt, _TokenVarName, _TokenConName, _TokenVarSym, _TokenConSym
     , aiPrevChar, aiSource, aiBytes, aiPos, posLine, posColumn
 
     -- * Error handling
@@ -277,7 +277,7 @@ initAlexInput s = AlexInput
     { _aiPrevChar   = '\0'
     , _aiSource     = s
     , _aiBytes      = []
-    , _aiPos        = (1,1,0)
+    , _aiPos        = (1,0,0)
     }
 
 --------------------------------------------------------------------------------

src/Rlp/Syntax/Good.hs

@@ -0,0 +1,56 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Rlp.Syntax.Good
+    ( Decl(..), Program(..)
+    , programDecls
+    , Mistake(..)
+    )
+    where
+--------------------------------------------------------------------------------
+import Data.Kind
+import Control.Lens
+import Rlp.Syntax.Types (NameP)
+import Rlp.Syntax.Types qualified as Rlp
+--------------------------------------------------------------------------------
+
+data Program b a = Program
+    { _programDecls :: [Decl b a]
+    }
+
+data Decl p a = FunD   (NameP p) [Rlp.Pat p] a
+              | TySigD [NameP p] (Rlp.Ty p)
+              | DataD  (NameP p) [NameP p] [Rlp.ConAlt p]
+              | InfixD Rlp.Assoc Int (NameP p)
+
+type Where p a = [Binding p a]
+
+data Binding p a = PatB (Rlp.Pat p) a
+    deriving (Functor, Foldable, Traversable)
+
+makeLenses ''Program
+
+class Mistake a where
+    type family Ammend a :: Type
+    ammendMistake :: a -> Ammend a
+
+instance Mistake (Rlp.Program p a) where
+    type Ammend (Rlp.Program p a) = Program p (Rlp.Expr' p a)
+
+    ammendMistake p = Program
+        { _programDecls = ammendMistake <$> Rlp._programDecls p
+        }
+
+instance Mistake (Rlp.Decl p a) where
+    type Ammend (Rlp.Decl p a) = Decl p (Rlp.Expr' p a)
+
+    ammendMistake = \case
+        Rlp.FunD n as e _  -> FunD n as e
+        Rlp.TySigD ns t    -> TySigD ns t
+        Rlp.DataD n as cs  -> DataD n as cs
+        Rlp.InfixD ass p n -> InfixD ass p n
+
+instance Mistake (Rlp.Binding p a) where
+    type Ammend (Rlp.Binding p a) = Binding p (Rlp.ExprF p a)
+
+    ammendMistake = \case
+        Rlp.PatB k v -> PatB k v
+

src/Rlp/Syntax/Types.hs

@@ -15,7 +15,7 @@ module Rlp.Syntax.Types
     , Rec(..)
     , Lit(..)
     , Pat(..)
-    , Decl(..)
+    , Decl(..), Decl'
     , Program(..)
     , Where
 
@@ -23,6 +23,8 @@ module Rlp.Syntax.Types
     , Cofree(..)
     , Trans.Cofree.CofreeF
     , SrcSpan(..)
+
+    , programDecls
     )
     where
 ----------------------------------------------------------------------------------

src/Rlp/TH.hs

@@ -13,16 +13,14 @@ import Control.Monad.IO.Class
 import Control.Monad
 
 import Compiler.RLPC
-import Rlp.Parse
+import Rlp.AltParse
 --------------------------------------------------------------------------------
 
 rlpProg :: QuasiQuoter
-rlpProg = undefined
+rlpProg = mkqq parseRlpProgR
--- rlpProg = mkqq parseRlpProgR
 
 rlpExpr :: QuasiQuoter
-rlpExpr = undefined
+rlpExpr = mkqq parseRlpExprR
--- rlpExpr = mkqq parseRlpExprR
 
 mkq :: (Lift a) => (Text -> RLPCIO a) -> String -> Q Exp
 mkq parse = evalAndParse >=> lift where

src/Rlp2Core.hs

@@ -28,6 +28,7 @@ import Data.Functor.Bind
 import Data.Function                    (on)
 import GHC.Stack
 import Debug.Trace
+import Numeric
 
 import Effectful.State.Static.Local
 import Effectful.Labeled
@@ -35,18 +36,11 @@ import Effectful
 import Text.Show.Deriving
 
 import Core.Syntax                      as Core
+import Rlp.AltSyntax                    as Rlp
 import Compiler.Types
 import Data.Pretty                      (render, pretty)
-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
@@ -65,180 +59,49 @@ deriveShow1 ''Branch
 
 --------------------------------------------------------------------------------
 
-desugarRlpProgR :: forall m. (Monad m) => RlpProgram RlpcPs -> RLPCT m Program'
+desugarRlpProgR :: forall m a. (Monad m)
+                => Rlp.Program PsName a
+                -> RLPCT m Core.Program'
 desugarRlpProgR p = do
     let p' = desugarRlpProg p
     addDebugMsg "dump-desugared" $ render (pretty p')
     pure p'
 
-desugarRlpProg :: RlpProgram RlpcPs -> Program'
+desugarRlpProg = undefined
-desugarRlpProg = rlpProgToCore
 
-desugarRlpExpr :: RlpExpr RlpcPs -> Expr'
+desugarRlpExpr = undefined
-desugarRlpExpr = runPureEff . runNameSupply "anon" . exprToCore
+
+runNameSupply :: Text -> Eff (NameSupply ': es) a -> Eff es a
+runNameSupply pre = undefined -- evalState [ pre <> "_" <> tshow name | name <- [0..] ]
 
 -- the rl' program is desugared by desugaring each declaration as a separate
 -- program, and taking the monoidal product of the lot :3
 
-rlpProgToCore :: RlpProgram RlpcPs -> Program'
+rlpProgToCore :: Rlp.Program PsName (RlpExpr PsName) -> Program'
-rlpProgToCore = foldMapOf (progDecls . each) declToCore
+rlpProgToCore = foldMapOf (programDecls . each) declToCore
 
-declToCore :: Decl' RlpcPs -> Program'
+declToCore :: Rlp.Decl PsName (RlpExpr PsName) -> Program'
 
-declToCore (TySigD'' ns t) = mempty &
+-- assume all arguments are VarP's for now
-    programTypeSigs .~ H.fromList [ (n, typeToCore t) | n <- ns ]
+declToCore (FunD b as e) = mempty & programScDefs .~ [ScDef b as' e']
-
-declToCore (DataD'' n as ds) = fold . getZipList $
-    constructorToCore t' <$> ZipList [0..] <*> ZipList ds
     where
-        -- create the appropriate type from the declared constructor and its
+        as' = as ^.. each . singular _VarP
-        -- arguments
+        e' = runPureEff . runNameSupply b . exprToCore $ e
-        t' = foldl TyApp (TyCon n) (TyVar . dsNameToName <$> as)
 
--- TODO: where-binds
+type NameSupply = State [Name]
-declToCore fd@(FunD'' n as e _) = mempty & programScDefs .~ [ScDef n' as' e']
+
+exprToCore :: (NameSupply :> es)
+           => RlpExpr PsName -> Eff es Core.Expr'
+exprToCore = foldFixM \case
+    InL e -> pure $ Fix e
+    InR e -> rlpExprToCore e
+
+rlpExprToCore :: (NameSupply :> es)
+           => Rlp.ExprF PsName Core.Expr' -> Eff es Core.Expr'
+
+-- assume all binders are simple variable patterns for now
+rlpExprToCore (LetEF r bs e) = pure $ Let r bs' e
   where
-        n' = dsNameToName n
+    bs' = b2b <$> bs
-        e' = runPureEff . runNameSupply n . exprToCore . unXRec $ e
+    b2b (VarB (VarP k) v) = Binding k v
-        as' = as <&> \case
-            (unXRec -> VarP k) -> dsNameToName k
-            _                  -> error "no patargs yet"
-
-type NameSupply = Labeled NameSupplyLabel (State [IdP RlpcPs])
-type NameSupplyLabel = "expr-name-supply"
-
-exprToCore :: forall es. (NameSupply :> es) => RlpExpr RlpcPs -> Eff es Expr'
-
-exprToCore (VarE n) = pure $ Var (dsNameToName n)
-
-exprToCore (AppE a b) = (liftA2 App `on` exprToCore . unXRec) a b
-
-exprToCore (OAppE f a b) = (liftA2 mkApp `on` exprToCore . unXRec) a b
-    where
-        mkApp s t = (Var f `App` s) `App` t
-
-exprToCore (CaseE (unXRec -> e) as) = do
-    e' <- exprToCore e
-    Case e' <$> caseAltToCore `traverse` as
-
-exprToCore (LetE bs e) = letToCore NonRec bs e
-exprToCore (LetrecE bs e) = letToCore Rec bs e
-
-exprToCore (LitE l) = litToCore l
-
-letToCore :: forall es. (NameSupply :> es)
-          => Rec -> [Rlp.Binding' RlpcPs] -> RlpExpr' RlpcPs -> Eff es Expr'
-letToCore r bs e = do
-    -- TODO: preserve binder order.
-    (bs',as) <- getParts
-    let insbs | null bs'  = pure
-              | otherwise = pure . Let r bs'
-    appKendo (foldMap Kendo (as `snoc` insbs)) <=< exprToCore $ unXRec e
-  where
-    -- partition & map the list of binders into:
-    --  bs'   : the let-binds that may be directly translated to Core
-    --          let-binds (we do exactly that). this is all the binders that
-    --          are a simple variable rather than a pattern match.
-    -- and as : the let-binds that may **not** be directly translated to
-    --          Core let-exprs. they get turned into case alternates.
-    getParts = traverse f bs <&> partitionEithers
-
-    f :: Rlp.Binding' RlpcPs
-      -> Eff es (Either Core.Binding' (Expr' -> Eff es Expr'))
-    f (PatB'' (VarP'' n) e) = Left . (n :=) <$> exprToCore (unXRec e)
-    f (PatB'' p          e) = pure $ Right (caseify p e)
-
-litToCore :: (NameSupply :> es) => Rlp.Lit RlpcPs -> Eff es Expr'
-litToCore (Rlp.IntL n) = pure . Lit $ Core.IntL n
-
-{-
-let C x = y
-in e
-
-case y of
-    C x -> e
- -}
-
-caseify :: (NameSupply :> es)
-        => Pat' RlpcPs -> RlpExpr' RlpcPs -> Expr' -> Eff es Expr'
-caseify p (unXRec -> e) i =
-    Case <$> exprToCore e <*> ((:[]) <$> alt)
-  where
-    alt = conToRose (unXRec p) <&> foldFix (branchToCore i)
-
--- TODO: where-binds
-caseAltToCore :: (HasCallStack, NameSupply :> es)
-              => (Alt RlpcPs, Where RlpcPs) -> Eff es Alter'
-caseAltToCore (AltA (unXRec -> p) e, wh) = do
-    e' <- exprToCore . unXRec $ e
-    conToRose p <&> foldFix (branchToCore e')
-
-altToCore :: (NameSupply :> es)
-          => Alt RlpcPs -> Eff es Alter'
-altToCore (AltA p e) = altToCore' p e
-
-altToCore' :: (NameSupply :> es)
-           => Pat' RlpcPs -> RlpExpr' RlpcPs -> Eff es Alter'
-altToCore' (unXRec -> p) (unXRec -> e) = do
-    e' <- exprToCore e
-    conToRose p <&> foldFix (branchToCore e')
-
-conToRose :: forall es. (HasCallStack, NameSupply :> es) => Pat RlpcPs -> Eff es Rose
-conToRose (ConP cn as) = Fix . Branch cn <$> patToForrest `traverse` as
-    where
-        patToForrest :: Pat' RlpcPs -> Eff es (Tree Rose)
-        patToForrest (VarP'' x) = pure $ Left (dsNameToName x)
-        patToForrest p@(ConP'' _ _) =
-            Right <$> liftA2 (,) uniqueName br
-          where
-            br = unwrapFix <$> conToRose (unXRec p)
-conToRose s = error $ "conToRose: not a ConP!: " <> show s
-
-branchToCore :: Expr' -> Branch Alter' -> Alter'
-branchToCore e (Branch cn as) = Alter (AltData cn) myBinds e'
-    where
-        -- gather binders for the /current/ pattern, and build an expression
-        -- matching subpatterns
-        (e', myBinds) = mapAccumL f e as
-
-        f :: Expr' -> Tree Alter' -> (Expr', Name)
-        f e (Left n)       = (e, dsNameToName n)
-        f e (Right (n,cs)) = (e', dsNameToName n) where
-            e' = Case (Var $ dsNameToName n) [branchToCore e cs]
-
-runNameSupply :: IdP RlpcPs -> Eff (NameSupply ': es) a -> Eff es a
-runNameSupply n = runLabeled @NameSupplyLabel (evalState ns) where
-    ns = [ "$" <> n <> "_" <> T.pack (show k) | k <- [0..] ]
-
--- | debug helper
-
-nameSupply :: [IdP RlpcPs]
-nameSupply = [ T.pack $ "$x_" <> show n | n <- [0..] ]
-
-uniqueName :: (NameSupply :> es) => Eff es (IdP RlpcPs)
-uniqueName = labeled @NameSupplyLabel @(State [IdP RlpcPs]) $
-    state @[IdP RlpcPs] (fromMaybe err . uncons)
-  where
-    err = error "NameSupply ran out of names! This shound never happen.\
-                \ The caller of runNameSupply is responsible."
-
-constructorToCore :: Type -> Tag -> ConAlt RlpcPs -> Program'
-constructorToCore t tag (ConAlt cn as) =
-    mempty & programTypeSigs . at cn ?~ foldr (:->) t as'
-           & programDataTags . at cn ?~ (tag, length as)
-    where
-        as' = typeToCore <$> as
-
-typeToCore :: RlpType' RlpcPs -> Type
-typeToCore FunConT''    = TyFun
-typeToCore (FunT'' s t) = typeToCore s :-> typeToCore t
-typeToCore (AppT'' s t) = TyApp (typeToCore s) (typeToCore t)
-typeToCore (ConT'' n)   = TyCon (dsNameToName n)
-typeToCore (VarT'' x)   = TyVar (dsNameToName x)
-
--- | Forwards-compatiblity if IdP RlpDs is changed
-dsNameToName :: IdP RlpcPs -> Name
-dsNameToName = id
-
--}
 

tst/Rlp/HindleyMilnerSpec.hs

@@ -0,0 +1,14 @@
+{-# LANGUAGE TemplateHaskell, QuasiQuotes #-}
+module Rlp.HindleyMilnerSpec
+    ( spec
+    )
+    where
+--------------------------------------------------------------------------------
+import Test.Hspec
+import Rlp.TH
+import Rlp.HindleyMilner
+--------------------------------------------------------------------------------
+
+spec :: Spec
+spec = undefined
+