~jojo/Carth

bc08ce7bc82bbe664803876deb503b172eca4529 — JoJo 1 year, 10 months ago 590f7a8
Check that no type vars are left after infer & subst

Crappy implementation -- just wanted it done asap. The error doesn't
tell what part of the type is still ambiguous, and some of
the (position, type) combinations of the check are kind of arbitrary.
7 files changed, 103 insertions(+), 18 deletions(-)

M src/AnnotAst.hs
M src/Check.hs
M src/Desugar.hs
M src/DesugaredAst.hs
M src/Infer.hs
M src/Subst.hs
M src/TypeErr.hs
M src/AnnotAst.hs => src/AnnotAst.hs +12 -4
@@ 1,10 1,12 @@
-- | Type annotated AST as a result of typechecking
module AnnotAst
    ( TVar(..)
    ( WithPos(..)
    , TVar(..)
    , TPrim(..)
    , TConst
    , Type(..)
    , Scheme(..)
    , Id
    , TypedVar(..)
    , Const(..)
    , VariantIx


@@ 12,7 14,8 @@ module AnnotAst
    , Span
    , VarBindings
    , DecisionTree(..)
    , Expr(..)
    , Expr
    , Expr'(..)
    , Defs
    , TypeDefs
    , Ctors


@@ 24,9 27,12 @@ import Data.Map.Strict (Map)
import Data.Word

import Ast (TVar(..), TPrim(..), TConst, Type(..), Scheme(..), Const(..))
import SrcPos


data TypedVar = TypedVar String Type
type Id = WithPos String

data TypedVar = TypedVar Id Type
    deriving (Show, Eq, Ord)

type VariantIx = Word64


@@ 43,7 49,7 @@ data DecisionTree
    | DSwitch Access (Map VariantIx DecisionTree) DecisionTree
    deriving Show

data Expr
data Expr'
    = Lit Const
    | Var TypedVar
    | App Expr Expr Type


@@ 55,6 61,8 @@ data Expr
    | Ctor VariantIx TConst [Type]
    deriving (Show)

type Expr = WithPos Expr'

type Defs = Map String (Scheme, Expr)
-- type TypeDefs = Map String ([TVar], [[Type]])
type TypeDefs = Map String ([TVar], [(String, [Type])])

M src/Check.hs => src/Check.hs +65 -0
@@ 4,10 4,13 @@ module Check (typecheck) where

import Prelude hiding (span)
import Control.Monad.Except
import Control.Monad.Reader
import Data.Bifunctor
import Data.Foldable
import qualified Data.Map.Strict as Map
import Data.Map.Strict (Map)
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Maybe

import SrcPos


@@ 28,6 31,7 @@ typecheck (Ast.Program defs tdefs externs) = runExcept $ do
    (tdefs', ctors) <- checkTypeDefs tdefs
    (externs', inferred, substs) <- inferTopDefs tdefs' ctors externs defs
    let substd = substTopDefs substs inferred
    checkTypeVarsBound substd
    let desugared = unsugar substd
    let tdefs'' = fmap (second (map snd)) tdefs'
    pure (uncurry Des.Program desugared tdefs'' externs')


@@ 130,3 134,64 @@ builtinDataTypes' =
      )
    , ("Str", [], [("Str", [TConst ("Array", [TPrim TNat8])])])
    ]

type Bound = ReaderT (Set TVar) (Except TypeErr) ()

-- TODO: Many of these positions are weird and kind of arbitrary, man. They may
--       not align with where the type variable is actually detected.
checkTypeVarsBound :: (An.Expr, An.Defs) -> Except TypeErr ()
checkTypeVarsBound (main, ds) = runReaderT
    (boundInExpr main >> boundInDefs ds)
    Set.empty
  where
    boundInDefs :: An.Defs -> Bound
    boundInDefs = mapM_ boundInDef
    boundInDef ((An.Forall tvs _), e) =
        local (Set.union tvs) (boundInExpr e)
    boundInExpr (WithPos pos e) = case e of
        An.Lit _ -> pure ()
        An.Var (An.TypedVar _ t) -> boundInType pos t
        An.App f a rt -> do
            boundInExpr f
            boundInExpr a
            boundInType pos rt
        An.If p c a -> do
            boundInExpr p
            boundInExpr c
            boundInExpr a
        An.Fun (_, pt) (e, et) -> do
            boundInType pos pt
            boundInExpr e
            boundInType pos et
        An.Let ds e -> do
            boundInDefs ds
            boundInExpr e
        An.Match m dt bt -> do
            boundInExpr m
            boundInDecTree dt
            boundInType pos bt
        An.FunMatch dt pt bt -> do
            boundInDecTree dt
            boundInType pos pt
            boundInType pos bt
        An.Ctor _ (_, instTs) ts -> do
            forM_ instTs (boundInType pos)
            forM_ ts (boundInType pos)
    boundInType :: SrcPos -> An.Type -> Bound
    boundInType pos = \case
        TVar tv ->
            ask
                >>= \bound -> when
                        (not (Set.member tv bound))
                        (throwError (UnboundTVar pos))
        TPrim _ -> pure ()
        TConst (_, ts) -> forM_ ts (boundInType pos)
        TFun ft at -> forM_ [ft, at] (boundInType pos)
        TBox t -> boundInType pos t
    boundInDecTree = \case
        An.DLeaf (bs, e) -> do
            forM_
                (Map.keys bs)
                (\(An.TypedVar (WithPos p _) t) -> boundInType p t)
            boundInExpr e
        An.DSwitch _ dts dt -> forM_ (dt : Map.elems dts) boundInDecTree

M src/Desugar.hs => src/Desugar.hs +8 -3
@@ 3,7 3,9 @@
module Desugar (unsugar) where

import Data.Bifunctor
import qualified Data.Map as Map

import SrcPos
import qualified AnnotAst as An
import DesugaredAst



@@ 14,9 16,9 @@ unsugarDefs :: An.Defs -> Defs
unsugarDefs = fmap (second unsugarExpr)

unsugarExpr :: An.Expr -> Expr
unsugarExpr = \case
unsugarExpr (WithPos _ e) = case e of
    An.Lit c -> Lit c
    An.Var tv -> Var tv
    An.Var v -> Var (unsugarTypedVar v)
    An.App f a rt -> App (unsugarExpr f) (unsugarExpr a) rt
    An.If p c a -> If (unsugarExpr p) (unsugarExpr c) (unsugarExpr a)
    An.Fun p b -> Fun p (first unsugarExpr b)


@@ 37,6 39,9 @@ unsugarExpr = \case

unsugarDecTree :: An.DecisionTree -> DecisionTree
unsugarDecTree = \case
    An.DLeaf (bs, e) -> DLeaf (bs, unsugarExpr e)
    An.DLeaf (bs, e) -> DLeaf (Map.mapKeys unsugarTypedVar bs, unsugarExpr e)
    An.DSwitch a cs def ->
        DSwitch a (fmap unsugarDecTree cs) (unsugarDecTree def)

unsugarTypedVar :: An.TypedVar -> TypedVar
unsugarTypedVar (An.TypedVar (WithPos _ x) t) = TypedVar x t

M src/DesugaredAst.hs => src/DesugaredAst.hs +5 -2
@@ 25,14 25,17 @@ import AnnotAst
    , TPrim(..)
    , TConst
    , Type(..)
    , TypedVar(..)
    , Scheme(..)
    , Const(..)
    , VariantIx
    , Access(..)
    , VarBindings
    )

data TypedVar = TypedVar String Type
    deriving (Show, Eq, Ord)

type VarBindings = Map TypedVar Access

data DecisionTree
    = DLeaf (VarBindings, Expr)
    | DSwitch Access (Map VariantIx DecisionTree) DecisionTree

M src/Infer.hs => src/Infer.hs +7 -8
@@ 24,7 24,7 @@ import NonEmpty
import qualified Ast
import Ast (Id(..), IdCase(..), idstr, scmBody)
import TypeErr
import AnnotAst
import AnnotAst hiding (Id)
import Match




@@ 142,10 142,10 @@ checkUserSchemes scms = forM_ scms $ \(WithPos p s1@(Forall _ t)) ->
        >>= \s2 -> when (s1 /= s2) (throwError (InvalidUserTypeSig p s1 s2))

infer :: Ast.Expr -> Infer (Type, Expr)
infer (WithPos pos e) = case e of
infer (WithPos pos e) = fmap (second (WithPos pos)) $ case e of
    Ast.Lit l -> pure (litType l, Lit l)
    Ast.Var (Id (WithPos p "_")) -> throwError (FoundHole p)
    Ast.Var x -> fmap (\t -> (t, Var (TypedVar (idstr x) t))) (lookupEnv x)
    Ast.Var x@(Id x') -> fmap (\t -> (t, Var (TypedVar x' t))) (lookupEnv x)
    Ast.App f a -> do
        ta <- fresh
        tr <- fresh


