~jojo/Carth

3cdd9e3c1c9ff4290861c7251e58f253df572168 — JoJo a month ago 9949085 lower2
For unbound tvars after Infer, substitute with Unit & accept

Before, unbound type vars remaining after Infer resulted in a
compilation error, but there's really no reason it should (right now,
at least). If a type var is unbound at that point, it means it could
be replaced with anything. So, we now substitute all remaining, free /
unbound tvars with ~Unit~ and accept the program.

For example, an unbound tvar could result from doing something like
`(const 69 (panic "123"))`. What type is the result of applying panic?
Anything!
13 files changed, 112 insertions(+), 102 deletions(-)

M src/Check.hs
M src/Checked.hs
M src/Codegen.hs
M src/Err.hs
M src/Infer.hs
M src/Inferred.hs
M src/Low.hs
M src/Lower.hs
M src/Monomorphic.hs
M src/Monomorphize.hs
M src/Subst.hs
D test/tests/bad/unbound-tvar.carth
A test/tests/good/unbound-tvar.carth
M src/Check.hs => src/Check.hs +49 -51
@@ 9,6 9,7 @@ import Control.Monad.State.Strict
import Data.Bifunctor
import Data.Bitraversable
import Data.Foldable
import Data.Functor
import Control.Applicative
import qualified Data.Map as Map
import Data.Map (Map)


