almost done

src/Core/Parse.y

@@ -128,7 +128,8 @@ TypeApp         :: { Type }
 Type1           :: { Type }
 Type1           : '(' Type ')'                  { $2 }
                 | varname                       { TyVar $1 }
-                | conname                       { TyCon $1 }
+                | conname                       { if $1 == "Type"
+                                                    then TyKindType else TyCon $1 }
 
 ParList      :: { [Name] }
 ParList      : varname ParList            { $1 : $2 }

src/Core/Syntax.hs

@@ -16,13 +16,13 @@ module Core.Syntax
     , ScDef(..), ScDef'
     , Program(..), Program'
     , Type(..), Kind, pattern (:->), pattern TyInt
-    , Alter(..), Alter', AltCon(..)
+    , AlterF(..), Alter(..), Alter', AltCon(..)
     , pattern Binding, pattern Alter
     , Rec(..), Lit(..)
     , Pragma(..)
     -- ** Variables and identifiers
-    , Name, Var(..), Tag
+    , Name, Var(..), Tag, pattern (:^)
-    , Binding(..), pattern (:=), pattern (:$)
+    , Binding, BindingF(..), pattern (:=), pattern (:$)
     , type Binding'
     -- ** Working with the fixed point of ExprF
     , Expr, Expr'
@@ -36,7 +36,7 @@ module Core.Syntax
     , programScDefs, programTypeSigs, programDataTags
     , formalising
     , HasRHS(_rhs), HasLHS(_lhs)
-    , applicants
+    , _BindingF, _MkVar
     -- ** Classy optics
     , HasBinders(..), HasArrowStops(..)
     )
@@ -110,6 +110,9 @@ type Kind = Type
 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
 
@@ -286,11 +289,13 @@ formalising = iso sa bt where
     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
 
 --------------------------------------------------------------------------------
@@ -386,6 +391,9 @@ instance Pretty Type where
         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
@@ -569,6 +577,9 @@ deriving instance Lift b => Lift (Program 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 HasApplicants (ExprF b (Fix (ExprF b))) (ExprF b (Fix (ExprF b)))
 --                        (Fix (ExprF b)) (Fix (ExprF b)) where
 --     applicants k (AppF f x) = AppF <$> applicants k f <*> k x
@@ -580,9 +591,9 @@ deriving instance Lift b => Lift (Program b)
 --                => LensLike' g (Fix f) (Fix f)
 --     applicants k (Fix f) = Fix <$> applicants k f
 
-applicants :: Traversal' (Expr b) (Expr b)
+-- applicants :: Traversal' (Expr b) (Expr b)
-applicants k (App f x) = App <$> applicants k f <*> k x
+-- applicants k (App f x) = App <$> applicants k f <*> k x
-applicants k x         = k x
+-- applicants 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
@@ -635,6 +646,7 @@ class HasArrowStops s t a b | s -> a, t -> b, s b -> t, t a -> s where
 
 instance HasArrowStops Type Type Type Type where
     arrowStops k (s :-> t) = (:->) <$> k s <*> arrowStops k t
+    arrowStops k t = k t
 
 --------------------------------------------------------------------------------
 
@@ -667,3 +679,6 @@ deriveEq1 ''ExprF
 
 deriving instance (Eq b, Eq a) => Eq (ExprF b a)
 
+makePrisms ''BindingF
+makePrisms ''Var
+

src/Core/SystemF.hs

@@ -1,15 +1,204 @@
+{-# 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 Control.Comonad
+import Control.Comonad.Cofree
+import Data.Fix
+import Data.Functor
+
+import Control.Lens                 hiding ((:<))
+import Control.Lens.Unsound
+
 import Compiler.RLPC
 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 TypeError
+
+data TypeError = TypeErrorUndefinedVariable Name
+               | TypeErrorKindMismatch Kind Kind
+               | TypeErrorCouldNotMatch Type Type
+               deriving Show
+
+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 (TypeErrorCouldNotMatch 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 (TypeErrorCouldNotMatch t t')
+            Left e -> Left e
+
+    Case e as -> do
+        (ts,as') <- unzip <$> checkAlt `traverse` as
+        unless (allSame ts) $
+            Left (error "unifica oh my god fix this later")
+        e' <- lintE g e
+        pure $ head ts :< CaseF e' as'
+      where
+        checkAlt :: Alter Var -> SysF (Type, AlterF Var ET)
+        checkAlt (AlterF (AltData con) bs e) = do
+            ct <- lookupVar g con
+            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 (TypeErrorCouldNotMatch t t')
+
+unforall :: Type -> Type
+unforall (TyForall _ m) = m
+unforall m = 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 (TypeErrorCouldNotMatch 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 (TypeErrorUndefinedVariable n)
+
+lookupVar :: Gamma -> Name -> SysF Type
+lookupVar g n = case g ^. gammaVars . at n of
+    Just t -> Right t
+    Nothing -> Left (TypeErrorUndefinedVariable n)
+
+lookupTyVar :: Gamma -> Name -> SysF Kind
+lookupTyVar g n = case g ^. gammaTyVars . at n of
+    Just k -> Right k
+    Nothing -> Left (TypeErrorUndefinedVariable 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)
+        ]
+    }
+