@@ 171,7 171,7 @@ infer (WithPos pos e) = case e of
        (bt, b') <- withLocals' defsScms (infer b)
        pure (bt, Let annotDefs b')
    Ast.TypeAscr x t -> do
        (tx, x') <- infer x
        (tx, WithPos _ x') <- infer x
        unify (Expected t) (Found (getPos x) tx)
        pure (t, x')
    Ast.Match matchee cases -> do


@@ 226,10 226,9 @@ inferPat = \case
    Ast.PVar (Id (WithPos _ "_")) -> do
        tv <- fresh
        pure (tv, PWild, Map.empty)
    Ast.PVar x -> do
    Ast.PVar x@(Id x') -> do
        tv <- fresh
        let x' = TypedVar (idstr x) tv
        pure (tv, PVar x', Map.singleton x (Forall Set.empty tv))
        pure (tv, PVar (TypedVar x' tv), Map.singleton x (Forall Set.empty tv))

inferPatConstruction
    :: SrcPos -> Id Big -> [Ast.Pat] -> Infer (Type, Pat, Map (Id Small) Scheme)


@@ 254,7 253,7 @@ nonconflictingPatVarDefs = flip foldM Map.empty $ \acc ks ->
        Just (Id (WithPos pos v)) -> throwError (ConflictingPatVarDefs pos v)
        Nothing -> pure (Map.union acc ks)

inferExprConstructor :: Id Big -> Infer (Type, Expr)
inferExprConstructor :: Id Big -> Infer (Type, Expr')
inferExprConstructor c = do
    (variantIx, tdefLhs, cParams, _) <- lookupEnvConstructor c
    (tdefInst, cParams') <- instantiateConstructorOfTypeDef tdefLhs cParams

M src/Subst.hs => src/Subst.hs +1 -1
@@ 20,7 20,7 @@ substDef :: Subst -> (Scheme, Expr) -> (Scheme, Expr)
substDef s = second (substExpr s)

substExpr :: Subst -> Expr -> Expr
substExpr s = \case
substExpr s (WithPos p e) = WithPos p $ case e of
    Lit c -> Lit c
    Var (TypedVar x t) -> Var (TypedVar x (subst s t))
    App f a rt -> App (substExpr s f) (substExpr s a) (subst s rt)

M src/TypeErr.hs => src/TypeErr.hs +5 -0
@@ 29,6 29,7 @@ data TypeErr
    | FoundHole SrcPos
    | RecTypeDef String SrcPos
    | UndefType SrcPos String
    | UnboundTVar SrcPos
    deriving Show

type Message = String


@@ 87,6 88,10 @@ prettyErr = \case
            ++ "has infinite size due to recursion without indirection.\n"
            ++ "Insert a pointer at some point to make it representable."
    UndefType p x -> posd p big $ "Undefined type `" ++ x ++ "` in constructor"
    UnboundTVar p ->
        posd p defOrExpr
            $ "Could not fully infer type of expression.\n"
            ++ "Type annotations needed."
  where
    -- | Used to handle that the position of the generated nested lambdas of a
    --   definition of the form `(define (foo a b ...) ...)` is set to the