@@ 34,9 35,9 @@ typecheck (Parsed.Program defs tdefs externs) = runExcept $ do
    (tdefs', ctors) <- checkTypeDefs tdefs
    externs' <- checkExterns tdefs' externs
    inferred <- inferTopDefs tdefs' ctors externs' defs
    checkTypeVarsBound inferred
    let bound = unboundTypeVarsToUnit inferred
    let mTypeDefs = fmap (map (unpos . fst) . snd) tdefs'
    compiled <- compileDecisionTrees mTypeDefs inferred
    compiled <- compileDecisionTrees mTypeDefs bound
    checkMainDefined compiled
    let tdefs'' = fmap (second (map snd)) tdefs'
    pure (Checked.Program compiled tdefs'' externs')


@@ 158,54 159,51 @@ checkExterns tdefs = fmap (Map.union Checked.builtinExterns . Map.fromList)
            Just tv -> throwError (ExternNotMonomorphic name tv)
            Nothing -> pure (idstr name, t')

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 :: Inferred.Defs -> Except TypeErr ()
checkTypeVarsBound ds = runReaderT (boundInDefs ds) Set.empty
-- Any free / unbound type variables left in the AST after Infer are replacable with any
-- type, unless there's a bug in the compiler. Therefore, replace them all with Unit now.
unboundTypeVarsToUnit :: Inferred.Defs -> Inferred.Defs
unboundTypeVarsToUnit (Topo defs) = Topo $ runReader (mapM goDef defs) Set.empty
  where
    boundInDefs :: Inferred.Defs -> Bound
    boundInDefs = mapM_ (secondM boundInDef) . Inferred.flattenDefs
    boundInDef (Inferred.Forall tvs _ _, e) = local (Set.union tvs) (boundInExpr e)
    boundInExpr (WithPos pos e) = case e of
        Inferred.Lit _ -> pure ()
        Inferred.Var (_, Inferred.TypedVar _ t) -> boundInType pos t
        Inferred.App f a rt -> do
            boundInExpr f
            boundInExpr a
            boundInType pos rt
        Inferred.If p c a -> do
            boundInExpr p
            boundInExpr c
            boundInExpr a
        Inferred.Let ld b -> do
            mapM_ (secondM boundInDef) (Inferred.defToVarDefs ld)
            boundInExpr b
        Inferred.FunMatch (cs, pt, bt) -> do
            boundInCases cs
            boundInType pos pt
            boundInType pos bt
        Inferred.Ctor _ _ (_, instTs) ts -> do
            forM_ instTs (boundInType pos)
            forM_ ts (boundInType pos)
        Inferred.Sizeof _t -> pure ()
    boundInType :: SrcPos -> Inferred.Type -> Bound
    boundInType pos = \case
        Inferred.TVar tv -> do
            bound <- ask
            when (not (Set.member tv bound)) (throwError (UnboundTVar pos))
        Inferred.TPrim _ -> pure ()
        Inferred.TConst (_, ts) -> forM_ ts (boundInType pos)
        Inferred.TFun ft at -> forM_ [ft, at] (boundInType pos)
        Inferred.TBox t -> boundInType pos t
    boundInCases cs = forM_ cs (bimapM boundInPat boundInExpr)
    boundInPat (WithPos pos pat) = case pat of
        Inferred.PVar (Inferred.TypedVar _ t) -> boundInType pos t
        Inferred.PWild -> pure ()
        Inferred.PCon con ps -> boundInCon pos con *> forM_ ps boundInPat
        Inferred.PBox p -> boundInPat p
    boundInCon pos (Con _ _ ts) = forM_ ts (boundInType pos)
    goDef :: Inferred.Def -> Reader (Set TVar) Inferred.Def
    goDef = \case
        Inferred.VarDef d -> fmap Inferred.VarDef $ secondM (goDefRhs goExpr) d
        Inferred.RecDefs ds ->
            fmap Inferred.RecDefs $ mapM (secondM (goDefRhs (mapPosdM goFunMatch))) ds

    goDefRhs f (scm, x) =
        fmap (scm, ) $ local (Set.union (Inferred._scmParams scm)) (f x)

    goFunMatch :: Inferred.FunMatch -> Reader (Set TVar) Inferred.FunMatch
    goFunMatch (cs, tp, tb) =
        liftA3 (,,) (mapM (bimapM goPat goExpr) cs) (subst tp) (subst tb)

    goExpr :: Inferred.Expr -> Reader (Set TVar) Inferred.Expr
    goExpr = mapPosdM $ \case
        Inferred.Lit c -> pure (Inferred.Lit c)
        Inferred.Var v -> fmap Inferred.Var $ secondM goTypedVar v
        Inferred.App f a tr -> liftA3 Inferred.App (goExpr f) (goExpr a) (subst tr)
        Inferred.If p c a -> liftA3 Inferred.If (goExpr p) (goExpr c) (goExpr a)
        Inferred.Let ld b -> liftA2 Inferred.Let (goDef ld) (goExpr b)
        Inferred.FunMatch fm -> fmap Inferred.FunMatch (goFunMatch fm)
        Inferred.Ctor v sp inst ts ->
            liftA2 (Inferred.Ctor v sp) (secondM (mapM subst) inst) (mapM subst ts)
        Inferred.Sizeof t -> fmap Inferred.Sizeof (subst t)

    goPat :: Inferred.Pat -> Reader (Set TVar) Inferred.Pat
    goPat = mapPosdM $ \case
        Inferred.PVar v -> fmap Inferred.PVar (goTypedVar v)
        Inferred.PWild -> pure Inferred.PWild
        Inferred.PCon con ps -> liftA2
            Inferred.PCon
            (fmap (\ts -> con { argTs = ts }) (mapM subst (argTs con)))
            (mapM goPat ps)
        Inferred.PBox p -> fmap Inferred.PBox (goPat p)

    goTypedVar (Inferred.TypedVar x t) = fmap (Inferred.TypedVar x) (subst t)

    subst :: Inferred.Type -> Reader (Set TVar) Inferred.Type
    subst t = ask <&> \bound ->
        subst' (\tv -> if Set.member tv bound then Nothing else Just tUnit) t

compileDecisionTrees :: MTypeDefs -> Inferred.Defs -> Except TypeErr Checked.Defs
compileDecisionTrees tdefs = compDefs


@@ 228,7 226,7 @@ compileDecisionTrees tdefs = compDefs
            Just e -> do
                dt <- liftEither e
                let v = (Checked.Var (NonVirt, Checked.TypedVar p tp))
                    b = Checked.Match v dt tb
                    b = Checked.Match v dt
                pure ((p, tp), (b, tb))

    compExpr :: Inferred.Expr -> Except TypeErr Checked.Expr


@@ 236,7 234,7 @@ compileDecisionTrees tdefs = compDefs
        Inferred.Lit c -> pure (Checked.Lit c)
        Inferred.Var (virt, Inferred.TypedVar (WithPos _ x) t) ->
            pure (Checked.Var (virt, Checked.TypedVar x t))
        Inferred.App f a tr -> liftA3 Checked.App (compExpr f) (compExpr a) (pure tr)
        Inferred.App f a _ -> liftA2 Checked.App (compExpr f) (compExpr a)
        Inferred.If p c a -> liftA3 Checked.If (compExpr p) (compExpr c) (compExpr a)
        Inferred.Let ld b -> liftA2 Checked.Let (compDef ld) (compExpr b)
        Inferred.FunMatch fm -> fmap Checked.Fun (compFunMatch (WithPos pos fm))

M src/Checked.hs => src/Checked.hs +2 -2
@@ 57,11 57,11 @@ type Var = (Virt, TypedVar)
data Expr
    = Lit Const
    | Var Var
    | App Expr Expr Type
    | App Expr Expr
    | If Expr Expr Expr
    | Fun Fun
    | Let Def Expr
    | Match Expr DecisionTree Type
    | Match Expr DecisionTree
    | Ction VariantIx Span TConst [Expr]
    | Sizeof Type
    | Absurd Type

M src/Codegen.hs => src/Codegen.hs +1 -1
@@ 220,7 220,7 @@ genExpr expr = do
        If p c a -> genExpr p >>= \p' -> genCondBr p' (genExpr c) (genExpr a)
        Fun (p, b) -> assign lambdaParentFunc parent *> genExprLambda p b >>= propagate
        Let d b -> genLet d b
        Match e cs _ -> genMatch e cs
        Match e cs -> genMatch e cs
        Ction c -> propagate =<< genCtion c
        Sizeof t ->
            propagate

M src/Err.hs => src/Err.hs +0 -4
@@ 66,10 66,6 @@ printTypeErr = \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 $ "Undefined type `" ++ x ++ "`."
    UnboundTVar p ->
        posd p
            $ "Could not fully infer type of expression, or otherwise unbound type variable.\n"
            ++ "Type annotations needed."
    WrongMainType p s ->
        posd p
            $ "Incorrect type of `main`.\n"

M src/Infer.hs => src/Infer.hs +6 -6
@@ 484,13 484,13 @@ generalize env mayGivenCs allCs t = fmap (\cs -> Forall vs cs t) constraints
    ftvEnv = Set.unions (map ftvScheme (Map.elems env))
    ftvScheme (Forall tvs _ t) = Set.difference (ftv t) tvs

substEnv :: Subst -> Map String Scheme -> Map String Scheme
substEnv :: Subst' -> Map String Scheme -> Map String Scheme
substEnv s = over (mapped . scmBody) (subst s)

ftvClassConstraint :: ClassConstraint -> Set TVar
ftvClassConstraint = mconcat . map ftv . snd

substClassConstraint :: Subst -> ClassConstraint -> ClassConstraint
substClassConstraint :: Subst' -> ClassConstraint -> ClassConstraint
substClassConstraint sub = second (map (subst sub))

fresh :: Infer Type


@@ 511,13 511,13 @@ unifyClass p c = tell ([], [(p, c)])

data UnifyErr = UInfType TVar Type | UFailed Type Type

solve :: Constraints -> Infer (Subst, (Map ClassConstraint SrcPos))
solve :: Constraints -> Infer (Subst', (Map ClassConstraint SrcPos))
solve (eqcs, ccs) = do
    sub <- lift $ lift $ lift $ solveUnis Map.empty eqcs
    ccs' <- solveClassCs (map (second (substClassConstraint sub)) ccs)
    pure (sub, ccs')
  where
    solveUnis :: Subst -> [EqConstraint] -> Except TypeErr Subst
    solveUnis :: Subst' -> [EqConstraint] -> Except TypeErr Subst'
    solveUnis sub1 = \case
        [] -> pure sub1
        (Expected et, Found pos ft) : cs -> do


@@ 606,7 606,7 @@ solve (eqcs, ccs) = do
        UInfType a t -> InfType pos t1 t2 a t
        UFailed t'1 t'2 -> UnificationFailed pos t1 t2 t'1 t'2

unifies :: Type -> Type -> Except UnifyErr Subst
unifies :: Type -> Type -> Except UnifyErr Subst'
unifies = curry $ \case
    (TPrim a, TPrim b) | a == b -> pure Map.empty
    (TConst (c0, ts0), TConst (c1, ts1)) | c0 == c1 -> if length ts0 /= length ts1


@@ 623,7 623,7 @@ unifies = curry $ \case
    (TBox t, TBox u) -> unifies t u
    (t1, t2) -> throwError (UFailed t1 t2)
  where
    unifiesMany :: [Type] -> [Type] -> Except UnifyErr Subst
    unifiesMany :: [Type] -> [Type] -> Except UnifyErr Subst'
    unifiesMany ts us = foldM
        (\s (t, u) -> fmap (flip composeSubsts s) (unifies (subst s t) (subst s u)))
        Map.empty

M src/Inferred.hs => src/Inferred.hs +0 -1
@@ 34,7 34,6 @@ data TypeErr
    | FoundHole SrcPos
    | RecTypeDef String SrcPos
    | UndefType SrcPos String
    | UnboundTVar SrcPos
    | WrongMainType SrcPos Parsed.Scheme
    | RecursiveVarDef (WithPos String)
    | TypeInstArityMismatch SrcPos String Int Int

M src/Low.hs => src/Low.hs +2 -2
@@ 52,7 52,7 @@ data Expr
    | If Expr Expr Expr
    | Fun Fun
    | Let Def Expr
    | Match Expr DecisionTree Type
    | Match Expr DecisionTree
    | Ction Ction
    | Sizeof Type
    | Absurd Type


@@ 89,7 89,7 @@ fvExpr = \case
    Let (VarDef (lhs, (_, rhs))) e ->
        Set.union (freeVars rhs) (Set.delete lhs (freeVars e))
    Let (RecDefs ds) e -> fvLet (unzip (map (second (Fun . snd)) ds)) e
    Match e dt _ -> Set.union (freeVars e) (fvDecisionTree dt)
    Match e dt -> Set.union (freeVars e) (fvDecisionTree dt)
    Ction (_, _, _, as) -> Set.unions (map freeVars as)
    Sizeof _t -> Set.empty
    Absurd _ -> Set.empty

M src/Lower.hs => src/Lower.hs +1 -1
@@ 44,7 44,7 @@ lowerExpr = \case
    Ast.If p c a -> If (lowerExpr p) (lowerExpr c) (lowerExpr a)
    Ast.Fun f -> Fun (lowerFun f)
    Ast.Let d e -> Let (lowerDef d) (lowerExpr e)
    Ast.Match m dt t -> Match (lowerExpr m) (lowerDecisionTree dt) (lowerType t)
    Ast.Match m dt -> Match (lowerExpr m) (lowerDecisionTree dt)
    Ast.Ction c -> Ction $ lowerCtion c
    Ast.Sizeof t -> Sizeof $ lowerType t
    Ast.Absurd t -> Absurd $ lowerType t

M src/Monomorphic.hs => src/Monomorphic.hs +1 -1
@@ 64,7 64,7 @@ data Expr
    | If Expr Expr Expr
    | Fun Fun
    | Let Def Expr
    | Match Expr DecisionTree Type
    | Match Expr DecisionTree
    | Ction Ction
    | Sizeof Type
    | Absurd Type

M src/Monomorphize.hs => src/Monomorphize.hs +4 -4
@@ 95,11 95,11 @@ mono = \case
            Virt -> pure ()
            NonVirt -> tell (DefInsts (Map.singleton x (Set.singleton t')))
        pure (Var (virt, TypedVar x t'))
    Checked.App f a _ -> liftA2 App (mono f) (mono a)
    Checked.App f a -> liftA2 App (mono f) (mono a)
    Checked.If p c a -> liftA3 If (mono p) (mono c) (mono a)
    Checked.Fun f -> fmap (Fun) (monoFun f)
    Checked.Let d e -> monoLet d e
    Checked.Match e cs tbody -> monoMatch e cs tbody
    Checked.Match e cs -> monoMatch e cs
    Checked.Ction v span' inst as -> monoCtion v span' inst as
    Checked.Sizeof t -> fmap Sizeof (monotype t)
    Checked.Absurd t -> fmap Absurd (monotype t)


@@ 164,8 164,8 @@ genInst (Forall _ _ rhsT) monoRhs instT = do
    rhs' <- local (Map.union boundTvs) monoRhs
    pure (Map.elems boundTvs, rhs')

monoMatch :: Checked.Expr -> Checked.DecisionTree -> Checked.Type -> Mono Expr
monoMatch e dt tbody = liftA3 Match (mono e) (monoDecisionTree dt) (monotype tbody)
monoMatch :: Checked.Expr -> Checked.DecisionTree -> Mono Expr
monoMatch e dt = liftA2 Match (mono e) (monoDecisionTree dt)

monoDecisionTree :: Checked.DecisionTree -> Mono DecisionTree
monoDecisionTree = \case

M src/Subst.hs => src/Subst.hs +35 -24
@@ 1,4 1,4 @@
module Subst (Subst, subst, substExpr, substFunMatch, composeSubsts) where
module Subst (Subst, Subst', subst, subst', substDef, substExpr, substExpr', substFunMatch, substFunMatch', composeSubsts) where

import qualified Data.Map as Map
import Data.Map (Map)


@@ 9,29 9,37 @@ import SrcPos
import Inferred

-- | Map of substitutions from type-variables to more specific types
type Subst = Map TVar Type
type Subst = TVar -> Maybe Type
type Subst' = Map TVar Type

substDef :: Subst -> Def -> Def
substDef s = \case
    VarDef d -> VarDef (second (second (substExpr s)) d)
    RecDefs ds -> RecDefs (map (second (second (mapPosd (substFunMatch s)))) ds)
    VarDef d -> VarDef (second (second (substExpr' s)) d)
    RecDefs ds -> RecDefs (map (second (second (mapPosd (substFunMatch' s)))) ds)

substExpr :: Subst -> Expr -> Expr
substExpr s (WithPos pos expr) = WithPos pos $ case expr of
substExpr :: Map TVar Type -> Expr -> Expr
substExpr s = substExpr' (flip Map.lookup s)

substExpr' :: Subst -> Expr -> Expr
substExpr' s (WithPos pos expr) = WithPos pos $ case expr of
    Lit c -> Lit c
    Var v -> Var (second (substTypedVar s) v)
    App f a rt -> App (substExpr s f) (substExpr s a) (subst s rt)
    If p c a -> If (substExpr s p) (substExpr s c) (substExpr s a)
    Let def body -> Let (substDef s def) (substExpr s body)
    FunMatch f -> FunMatch (substFunMatch s f)
    Ctor i span' (tx, tts) ps -> Ctor i span' (tx, map (subst s) tts) (map (subst s) ps)
    Sizeof t -> Sizeof (subst s t)
    App f a rt -> App (substExpr' s f) (substExpr' s a) (subst' s rt)
    If p c a -> If (substExpr' s p) (substExpr' s c) (substExpr' s a)
    Let def body -> Let (substDef s def) (substExpr' s body)
    FunMatch f -> FunMatch (substFunMatch' s f)
    Ctor i span' (tx, tts) ps ->
        Ctor i span' (tx, map (subst' s) tts) (map (subst' s) ps)
    Sizeof t -> Sizeof (subst' s t)

substFunMatch :: Map TVar Type -> FunMatch -> FunMatch
substFunMatch s = substFunMatch' (flip Map.lookup s)

substFunMatch :: Subst -> FunMatch -> FunMatch
substFunMatch s (cs, tp, tb) = ((substCases s cs), (subst s tp), (subst s tb))
substFunMatch' :: Subst -> FunMatch -> FunMatch
substFunMatch' s (cs, tp, tb) = ((substCases s cs), (subst' s tp), (subst' s tb))

substCases :: Subst -> Cases -> Cases
substCases s cs = map (bimap (substPat s) (substExpr s)) cs
substCases s cs = map (bimap (substPat s) (substExpr' s)) cs

substPat :: Subst -> Pat -> Pat
substPat s (WithPos pos pat) = WithPos pos $ case pat of


@@ 41,18 49,21 @@ substPat s (WithPos pos pat) = WithPos pos $ case pat of
    PCon c ps -> PCon (substCon s c) (map (substPat s) ps)

substCon :: Subst -> Con -> Con
substCon s (Con ix sp ts) = Con ix sp (map (subst s) ts)
substCon s (Con ix sp ts) = Con ix sp (map (subst' s) ts)

substTypedVar :: Subst -> TypedVar -> TypedVar
substTypedVar s (TypedVar x t) = TypedVar x (subst s t)
substTypedVar s (TypedVar x t) = TypedVar x (subst' s t)

subst :: Map TVar Type -> Type -> Type
subst s = subst' (flip Map.lookup s)

subst :: Subst -> Type -> Type
subst s t = case t of
    TVar tv -> fromMaybe t (Map.lookup tv s)
subst' :: Subst -> Type -> Type
subst' s t = case t of
    TVar tv -> fromMaybe t (s tv)
    TPrim _ -> t
    TFun a b -> TFun (subst s a) (subst s b)
    TBox a -> TBox (subst s a)
    TConst (c, ts) -> TConst (c, (map (subst s) ts))
    TFun a b -> TFun (subst' s a) (subst' s b)
    TBox a -> TBox (subst' s a)
    TConst (c, ts) -> TConst (c, (map (subst' s) ts))

composeSubsts :: Subst -> Subst -> Subst
composeSubsts :: Map TVar Type -> Map TVar Type -> Map TVar Type
composeSubsts s1 s2 = Map.union (fmap (subst s1) s2) s1

D test/tests/bad/unbound-tvar.carth => test/tests/bad/unbound-tvar.carth +0 -5
@@ 1,5 0,0 @@
;; UnboundTVar

(define (seq a b) b)
(define (undef a) (undef a))
(define (foo a) (seq (undef Unit) 123))

A test/tests/good/unbound-tvar.carth => test/tests/good/unbound-tvar.carth +11 -0
@@ 0,0 1,11 @@
;; 456

(import std)

(define (foo p)
  (if p
      (seq (undefined Unit) 123)
    456))

(define main
  (display (show-int (foo False))))