something

app/Server.hs

@@ -11,7 +11,7 @@ import Data.Text.Encoding           qualified as T
 import Data.Text                    (Text)
 import Data.Text                    qualified as T
 import Data.Text.IO                 qualified as T
-import Data.Pretty
+import Data.Pretty                  hiding (annotate)
 import Data.Aeson
 import Data.Function
 import Control.Arrow
@@ -43,7 +43,8 @@ application :: WS.ServerApp
 application pending = do
     WS.acceptRequest pending >>= talk
 
-newtype Command = Annotate Text
+data Command = Annotate Text
+             | PartiallyAnnotate Text
     deriving Show
 
 instance FromJSON Command where
@@ -51,6 +52,7 @@ instance FromJSON Command where
         cmd :: Text <- v .: "command"
         case cmd of
             "annotate"           -> Annotate <$> v .: "source"
+            "partially-annotate" -> PartiallyAnnotate <$> v .: "source"
             _          -> empty
 
 data Response = Annotated Value
@@ -75,12 +77,20 @@ doCommand conn c = do
 respond :: Command -> Response
 respond (Annotate s)
     = s & (parseRlpProgR >=> typeCheckRlpProgR)
-        & fmap (\p -> p ^.. programDecls . each . _FunD
-           <&> serialiseSc)
+        & fmap (\p -> p ^.. funDs
+           <&> \sc -> serialiseSc (sc & _3 . mapped %~ rout @String))
         & runRLPCJsonDef
         & Annotated
