lintCoreProg

src/Core/Syntax.hs

@@ -33,10 +33,10 @@ module Core.Syntax
     , Pretty(pretty), WithTerseBinds(..)
 
     -- * Optics
-    , programScDefs, programTypeSigs, programDataTags
-    , formalising
+    , programScDefs, programTypeSigs, programDataTags, programTyCons
+    , formalising, lambdaLifting
     , HasRHS(_rhs), HasLHS(_lhs)
-    , _BindingF, _MkVar
+    , _BindingF, _MkVar, _ScDef
     -- ** Classy optics
     , HasBinders(..), HasArrowStops(..), HasApplicants1(..), HasApplicants(..)
     )
@@ -216,6 +216,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 +244,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
@@ -621,6 +631,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 +703,5 @@ deriving instance (Eq b, Eq a) => Eq (ExprF b a)
 
 makePrisms ''BindingF
 makePrisms ''Var
+makePrisms ''ScDef
 

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
-lint = undefined
+lintDontCheck :: Program Var -> Program Name
+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