preparing for rewrite #100

src/Rlp/HindleyMilner.hs

@@ -2,11 +2,12 @@
 {-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE TemplateHaskell #-}
 module Rlp.HindleyMilner
-    -- ( infer
-    -- , check
-    -- , TypeError(..)
-    -- , HMError
-    -- )
+    ( typeCheckRlpProgR
+    , solve
+    , TypeError(..)
+    , runHM'
+    , HM
+    )
     where
 --------------------------------------------------------------------------------
 import Control.Lens             hiding (Context', Context, (:<), para)
@@ -31,6 +32,7 @@ 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
@@ -120,3 +122,15 @@ prettyHM :: (Pretty a)
 prettyHM = over (mapped . _1) rpretty
          . over (mapped . _2 . each) rpretty
 
+fixtend :: (f (Fix f) -> b) -> Fix f -> Cofree f b
+fixtend = undefined
+
+infer :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName))
+infer = _ . fixtend (solve _ . wrapFix)
+
+typeCheckRlpProgR :: (Monad m)
+                  => Program PsName (RlpExpr PsName)
+                  -> RLPCT m (Program PsName
+                      (Cofree (RlpExprF PsName) (Type PsName)))
+typeCheckRlpProgR = undefined
+

src/Rlp/HindleyMilner/Types.hs

@@ -26,6 +26,9 @@ import Rlp.AltSyntax
 newtype Context = Context
     { _contextVars      :: HashMap PsName (Type PsName)
     }
+    deriving (Generic)
+    deriving (Semigroup, Monoid)
+        via Generically Context
 
 data Constraint = Equality (Type PsName) (Type PsName)
     deriving (Eq, Generic, Show)
@@ -49,6 +52,7 @@ data TypeError
     -- | Untyped, potentially undefined variable
     | TyErrUntypedVariable Name
     | TyErrMissingTypeSig Name
+    | TyErrNonHomogenousCaseAlternatives (RlpExpr PsName)
     deriving (Show)
 
 instance IsRlpcError TypeError where
@@ -124,6 +128,7 @@ addConstraint = tell . pure
 
 makeLenses ''Context
 makePrisms ''Constraint
+makePrisms ''TypeError
 
 supplement :: [(PsName, Type PsName)] -> Context -> Context
 supplement bs = contextVars %~ (H.fromList bs <>)

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
+