-  where
-    serialiseSc (n,as,e) = object
+
+showPartialAnn = undefined
+
+funDs :: Traversal' (Program b a) (b, [Pat b], a)
+funDs = programDecls . each . _FunD
+
+serialiseSc :: ToJSON a
+            => (PsName, [Pat PsName], Cofree (RlpExprF PsName) a)
+            -> Value
+serialiseSc (n,as,e) = object
     [ "name" .= n
     , "args" .= as
     , "body" .= let rootType = extract e

src/Rlp/AltSyntax.hs

@@ -6,6 +6,7 @@ module Rlp.AltSyntax
     , RlpExprF, RlpExpr, Binding(..), Alter(..)
     , DataCon(..), Type(..)
     , pattern IntT
+    , Core.Rec(..)
 
     , AnnotatedRlpExpr, TypedRlpExpr
     , TypeF(..)
@@ -179,6 +180,8 @@ instance (Out b) => Out (Type b) where
     outPrec p (AppT f x) = maybeParens (p>appPrec) $
         outPrec appPrec f <+> outPrec appPrec1 x
     outPrec p FunT = maybeParens (p>0) "->"
+    outPrec p (ForallT x m) = maybeParens (p>0) $
+        hsep [ "∀", ttext x, outPrec 0 m ]
 
 instance (Out b) => Out (Pat b) where
     outPrec p (VarP b) = outPrec p b

src/Rlp/HindleyMilner.hs

@@ -5,6 +5,7 @@ module Rlp.HindleyMilner
     , annotate
     , TypeError(..)
     , runHM'
+    , liftHM
     , HM
     , prettyVars
     , prettyVars'
@@ -29,6 +30,7 @@ import Data.Hashable
 import Data.HashMap.Strict      (HashMap)
 import Data.HashMap.Strict      qualified as H
 import Data.HashSet             (HashSet)
+import Data.HashSet.Lens
 import Data.HashSet             qualified as S
 import Data.Maybe               (fromMaybe)
 import Data.Traversable
@@ -95,6 +97,15 @@ gather' = \case
             t = foldr (:->) te tbs
         pure (t,j)
 
+    Finr (LetEF NonRec [VarB (VarP x) y] e) -> do
+        (ty,jy) <- gather y
+        (te,je) <- gather e
+        traceM $ "ty: " <> show ty
+        traceM $ "jy: " <> show jy
+        traceM $ "te: " <> show te
+        traceM $ "je: " <> show je
+        undefined
+
     -- Finl (LamF [b] e) -> do
     --     tb <- freshTv
     --     (te,je) <- gather e
@@ -104,6 +115,12 @@ gather' = \case
     --         t = tb :-> te
     --     pure (t,j)
 
+generalise :: Context -> Type PsName -> Type PsName
+generalise g t = ifoldr (\n _ s -> ForallT n s) t vs
+    where
+        vs = H.difference (freeVariables t ^. hashMap)
+                          (g ^. contextTyVars)
+
 unify :: [Constraint] -> HM [(PsName, Type PsName)]
 
 unify [] = pure mempty
@@ -124,6 +141,7 @@ unify (Equality (VarT s) t : cs)
 -- swap
 unify (Equality s (VarT t) : cs) = unify (Equality (VarT t) s : cs)
 
+-- failure!
 unify (Equality s t : _) = addFatal $ TyErrCouldNotUnify s t
 
 annotate :: RlpExpr PsName
@@ -135,10 +153,6 @@ assocs f []         = pure []
 assocs f ((k,v):xs) = (\v' xs' -> (k,v') : xs')
                   <$> indexed f k v <*> assocs f xs
 
-traceSubst k v t = trace ("subst " <> show' k <> " " <> show' v <> " " <> show' t)
-                 $ subst k v t
-                 where show' a = showsPrec 11 a mempty
-
 elimAssumptions :: Assumptions -> PsName -> Type PsName -> [Constraint]
 -- elimAssumptions b tb as = maybe [] (fmap $ Equality tb) (as ^. at b)
 elimAssumptions as b tb =
@@ -166,23 +180,23 @@ infer g0 e = do
 infer1 :: Context -> RlpExpr PsName -> HM (Type PsName)
 infer1 g = fmap extract . infer g
 
-unionContextWithKeyM :: Monad m
-                     => (PsName -> Type PsName -> Type PsName
-                                               -> m (Type PsName))
-                     -> Context -> Context -> m Context
-unionContextWithKeyM f a b = Context <$> unionWithKeyM f a' b'
-    where
-        a' = a ^. contextVars
-        b' = b ^. contextVars
+-- unionContextWithKeyM :: Monad m
+--                      => (PsName -> Type PsName -> Type PsName
+--                                                -> m (Type PsName))
+--                      -> Context -> Context -> m Context
+-- unionContextWithKeyM f a b = Context <$> unionWithKeyM f a' b'
+--     where
+--         a' = a ^. contextVars
+--         b' = b ^. contextVars
 
-unionWithKeyM :: forall m k v. (Eq k, Hashable k, Monad m)
-              => (k -> v -> v -> m v) -> HashMap k v -> HashMap k v
-              -> m (HashMap k v)
-unionWithKeyM f a b = sequenceA $ H.unionWithKey f' ma mb
-    where
-        f' k x y = join $ liftA2 (f k) x y
-        ma = fmap (pure @m) a
-        mb = fmap (pure @m) b
+-- unionWithKeyM :: forall m k v. (Eq k, Hashable k, Monad m)
+--               => (k -> v -> v -> m v) -> HashMap k v -> HashMap k v
+--               -> m (HashMap k v)
+-- unionWithKeyM f a b = sequenceA $ H.unionWithKey f' ma mb
+--     where
+--         f' k x y = join $ liftA2 (f k) x y
+--         ma = fmap (pure @m) a
+--         mb = fmap (pure @m) b
 
 -- solve :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName))
 -- solve = solve' mempty
@@ -213,8 +227,8 @@ fixtend :: Functor f => (f (Fix f) -> b) -> Fix f -> Cofree f b
 fixtend c (Fix f) = c f :< fmap (fixtend c) f
 
 buildInitialContext :: Program PsName a -> Context
-buildInitialContext =
-    Context . H.fromList . toListOf (programDecls . each . _TySigD)
+buildInitialContext = const mempty
+    -- Context . H.fromList . toListOf (programDecls . each . _TySigD)
 
 typeCheckRlpProgR :: (Monad m)
                   => Program PsName (RlpExpr PsName)
@@ -241,7 +255,7 @@ liftHM = liftEither . runHM'
 freeVariables :: Type PsName -> HashSet PsName
 freeVariables = cata \case
     VarTF x -> S.singleton x
-    ForallTF x m -> m `S.difference` S.singleton x
+    ForallTF x m -> S.delete x m
     vs -> fold vs
 
 boundVariables :: Type PsName -> HashSet PsName

src/Rlp/HindleyMilner/Types.hs

@@ -26,8 +26,9 @@ import Compiler.RlpcError
 import Rlp.AltSyntax
 --------------------------------------------------------------------------------
 
-newtype Context = Context
+data Context = Context
     { _contextVars      :: HashMap PsName (Type PsName)
+    , _contextTyVars    :: HashMap PsName (Type PsName)
     }
     deriving (Show, Generic)
     deriving (Semigroup, Monoid)